[STATEMENT]
lemma acyclic_trans':
 assumes "is_acyclic x"
   shows "x\<^sup>\<star> \<le> -(x\<^sup>T\<^sup>+)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x\<^sup>\<star> \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
have "x\<^sup>\<star> \<le> - (- (- (x\<^sup>T ; - (- 1'))) ; (x\<^sup>\<star>)\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star> \<le> - (- (- (x\<^sup>T ; - (- 1'))) ; (x\<^sup>\<star>)\<^sup>T)
[PROOF STEP]
by (metis assms conv_galois_1 conv_galois_2 order_trans star_trans)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> \<le> - (- (- (x\<^sup>T ; - (- 1'))) ; (x\<^sup>\<star>)\<^sup>T)

goal (1 subgoal):
 1. x\<^sup>\<star> \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x\<^sup>\<star> \<le> - (- (- (x\<^sup>T ; - (- 1'))) ; (x\<^sup>\<star>)\<^sup>T)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sup>\<star> \<le> - (- (- (x\<^sup>T ; - (- 1'))) ; (x\<^sup>\<star>)\<^sup>T)

goal (1 subgoal):
 1. x\<^sup>\<star> \<le> - x\<^sup>T\<^sup>+
[PROOF STEP]
by (simp add: star_conv)
[PROOF STATE]
proof (state)
this:
x\<^sup>\<star> \<le> - x\<^sup>T\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma regressively_finite_acyclic:
  assumes "regressively_finite x"
    shows "is_acyclic x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
have 1: "is_vector ((x\<^sup>+ \<cdot> 1');1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_vector ((x\<^sup>+ \<cdot> 1') ; 1)
[PROOF STEP]
by (simp add: is_vector_def mult_assoc)
[PROOF STATE]
proof (state)
this:
is_vector ((x\<^sup>+ \<cdot> 1') ; 1)

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
have "(x\<^sup>+ \<cdot> 1');1 = (x\<^sup>T\<^sup>+ \<cdot> 1');1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>+ \<cdot> 1') ; 1 = (x\<^sup>T\<^sup>+ \<cdot> 1') ; 1
[PROOF STEP]
by (metis plus_conv test_converse)
[PROOF STATE]
proof (state)
this:
(x\<^sup>+ \<cdot> 1') ; 1 = (x\<^sup>T\<^sup>+ \<cdot> 1') ; 1

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x\<^sup>+ \<cdot> 1') ; 1 = (x\<^sup>T\<^sup>+ \<cdot> 1') ; 1

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
have "... \<le> x\<^sup>T;(1';x\<^sup>T\<^sup>\<star> \<cdot> x);1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>T\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; (1' ; x\<^sup>T\<^sup>\<star> \<cdot> x) ; 1
[PROOF STEP]
by (metis conv_invol modular_1_var mult_isor mult_oner mult_onel)
[PROOF STATE]
proof (state)
this:
(x\<^sup>T\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; (1' ; x\<^sup>T\<^sup>\<star> \<cdot> x) ; 1

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x\<^sup>T\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; (1' ; x\<^sup>T\<^sup>\<star> \<cdot> x) ; 1

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
have "... \<le> x\<^sup>T;(1' \<cdot> x\<^sup>+);x\<^sup>T\<^sup>\<star>;1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T ; (1' ; x\<^sup>T\<^sup>\<star> \<cdot> x) ; 1 \<le> x\<^sup>T ; (1' \<cdot> x\<^sup>+) ; x\<^sup>T\<^sup>\<star> ; 1
[PROOF STEP]
by (metis comp_assoc conv_invol modular_2_var mult_isol mult_isor star_conv)
[PROOF STATE]
proof (state)
this:
x\<^sup>T ; (1' ; x\<^sup>T\<^sup>\<star> \<cdot> x) ; 1 \<le> x\<^sup>T ; (1' \<cdot> x\<^sup>+) ; x\<^sup>T\<^sup>\<star> ; 1

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>T ; (1' ; x\<^sup>T\<^sup>\<star> \<cdot> x) ; 1 \<le> x\<^sup>T ; (1' \<cdot> x\<^sup>+) ; x\<^sup>T\<^sup>\<star> ; 1

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
have "... = x\<^sup>T;(x\<^sup>+ \<cdot> 1');1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T ; (1' \<cdot> x\<^sup>+) ; x\<^sup>T\<^sup>\<star> ; 1 = x\<^sup>T ; (x\<^sup>+ \<cdot> 1') ; 1
[PROOF STEP]
by (metis comp_assoc conway.dagger_unfoldr_distr inf.commute sup.cobounded1 top_le)
[PROOF STATE]
proof (state)
this:
x\<^sup>T ; (1' \<cdot> x\<^sup>+) ; x\<^sup>T\<^sup>\<star> ; 1 = x\<^sup>T ; (x\<^sup>+ \<cdot> 1') ; 1

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; (x\<^sup>+ \<cdot> 1') ; 1
[PROOF STEP]
have "(x\<^sup>+ \<cdot> 1');1 = 0"
[PROOF STATE]
proof (prove)
using this:
(x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; (x\<^sup>+ \<cdot> 1') ; 1

goal (1 subgoal):
 1. (x\<^sup>+ \<cdot> 1') ; 1 = 0
[PROOF STEP]
using 1 assms
[PROOF STATE]
proof (prove)
using this:
(x\<^sup>+ \<cdot> 1') ; 1 \<le> x\<^sup>T ; (x\<^sup>+ \<cdot> 1') ; 1
is_vector ((x\<^sup>+ \<cdot> 1') ; 1)
regressively_finite x

goal (1 subgoal):
 1. (x\<^sup>+ \<cdot> 1') ; 1 = 0
[PROOF STEP]
by (simp add: comp_assoc)
[PROOF STATE]
proof (state)
this:
(x\<^sup>+ \<cdot> 1') ; 1 = 0

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(x\<^sup>+ \<cdot> 1') ; 1 = 0

goal (1 subgoal):
 1. is_acyclic x
[PROOF STEP]
by (simp add: galois_aux ss_p18)
[PROOF STATE]
proof (state)
this:
is_acyclic x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_suc_below_plus:
  "x \<up> Suc n \<le> x\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. power.power 1' (;) x (Suc n) \<le> x\<^sup>+
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. power.power 1' (;) x (Suc zero_class.zero) \<le> x\<^sup>+
 2. \<And>n. power.power 1' (;) x (Suc n) \<le> x\<^sup>+ \<Longrightarrow> power.power 1' (;) x (Suc (Suc n)) \<le> x\<^sup>+
[PROOF STEP]
using mult_isol star_ref
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z ; ?x \<le> ?z ; ?y
reflexive (?x\<^sup>\<star>)

goal (2 subgoals):
 1. power.power 1' (;) x (Suc zero_class.zero) \<le> x\<^sup>+
 2. \<And>n. power.power 1' (;) x (Suc n) \<le> x\<^sup>+ \<Longrightarrow> power.power 1' (;) x (Suc (Suc n)) \<le> x\<^sup>+
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. power.power 1' (;) x (Suc n) \<le> x\<^sup>+ \<Longrightarrow> power.power 1' (;) x (Suc (Suc n)) \<le> x\<^sup>+
[PROOF STEP]
by (simp add: mult_isol_var order_trans)


[STATEMENT]
lemma point_loop_not_acyclic:
  assumes "is_point p"
      and "p \<le> x \<up> Suc n ; p"
    shows "\<not> is_acyclic x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_acyclic x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_acyclic x
[PROOF STEP]
have "p \<le> x\<^sup>+ ; p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> x\<^sup>+ ; p
[PROOF STEP]
by (meson assms dual_order.trans point_def point_is_point ss423bij power_suc_below_plus)
[PROOF STATE]
proof (state)
this:
p \<le> x\<^sup>+ ; p

goal (1 subgoal):
 1. \<not> is_acyclic x
[PROOF STEP]
hence "p ; p\<^sup>T \<le> x\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
p \<le> x\<^sup>+ ; p

goal (1 subgoal):
 1. p ; p\<^sup>T \<le> x\<^sup>+
[PROOF STEP]
using assms(1) point_def point_is_point ss423bij
[PROOF STATE]
proof (prove)
using this:
p \<le> x\<^sup>+ ; p
is_point p
point ?x \<equiv> is_vector ?x \<and> bijective ?x
point ?x = is_point ?x
bijective ?x \<Longrightarrow> (?y ; ?x\<^sup>T \<le> ?z) = (?y \<le> ?z ; ?x)

goal (1 subgoal):
 1. p ; p\<^sup>T \<le> x\<^sup>+
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p ; p\<^sup>T \<le> x\<^sup>+

goal (1 subgoal):
 1. \<not> is_acyclic x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p ; p\<^sup>T \<le> x\<^sup>+

goal (1 subgoal):
 1. \<not> is_acyclic x
[PROOF STEP]
using assms(1) order.trans point_not_equal(1) point_not_equal(2)
[PROOF STATE]
proof (prove)
using this:
p ; p\<^sup>T \<le> x\<^sup>+
is_point p
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c
\<lbrakk>is_point ?p; is_point ?q\<rbrakk> \<Longrightarrow> (?p \<noteq> ?q) = (?p \<le> - ?q)
\<lbrakk>is_point ?p; is_point ?q\<rbrakk> \<Longrightarrow> (?p \<le> - ?q) = (?p ; ?q\<^sup>T \<le> - 1')

goal (1 subgoal):
 1. \<not> is_acyclic x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_acyclic x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_power_vanishes:
  assumes "is_acyclic x"
    shows "\<exists>n . x \<up> Suc n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. power.power 1' (;) x (Suc n) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. power.power 1' (;) x (Suc n) = 0
[PROOF STEP]
let ?n = "card { p . is_point p }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. power.power 1' (;) x (Suc n) = 0
[PROOF STEP]
let ?p = "x \<up> ?n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. power.power 1' (;) x (Suc n) = 0
[PROOF STEP]
have "?p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) = 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "?p \<noteq> 0"
[PROOF STATE]
proof (state)
this:
power.power 1' (;) x (card {p. is_point p}) \<noteq> 0

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
power.power 1' (;) x (card {p. is_point p}) \<noteq> 0
[PROOF STEP]
obtain p q where 1: "point p \<and> point q \<and> p;q\<^sup>T \<le> ?p"
[PROOF STATE]
proof (prove)
using this:
power.power 1' (;) x (card {p. is_point p}) \<noteq> 0

goal (1 subgoal):
 1. (\<And>p q. point p \<and> point q \<and> p ; q\<^sup>T \<le> power.power 1' (;) x (card {p. is_point p}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using point_axiom
[PROOF STATE]
proof (prove)
using this:
power.power 1' (;) x (card {p. is_point p}) \<noteq> 0
?x \<noteq> 0 \<longrightarrow> (\<exists>y z. point y \<and> point z \<and> y ; z\<^sup>T \<le> ?x)

goal (1 subgoal):
 1. (\<And>p q. point p \<and> point q \<and> p ; q\<^sup>T \<le> power.power 1' (;) x (card {p. is_point p}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
point p \<and> point q \<and> p ; q\<^sup>T \<le> power.power 1' (;) x (card {p. is_point p})

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence 2: "p \<le> ?p;q"
[PROOF STATE]
proof (prove)
using this:
point p \<and> point q \<and> p ; q\<^sup>T \<le> power.power 1' (;) x (card {p. is_point p})

goal (1 subgoal):
 1. p \<le> power.power 1' (;) x (card {p. is_point p}) ; q
[PROOF STEP]
using point_def ss423bij
[PROOF STATE]
proof (prove)
using this:
point p \<and> point q \<and> p ; q\<^sup>T \<le> power.power 1' (;) x (card {p. is_point p})
point ?x \<equiv> is_vector ?x \<and> bijective ?x
bijective ?x \<Longrightarrow> (?y ; ?x\<^sup>T \<le> ?z) = (?y \<le> ?z ; ?x)

goal (1 subgoal):
 1. p \<le> power.power 1' (;) x (card {p. is_point p}) ; q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<le> power.power 1' (;) x (card {p. is_point p}) ; q

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "\<forall>n\<le>?n . (\<exists>f. \<forall>i\<le>n . is_point (f i) \<and> (\<forall>j\<le>i . p \<le> x\<up>(?n-i) ; f i \<and> f i \<le> x\<up>(i-j) ; f j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<le>card {p. is_point p}. \<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
show "n\<le>?n \<longrightarrow> (\<exists>f. \<forall>i\<le>n . is_point (f i) \<and> (\<forall>j\<le>i . p \<le> x\<up>(?n-i) ; f i \<and> f i \<le> x\<up>(i-j) ; f j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zero_class.zero \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>zero_class.zero. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
 2. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)) \<Longrightarrow> Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. zero_class.zero \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>zero_class.zero. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
 2. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)) \<Longrightarrow> Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_class.zero \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>zero_class.zero. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
using 1 2 point_is_point
[PROOF STATE]
proof (prove)
using this:
point p \<and> point q \<and> p ; q\<^sup>T \<le> power.power 1' (;) x (card {p. is_point p})
p \<le> power.power 1' (;) x (card {p. is_point p}) ; q
point ?x = is_point ?x

goal (1 subgoal):
 1. zero_class.zero \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>zero_class.zero. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
zero_class.zero \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>zero_class.zero. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))

goal (1 subgoal):
 1. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)) \<Longrightarrow> Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)) \<Longrightarrow> Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))

goal (1 subgoal):
 1. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)) \<Longrightarrow> Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)) \<Longrightarrow> Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
assume 3: "n\<le>?n \<longrightarrow> (\<exists>f . \<forall>i\<le>n . is_point (f i) \<and> (\<forall>j\<le>i . p \<le> x \<up> (?n-i) ; f i \<and> f i \<le> x \<up> (i-j) ; f j))"
[PROOF STATE]
proof (state)
this:
n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))

goal (1 subgoal):
 1. \<And>n. n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)) \<Longrightarrow> Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
show "Suc n\<le>?n \<longrightarrow> (\<exists>f . \<forall>i\<le>Suc n . is_point (f i) \<and> (\<forall>j\<le>i . p \<le> x \<up> (?n-i) ; f i \<and> f i \<le> x \<up> (i-j) ; f j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
assume 4: "Suc n\<le>?n"
[PROOF STATE]
proof (state)
this:
Suc n \<le> card {p. is_point p}

goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Suc n \<le> card {p. is_point p}
[PROOF STEP]
obtain f where 5: "\<forall>i\<le>n . is_point (f i) \<and> (\<forall>j\<le>i . p \<le> x \<up> (?n-i) ; f i \<and> f i \<le> x \<up> (i-j) ; f j)"
[PROOF STATE]
proof (prove)
using this:
Suc n \<le> card {p. is_point p}

goal (1 subgoal):
 1. (\<And>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
Suc n \<le> card {p. is_point p}
n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))

goal (1 subgoal):
 1. (\<And>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
have "p \<le> x \<up> (?n-n) ; f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> power.power 1' (;) x (card {p. is_point p} - n) ; f n
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal (1 subgoal):
 1. p \<le> power.power 1' (;) x (card {p. is_point p} - n) ; f n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<le> power.power 1' (;) x (card {p. is_point p} - n) ; f n

goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p \<le> power.power 1' (;) x (card {p. is_point p} - n) ; f n

goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
have "... = x \<up> (?n-n-one_class.one) ; x ; f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p} - n) ; f n = power.power 1' (;) x (card {p. is_point p} - n - one_class.one) ; x ; f n
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
Suc n \<le> card {p. is_point p}

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p} - n) ; f n = power.power 1' (;) x (card {p. is_point p} - n - one_class.one) ; x ; f n
[PROOF STEP]
by (metis (no_types) Suc_diff_le diff_Suc_1 diff_Suc_Suc power_Suc2)
[PROOF STATE]
proof (state)
this:
power.power 1' (;) x (card {p. is_point p} - n) ; f n = power.power 1' (;) x (card {p. is_point p} - n - one_class.one) ; x ; f n

goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p \<le> power.power 1' (;) x (card {p. is_point p} - n - one_class.one) ; x ; f n
[PROOF STEP]
obtain r where 6: "point r \<and> p \<le> x \<up> (?n-Suc n) ; r \<and> r \<le> x ; f n"
[PROOF STATE]
proof (prove)
using this:
p \<le> power.power 1' (;) x (card {p. is_point p} - n - one_class.one) ; x ; f n

goal (1 subgoal):
 1. (\<And>r. point r \<and> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; r \<and> r \<le> x ; f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1 5 intermediate_point_theorem point_is_point
[PROOF STATE]
proof (prove)
using this:
p \<le> power.power 1' (;) x (card {p. is_point p} - n - one_class.one) ; x ; f n
point p \<and> point q \<and> p ; q\<^sup>T \<le> power.power 1' (;) x (card {p. is_point p})
\<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
\<lbrakk>point ?p; point ?r\<rbrakk> \<Longrightarrow> (?p \<le> ?x ; ?y ; ?r) = (\<exists>q. point q \<and> ?p \<le> ?x ; q \<and> q \<le> ?y ; ?r)
point ?x = is_point ?x

goal (1 subgoal):
 1. (\<And>r. point r \<and> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; r \<and> r \<le> x ; f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
point r \<and> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; r \<and> r \<le> x ; f n

goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
let ?g = "\<lambda>m . if m = Suc n then r else f m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
have "\<forall>i\<le>Suc n . is_point (?g i) \<and> (\<forall>j\<le>i . p \<le> x \<up> (?n-i) ; ?g i \<and> ?g i \<le> x \<up> (i-j) ; ?g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<le>Suc n. is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
show "i\<le>Suc n \<longrightarrow> is_point (?g i) \<and> (\<forall>j\<le>i . p \<le> x \<up> (?n-i) ; ?g i \<and> ?g i \<le> x \<up> (i-j) ; ?g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
proof (cases "i\<le>n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
 2. \<not> i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<le> n

goal (2 subgoals):
 1. i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
 2. \<not> i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> n

goal (1 subgoal):
 1. i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
i \<le> n
\<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal (1 subgoal):
 1. i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))

goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i \<le> n

goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
have "is_point (?g (Suc n)) \<and> (\<forall>j\<le>Suc n . p \<le> x \<up> (?n-Suc n) ; ?g (Suc n) \<and> ?g (Suc n) \<le> x \<up> (Suc n-j) ; ?g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_point (if Suc n = Suc n then r else f (Suc n)) \<and> (\<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_point (if Suc n = Suc n then r else f (Suc n))
 2. \<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
show "is_point (?g (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_point (if Suc n = Suc n then r else f (Suc n))
[PROOF STEP]
using 6 point_is_point
[PROOF STATE]
proof (prove)
using this:
point r \<and> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; r \<and> r \<le> x ; f n
point ?x = is_point ?x

goal (1 subgoal):
 1. is_point (if Suc n = Suc n then r else f (Suc n))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_point (if Suc n = Suc n then r else f (Suc n))

goal (1 subgoal):
 1. \<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
show "\<forall>j\<le>Suc n . p \<le> x \<up> (?n-Suc n) ; ?g (Suc n) \<and> ?g (Suc n) \<le> x \<up> (Suc n-j) ; ?g j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j \<le> Suc n \<longrightarrow> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j \<le> Suc n \<longrightarrow> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
show "j\<le>Suc n \<longrightarrow> p \<le> x \<up> (?n-Suc n) ; ?g (Suc n) \<and> ?g (Suc n) \<le> x \<up> (Suc n-j) ; ?g j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> Suc n \<longrightarrow> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<le> Suc n \<Longrightarrow> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
assume 7: "j\<le>Suc n"
[PROOF STATE]
proof (state)
this:
j \<le> Suc n

goal (1 subgoal):
 1. j \<le> Suc n \<Longrightarrow> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
show "p \<le> x \<up> (?n-Suc n) ; ?g (Suc n) \<and> ?g (Suc n) \<le> x \<up> (Suc n-j) ; ?g j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n))
 2. (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
show "p \<le> x \<up> (?n-Suc n) ; ?g (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n))
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
point r \<and> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; r \<and> r \<le> x ; f n

goal (1 subgoal):
 1. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n))

goal (1 subgoal):
 1. (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
show "?g (Suc n) \<le> x \<up> (Suc n-j) ; ?g j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
proof (cases "j = Suc n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j = Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
 2. j \<noteq> Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j = Suc n

goal (2 subgoals):
 1. j = Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
 2. j \<noteq> Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j = Suc n

goal (1 subgoal):
 1. (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)

goal (1 subgoal):
 1. j \<noteq> Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
j \<noteq> Suc n

goal (1 subgoal):
 1. j \<noteq> Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
hence "f n \<le> x \<up> (n-j) ; f j"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> Suc n

goal (1 subgoal):
 1. f n \<le> power.power 1' (;) x (n - j) ; f j
[PROOF STEP]
using 5 7
[PROOF STATE]
proof (prove)
using this:
j \<noteq> Suc n
\<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
j \<le> Suc n

goal (1 subgoal):
 1. f n \<le> power.power 1' (;) x (n - j) ; f j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f n \<le> power.power 1' (;) x (n - j) ; f j

goal (1 subgoal):
 1. j \<noteq> Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
hence "x ; f n \<le> x \<up> (Suc n-j) ; f j"
[PROOF STATE]
proof (prove)
using this:
f n \<le> power.power 1' (;) x (n - j) ; f j

goal (1 subgoal):
 1. x ; f n \<le> power.power 1' (;) x (Suc n - j) ; f j
[PROOF STEP]
using 7 False Suc_diff_le comp_assoc mult_isol
[PROOF STATE]
proof (prove)
using this:
f n \<le> power.power 1' (;) x (n - j) ; f j
j \<le> Suc n
j \<noteq> Suc n
?n \<le> ?m \<Longrightarrow> Suc ?m - ?n = Suc (?m - ?n)
?x ; ?y ; ?z = ?x ; (?y ; ?z)
?x \<le> ?y \<Longrightarrow> ?z ; ?x \<le> ?z ; ?y

goal (1 subgoal):
 1. x ; f n \<le> power.power 1' (;) x (Suc n - j) ; f j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x ; f n \<le> power.power 1' (;) x (Suc n - j) ; f j

goal (1 subgoal):
 1. j \<noteq> Suc n \<Longrightarrow> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x ; f n \<le> power.power 1' (;) x (Suc n - j) ; f j

goal (1 subgoal):
 1. (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
using 6 False
[PROOF STATE]
proof (prove)
using this:
x ; f n \<le> power.power 1' (;) x (Suc n - j) ; f j
point r \<and> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; r \<and> r \<le> x ; f n
j \<noteq> Suc n

goal (1 subgoal):
 1. (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
j \<le> Suc n \<longrightarrow> p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_point (if Suc n = Suc n then r else f (Suc n)) \<and> (\<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j))

goal (1 subgoal):
 1. \<not> i \<le> n \<Longrightarrow> i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_point (if Suc n = Suc n then r else f (Suc n)) \<and> (\<forall>j\<le>Suc n. p \<le> power.power 1' (;) x (card {p. is_point p} - Suc n) ; (if Suc n = Suc n then r else f (Suc n)) \<and> (if Suc n = Suc n then r else f (Suc n)) \<le> power.power 1' (;) x (Suc n - j) ; (if j = Suc n then r else f j))

goal (1 subgoal):
 1. i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))
[PROOF STEP]
by (simp add: False le_Suc_eq)
[PROOF STATE]
proof (state)
this:
i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<le> Suc n \<longrightarrow> is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>Suc n. is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))

goal (1 subgoal):
 1. Suc n \<le> card {p. is_point p} \<Longrightarrow> \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
thus "\<exists>f . \<forall>i\<le>Suc n . is_point (f i) \<and> (\<forall>j\<le>i . p \<le> x \<up> (?n-i) ; f i \<and> f i \<le> x \<up> (i-j) ; f j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>Suc n. is_point (if i = Suc n then r else f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; (if i = Suc n then r else f i) \<and> (if i = Suc n then r else f i) \<le> power.power 1' (;) x (i - j) ; (if j = Suc n then r else f j))

goal (1 subgoal):
 1. \<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>Suc n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<le> card {p. is_point p} \<longrightarrow> (\<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<le>card {p. is_point p}. \<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<le>card {p. is_point p}. \<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
[PROOF STEP]
obtain f where 8: "\<forall>i\<le>?n . is_point (f i) \<and> (\<forall>j\<le>i . p \<le> x \<up> (?n-i) ; f i \<and> f i \<le> x \<up> (i-j) ; f j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<le>card {p. is_point p}. \<exists>f. \<forall>i\<le>n. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal (1 subgoal):
 1. (\<And>f. \<forall>i\<le>card {p. is_point p}. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>card {p. is_point p}. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
let ?A = "{ k . k\<le>?n }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "f ` ?A \<subseteq> { p . is_point p }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {k. k \<le> card {p. is_point p}} \<subseteq> {p. is_point p}
[PROOF STEP]
using 8
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>card {p. is_point p}. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)

goal (1 subgoal):
 1. f ` {k. k \<le> card {p. is_point p}} \<subseteq> {p. is_point p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` {k. k \<le> card {p. is_point p}} \<subseteq> {p. is_point p}

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "card (f ` ?A) \<le> ?n"
[PROOF STATE]
proof (prove)
using this:
f ` {k. k \<le> card {p. is_point p}} \<subseteq> {p. is_point p}

goal (1 subgoal):
 1. card (f ` {k. k \<le> card {p. is_point p}}) \<le> card {p. is_point p}
[PROOF STEP]
by (simp add: card_mono)
[PROOF STATE]
proof (state)
this:
card (f ` {k. k \<le> card {p. is_point p}}) \<le> card {p. is_point p}

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "\<not> inj_on f ?A"
[PROOF STATE]
proof (prove)
using this:
card (f ` {k. k \<le> card {p. is_point p}}) \<le> card {p. is_point p}

goal (1 subgoal):
 1. \<not> inj_on f {k. k \<le> card {p. is_point p}}
[PROOF STEP]
by (simp add: pigeonhole)
[PROOF STATE]
proof (state)
this:
\<not> inj_on f {k. k \<le> card {p. is_point p}}

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on f {k. k \<le> card {p. is_point p}}
[PROOF STEP]
obtain i j where 9: "i \<le> ?n \<and> j \<le> ?n \<and> i \<noteq> j \<and> f i = f j"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on f {k. k \<le> card {p. is_point p}}

goal (1 subgoal):
 1. (\<And>i j. i \<le> card {p. is_point p} \<and> j \<le> card {p. is_point p} \<and> i \<noteq> j \<and> f i = f j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) inj_on_def mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
i \<le> card {p. is_point p} \<and> j \<le> card {p. is_point p} \<and> i \<noteq> j \<and> f i = f j

goal (1 subgoal):
 1. power.power 1' (;) x (card {p. is_point p}) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
apply (cases "i < j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < j \<Longrightarrow> False
 2. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
using 8 9
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>card {p. is_point p}. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
i \<le> card {p. is_point p} \<and> j \<le> card {p. is_point p} \<and> i \<noteq> j \<and> f i = f j

goal (2 subgoals):
 1. i < j \<Longrightarrow> False
 2. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
apply (metis Suc_diff_le Suc_leI assms diff_Suc_Suc order_less_imp_le
                            point_loop_not_acyclic)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
using 8 9
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>card {p. is_point p}. is_point (f i) \<and> (\<forall>j\<le>i. p \<le> power.power 1' (;) x (card {p. is_point p} - i) ; f i \<and> f i \<le> power.power 1' (;) x (i - j) ; f j)
i \<le> card {p. is_point p} \<and> j \<le> card {p. is_point p} \<and> i \<noteq> j \<and> f i = f j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
by (metis assms neqE point_loop_not_acyclic Suc_diff_le Suc_leI assms diff_Suc_Suc
                        order_less_imp_le)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
power.power 1' (;) x (card {p. is_point p}) = 0

goal (1 subgoal):
 1. \<exists>n. power.power 1' (;) x (Suc n) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
power.power 1' (;) x (card {p. is_point p}) = 0

goal (1 subgoal):
 1. \<exists>n. power.power 1' (;) x (Suc n) = 0
[PROOF STEP]
by (metis annir power.simps(2))
[PROOF STATE]
proof (state)
this:
\<exists>n. power.power 1' (;) x (Suc n) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_regressively_finite:
  assumes "is_acyclic x"
    shows "regressively_finite x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regressively_finite x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. is_vector v \<and> v \<le> x\<^sup>T ; v \<longrightarrow> v = 0
[PROOF STEP]
have "is_acyclic (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acyclic (x\<^sup>T)
[PROOF STEP]
using assms acyclic_trans' compl_le_swap1 order_trans star_ref
[PROOF STATE]
proof (prove)
using this:
is_acyclic x
is_acyclic ?x \<Longrightarrow> ?x\<^sup>\<star> \<le> - ?x\<^sup>T\<^sup>+
?y \<le> - ?x \<Longrightarrow> ?x \<le> - ?y
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
reflexive (?x\<^sup>\<star>)

goal (1 subgoal):
 1. is_acyclic (x\<^sup>T)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_acyclic (x\<^sup>T)

goal (1 subgoal):
 1. \<And>v. is_vector v \<and> v \<le> x\<^sup>T ; v \<longrightarrow> v = 0
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
is_acyclic (x\<^sup>T)
[PROOF STEP]
obtain n where 1: "x\<^sup>T \<up> Suc n = 0"
[PROOF STATE]
proof (prove)
using this:
is_acyclic (x\<^sup>T)

goal (1 subgoal):
 1. (\<And>n. power.power 1' (;) (x\<^sup>T) (Suc n) = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using acyclic_power_vanishes
[PROOF STATE]
proof (prove)
using this:
is_acyclic (x\<^sup>T)
is_acyclic ?x \<Longrightarrow> \<exists>n. power.power 1' (;) ?x (Suc n) = 0

goal (1 subgoal):
 1. (\<And>n. power.power 1' (;) (x\<^sup>T) (Suc n) = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
power.power 1' (;) (x\<^sup>T) (Suc n) = 0

goal (1 subgoal):
 1. \<And>v. is_vector v \<and> v \<le> x\<^sup>T ; v \<longrightarrow> v = 0
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. is_vector v \<and> v \<le> x\<^sup>T ; v \<longrightarrow> v = 0
[PROOF STEP]
show "is_vector v \<and> v \<le> x\<^sup>T;v \<longrightarrow> v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_vector v \<and> v \<le> x\<^sup>T ; v \<longrightarrow> v = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_vector v \<and> v \<le> x\<^sup>T ; v \<Longrightarrow> v = 0
[PROOF STEP]
assume 2: "is_vector v \<and> v \<le> x\<^sup>T;v"
[PROOF STATE]
proof (state)
this:
is_vector v \<and> v \<le> x\<^sup>T ; v

goal (1 subgoal):
 1. is_vector v \<and> v \<le> x\<^sup>T ; v \<Longrightarrow> v = 0
[PROOF STEP]
have "v \<le> x\<^sup>T \<up> Suc n ; v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<le> power.power 1' (;) (x\<^sup>T) (Suc zero_class.zero) ; v
 2. \<And>n. v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v \<Longrightarrow> v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. v \<le> power.power 1' (;) (x\<^sup>T) (Suc zero_class.zero) ; v
 2. \<And>n. v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v \<Longrightarrow> v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<le> power.power 1' (;) (x\<^sup>T) (Suc zero_class.zero) ; v
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
is_vector v \<and> v \<le> x\<^sup>T ; v

goal (1 subgoal):
 1. v \<le> power.power 1' (;) (x\<^sup>T) (Suc zero_class.zero) ; v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<le> power.power 1' (;) (x\<^sup>T) (Suc zero_class.zero) ; v

goal (1 subgoal):
 1. \<And>n. v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v \<Longrightarrow> v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v \<Longrightarrow> v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v

goal (1 subgoal):
 1. \<And>n. v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v \<Longrightarrow> v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
hence "x\<^sup>T ; v \<le> x\<^sup>T \<up> Suc (Suc n) ; v"
[PROOF STATE]
proof (prove)
using this:
v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v

goal (1 subgoal):
 1. x\<^sup>T ; v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
by (simp add: comp_assoc mult_isol)
[PROOF STATE]
proof (state)
this:
x\<^sup>T ; v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v

goal (1 subgoal):
 1. \<And>n. v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v \<Longrightarrow> v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T ; v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v

goal (1 subgoal):
 1. v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
using 2 dual_order.trans
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T ; v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
is_vector v \<and> v \<le> x\<^sup>T ; v
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<le> power.power 1' (;) (x\<^sup>T) (Suc (Suc n)) ; v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v

goal (1 subgoal):
 1. is_vector v \<and> v \<le> x\<^sup>T ; v \<Longrightarrow> v = 0
[PROOF STEP]
thus "v = 0"
[PROOF STATE]
proof (prove)
using this:
v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v

goal (1 subgoal):
 1. v = 0
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
v \<le> power.power 1' (;) (x\<^sup>T) (Suc n) ; v
power.power 1' (;) (x\<^sup>T) (Suc n) = 0

goal (1 subgoal):
 1. v = 0
[PROOF STEP]
by (simp add: le_bot)
[PROOF STATE]
proof (state)
this:
v = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_vector v \<and> v \<le> x\<^sup>T ; v \<longrightarrow> v = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_is_regressively_finite:
  "is_acyclic x \<longleftrightarrow> regressively_finite x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acyclic x = regressively_finite x
[PROOF STEP]
using acyclic_regressively_finite regressively_finite_acyclic
[PROOF STATE]
proof (prove)
using this:
is_acyclic ?x \<Longrightarrow> regressively_finite ?x
regressively_finite ?x \<Longrightarrow> is_acyclic ?x

goal (1 subgoal):
 1. is_acyclic x = regressively_finite x
[PROOF STEP]
by blast


[STATEMENT]
lemma atoms_finite[simp,intro!]: "finite (atoms F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (atoms F)
[PROOF STEP]
by(induction F; simp)


[STATEMENT]
lemma atoms_are_subformulae: "Atom ` atoms F \<subseteq> set (subformulae F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Atom ` atoms F \<subseteq> set (subformulae F)
[PROOF STEP]
by (induction F) auto


[STATEMENT]
lemma subsubformulae: "G \<in> set (subformulae F) \<Longrightarrow> H \<in> set (subformulae G) \<Longrightarrow> H \<in> set (subformulae F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<in> set (subformulae F); H \<in> set (subformulae G)\<rbrakk> \<Longrightarrow> H \<in> set (subformulae F)
[PROOF STEP]
by(induction F; force)


[STATEMENT]
lemma subformula_atoms: "G \<in> set (subformulae F) \<Longrightarrow> atoms G \<subseteq> atoms F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<in> set (subformulae F) \<Longrightarrow> atoms G \<subseteq> atoms F
[PROOF STEP]
by(induction F) auto


[STATEMENT]
lemma subformulae_self[simp,intro]: "F \<in> set (subformulae F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> set (subformulae F)
[PROOF STEP]
by(induction F; simp)


[STATEMENT]
lemma subformulas_in_subformulas:
  "G \<^bold>\<and> H \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F) \<and> H \<in> set (subformulae F)"
  "G \<^bold>\<or> H \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F) \<and> H \<in> set (subformulae F)"
  "G \<^bold>\<rightarrow> H \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F) \<and> H \<in> set (subformulae F)"
  "\<^bold>\<not> G \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((G \<^bold>\<and> H \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F) \<and> H \<in> set (subformulae F)) &&& (G \<^bold>\<or> H \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F) \<and> H \<in> set (subformulae F))) &&& (G \<^bold>\<rightarrow> H \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F) \<and> H \<in> set (subformulae F)) &&& (\<^bold>\<not> G \<in> set (subformulae F) \<Longrightarrow> G \<in> set (subformulae F))
[PROOF STEP]
by(fastforce elim: subsubformulae)+


[STATEMENT]
lemma length_subformulae: "length (subformulae F) = size F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (subformulae F) = size F
[PROOF STEP]
by(induction F; simp)


[STATEMENT]
lemma top_atoms_simp[simp]: "atoms \<top> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms \<top> = {}
[PROOF STEP]
unfolding Top_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms (\<bottom> \<^bold>\<rightarrow> \<bottom>) = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma atoms_BigAnd[simp]: "atoms (\<^bold>\<And>Fs) = \<Union>(atoms ` set Fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms \<^bold>\<And>Fs = \<Union> (atoms ` set Fs)
[PROOF STEP]
by(induction Fs; simp)


[STATEMENT]
lemma pn_atoms_atoms: "atoms F = fst (pn_atoms F) \<union> snd (pn_atoms F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms F = fst (pn_atoms F) \<union> snd (pn_atoms F)
[PROOF STEP]
by(induction F) (auto simp add: prod_unions_def split: prod.splits)


[STATEMENT]
lemma simplify_consts_size_le: "size (simplify_consts F) \<le> size F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (simplify_consts F) \<le> size F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. size (simplify_consts F) \<le> size F
[PROOF STEP]
have [simp]: "Suc (Suc 0) \<le> size F + size G" for F G :: "'a formula"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Suc 0) \<le> size F + size G
[PROOF STEP]
by(cases F; cases G; simp)
[PROOF STATE]
proof (state)
this:
Suc (Suc 0) \<le> size ?F + size ?G

goal (1 subgoal):
 1. size (simplify_consts F) \<le> size F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (simplify_consts F) \<le> size F
[PROOF STEP]
by(induction F; fastforce simp add: Let_def isstop_def Top_def split: formula.splits)
[PROOF STATE]
proof (state)
this:
size (simplify_consts F) \<le> size F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simplify_const: "atoms F = {} \<Longrightarrow> isstop (simplify_consts F) \<or> (simplify_consts F) = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms F = {} \<Longrightarrow> isstop (simplify_consts F) \<or> simplify_consts F = \<bottom>
[PROOF STEP]
by(induction F; fastforce simp add: Let_def isstop_def Top_def split: formula.splits)