[STATEMENT]
lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if xc then [xab] else [an]) = [if xc then xab else an]
[PROOF STEP]
by auto

\<comment> \<open>note -- \<open>if_Cons\<close> can cause blowup in the size, if \<open>p\<close> is complex, so make a simproc\<close>


[STATEMENT]
lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if p then x # xs else y # ys) = (if p then x else y) # (if p then xs else ys)
[PROOF STEP]
by auto


[STATEMENT]
lemma list_of_false:
  "True \<notin> set xs \<Longrightarrow> xs = replicate (length xs) False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<notin> set xs \<Longrightarrow> xs = replicate (length xs) False
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma list_all2_induct [consumes 1, case_names Nil Cons]:
  assumes lall: "list_all2 Q xs ys"
  and     nilr: "P [] []"
  and    consr: "\<And>x xs y ys. \<lbrakk>list_all2 Q xs ys; Q x y; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)"
  shows  "P xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
using lall
[PROOF STATE]
proof (prove)
using this:
list_all2 Q xs ys

goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
proof (induct rule: list_induct2 [OF list_all2_lengthD [OF lall]])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list_all2 Q [] [] \<Longrightarrow> P [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
list_all2 Q [] []

goal (2 subgoals):
 1. list_all2 Q [] [] \<Longrightarrow> P [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all2 Q [] []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_all2 Q [] []

goal (1 subgoal):
 1. P [] []
[PROOF STEP]
by auto fact+
[PROOF STATE]
proof (state)
this:
P [] []

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)
[PROOF STEP]
case (2 x xs y ys)
[PROOF STATE]
proof (state)
this:
length xs = length ys
list_all2 Q xs ys \<Longrightarrow> P xs ys
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (x # xs) (y # ys)
[PROOF STEP]
proof (rule consr)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. list_all2 Q xs ys
 2. Q x y
 3. P xs ys
[PROOF STEP]
from "2.prems"
[PROOF STATE]
proof (chain)
picking this:
list_all2 Q (x # xs) (y # ys)
[PROOF STEP]
show "list_all2 Q xs ys" and "Q x y"
[PROOF STATE]
proof (prove)
using this:
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. list_all2 Q xs ys &&& Q x y
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
list_all2 Q xs ys
Q x y

goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all2 Q xs ys
Q x y
[PROOF STEP]
show "P xs ys"
[PROOF STATE]
proof (prove)
using this:
list_all2 Q xs ys
Q x y

goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
by (intro "2.hyps")
[PROOF STATE]
proof (state)
this:
P xs ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (x # xs) (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma replicate_minus:
  "k < n \<Longrightarrow> replicate n False = replicate (n - k) False @ replicate k False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> replicate n False = replicate (n - k) False @ replicate k False
[PROOF STEP]
by (subst replicate_add [symmetric]) simp


[STATEMENT]
lemma cart_singleton_empty:
  "(S \<times> {e} = {}) = (S = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S \<times> {e} = {}) = (S = {})
[PROOF STEP]
by blast


[STATEMENT]
lemma MinI:
  assumes fa: "finite A"
  and     ne: "A \<noteq> {}"
  and     xv: "m \<in> A"
  and    min: "\<forall>y \<in> A. m \<le> y"
  shows "Min A = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min A = m
[PROOF STEP]
using fa ne xv min
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
m \<in> A
\<forall>y\<in>A. m \<le> y

goal (1 subgoal):
 1. Min A = m
[PROOF STEP]
proof (induct A arbitrary: m rule: finite_ne_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x m. \<lbrakk>m \<in> {x}; Ball {x} ((\<le>) m)\<rbrakk> \<Longrightarrow> Min {x} = m
 2. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m
[PROOF STEP]
case singleton
[PROOF STATE]
proof (state)
this:
m \<in> {x_}
\<forall>a\<in>{x_}. m \<le> a

goal (2 subgoals):
 1. \<And>x m. \<lbrakk>m \<in> {x}; Ball {x} ((\<le>) m)\<rbrakk> \<Longrightarrow> Min {x} = m
 2. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> {x_}
\<forall>a\<in>{x_}. m \<le> a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m \<in> {x_}
\<forall>a\<in>{x_}. m \<le> a

goal (1 subgoal):
 1. Min {x_} = m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min {x_} = m

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m
[PROOF STEP]
case (insert y F)
[PROOF STATE]
proof (state)
this:
finite F
F \<noteq> {}
y \<notin> F
\<lbrakk>?m \<in> F; \<forall>a\<in>F. ?m \<le> a\<rbrakk> \<Longrightarrow> Min F = ?m
m \<in> insert y F
\<forall>a\<in>insert y F. m \<le> a

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m
[PROOF STEP]
from insert.prems
[PROOF STATE]
proof (chain)
picking this:
m \<in> insert y F
\<forall>a\<in>insert y F. m \<le> a
[PROOF STEP]
have yx: "m \<le> y" and fx: "\<forall>y \<in> F. m \<le> y"
[PROOF STATE]
proof (prove)
using this:
m \<in> insert y F
\<forall>a\<in>insert y F. m \<le> a

goal (1 subgoal):
 1. m \<le> y &&& \<forall>y\<in>F. m \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<le> y
\<forall>y\<in>F. m \<le> y

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m
[PROOF STEP]
have "m \<in> insert y F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> insert y F
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
m \<in> insert y F

goal (1 subgoal):
 1. \<And>x F m. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>m. \<lbrakk>m \<in> F; Ball F ((\<le>) m)\<rbrakk> \<Longrightarrow> Min F = m; m \<in> insert x F; Ball (insert x F) ((\<le>) m)\<rbrakk> \<Longrightarrow> Min (insert x F) = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> insert y F
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m \<in> insert y F

goal (1 subgoal):
 1. Min (insert y F) = m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = y \<Longrightarrow> Min (insert y F) = m
 2. m \<in> F \<Longrightarrow> Min (insert y F) = m
[PROOF STEP]
assume mv: "m = y"
[PROOF STATE]
proof (state)
this:
m = y

goal (2 subgoals):
 1. m = y \<Longrightarrow> Min (insert y F) = m
 2. m \<in> F \<Longrightarrow> Min (insert y F) = m
[PROOF STEP]
have mlt: "m \<le> Min F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> Min F
[PROOF STEP]
by (rule iffD2 [OF Min_ge_iff [OF insert.hyps(1) insert.hyps(2)] fx])
[PROOF STATE]
proof (state)
this:
m \<le> Min F

goal (2 subgoals):
 1. m = y \<Longrightarrow> Min (insert y F) = m
 2. m \<in> F \<Longrightarrow> Min (insert y F) = m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (insert y F) = m
[PROOF STEP]
apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min y (Min F) = m
[PROOF STEP]
apply (subst mv [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min m (Min F) = m
[PROOF STEP]
apply (auto simp: min_def mlt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Min (insert y F) = m

goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m
[PROOF STEP]
assume "m \<in> F"
[PROOF STATE]
proof (state)
this:
m \<in> F

goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> F
[PROOF STEP]
have mf: "Min F = m"
[PROOF STATE]
proof (prove)
using this:
m \<in> F

goal (1 subgoal):
 1. Min F = m
[PROOF STEP]
by (rule insert.hyps(4) [OF _ fx])
[PROOF STATE]
proof (state)
this:
Min F = m

goal (1 subgoal):
 1. m \<in> F \<Longrightarrow> Min (insert y F) = m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (insert y F) = m
[PROOF STEP]
apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min y (Min F) = m
[PROOF STEP]
apply (subst mf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min y m = m
[PROOF STEP]
apply (rule iffD2 [OF _ yx])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (min y m = m) = (m \<le> y)
[PROOF STEP]
apply (auto simp: min_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Min (insert y F) = m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (insert y F) = m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ^ numeral k = a * a ^ pred_numeral k
[PROOF STEP]
by (simp add: numeral_eq_Suc)


[STATEMENT]
lemma funpow_numeral [simp]: "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ^^ numeral k = f \<circ> f ^^ pred_numeral k
[PROOF STEP]
by (simp add: numeral_eq_Suc)


[STATEMENT]
lemma funpow_minus_simp: "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)
[PROOF STEP]
by (auto dest: gr0_implies_Suc)


[STATEMENT]
lemma rco_alt: "(f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ((f \<circ> g) ^^ n \<circ> f) x = (f \<circ> (g \<circ> f) ^^ n) x
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. ((f \<circ> g) ^^ 0 \<circ> f) x = (f \<circ> (g \<circ> f) ^^ 0) x
 2. \<And>n x. (\<And>x. ((f \<circ> g) ^^ n \<circ> f) x = (f \<circ> (g \<circ> f) ^^ n) x) \<Longrightarrow> ((f \<circ> g) ^^ Suc n \<circ> f) x = (f \<circ> (g \<circ> f) ^^ Suc n) x
[PROOF STEP]
apply (simp_all add: o_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma union_sub:
  "\<lbrakk>B \<subseteq> A; C \<subseteq> B\<rbrakk> \<Longrightarrow> (A - B) \<union> (B - C) = (A - C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B \<subseteq> A; C \<subseteq> B\<rbrakk> \<Longrightarrow> A - B \<union> (B - C) = A - C
[PROOF STEP]
by fastforce


[STATEMENT]
lemma insert_sub:
  "x \<in> xs \<Longrightarrow> (insert x (xs - ys)) = (xs - (ys - {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> xs \<Longrightarrow> insert x (xs - ys) = xs - (ys - {x})
[PROOF STEP]
by blast


[STATEMENT]
lemma ran_upd:
  "\<lbrakk> inj_on f (dom f); f y = Some z \<rbrakk> \<Longrightarrow> ran (\<lambda>x. if x = y then None else f x) = ran f - {z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> ran (\<lambda>x. if x = y then None else f x) = ran f - {z}
[PROOF STEP]
unfolding ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> {b. \<exists>a. (if a = y then None else f a) = Some b} = {b. \<exists>a. f a = Some b} - {z}
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> (x \<in> {b. \<exists>a. (if a = y then None else f a) = Some b}) = (x \<in> {b. \<exists>a. f a = Some b} - {z})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> (\<exists>a. a \<noteq> y \<and> (a \<noteq> y \<longrightarrow> f a = Some x)) = ((\<exists>a. f a = Some x) \<and> x \<noteq> z)
[PROOF STEP]
by (metis domI inj_on_eq_iff option.sel)


[STATEMENT]
lemma if_apply_def2:
  "(if P then F else G) = (\<lambda>x. (P \<longrightarrow> F x) \<and> (\<not> P \<longrightarrow> G x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if P then F else G) = (\<lambda>x. (P \<longrightarrow> F x) \<and> (\<not> P \<longrightarrow> G x))
[PROOF STEP]
by simp


[STATEMENT]
lemma case_bool_If:
  "case_bool P Q b = (if b then P else Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case b of True \<Rightarrow> P | False \<Rightarrow> Q) = (if b then P else Q)
[PROOF STEP]
by simp


[STATEMENT]
lemma if_f:
  "(if a then f b else f c) = f (if a then b else c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a then f b else f c) = f (if a then b else c)
[PROOF STEP]
by simp


[STATEMENT]
lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (if p then xs else ys) = (if p then size xs else size ys)
[PROOF STEP]
by (fact if_distrib)


[STATEMENT]
lemma if_Not_x: "(if p then \<not> x else x) = (p = (\<not> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if p then \<not> x else x) = (p = (\<not> x))
[PROOF STEP]
by auto


[STATEMENT]
lemma if_x_Not: "(if p then x else \<not> x) = (p = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if p then x else \<not> x) = (p = x)
[PROOF STEP]
by auto


[STATEMENT]
lemma if_same_and: "(If p x y \<and> If p u v) = (if p then x \<and> u else y \<and> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if p then x else y) \<and> (if p then u else v)) = (if p then x \<and> u else y \<and> v)
[PROOF STEP]
by auto


[STATEMENT]
lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = u else y = v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if p then x else y) = (if p then u else v)) = (if p then x = u else y = v)
[PROOF STEP]
by auto


[STATEMENT]
lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if p then x else y) = (\<not> (if p then u else v))) = (if p then x = (\<not> u) else y = (\<not> v))
[PROOF STEP]
by auto


[STATEMENT]
lemma the_elemI: "y = {x} \<Longrightarrow> the_elem y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = {x} \<Longrightarrow> the_elem y = x
[PROOF STEP]
by simp


[STATEMENT]
lemma nonemptyE: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> R) \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<noteq> {}; \<And>x. x \<in> S \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by auto


[STATEMENT]
lemma not_empty_eq:
  "(S \<noteq> {}) = (\<exists>x. x \<in> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S \<noteq> {}) = (\<exists>x. x \<in> S)
[PROOF STEP]
by auto


[STATEMENT]
lemma range_subset_lower:
  fixes c :: "'a ::linorder"
  shows "\<lbrakk> {a..b} \<subseteq> {c..d}; x \<in> {a..b} \<rbrakk> \<Longrightarrow> c \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}\<rbrakk> \<Longrightarrow> c \<le> a
[PROOF STEP]
apply (frule (1) subsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}\<rbrakk> \<Longrightarrow> c \<le> a
[PROOF STEP]
apply (rule classical)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}; \<not> c \<le> a\<rbrakk> \<Longrightarrow> c \<le> a
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma range_subset_upper:
  fixes c :: "'a ::linorder"
  shows "\<lbrakk> {a..b} \<subseteq> {c..d}; x \<in> {a..b} \<rbrakk> \<Longrightarrow> b \<le> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}\<rbrakk> \<Longrightarrow> b \<le> d
[PROOF STEP]
apply (frule (1) subsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}\<rbrakk> \<Longrightarrow> b \<le> d
[PROOF STEP]
apply (rule classical)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}; \<not> b \<le> d\<rbrakk> \<Longrightarrow> b \<le> d
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma range_subset_eq:
  fixes a::"'a::linorder"
  assumes non_empty: "a \<le> b"
  shows "({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d)
[PROOF STEP]
apply (insert non_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> ({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> b; {a..b} \<subseteq> {c..d}\<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d
 2. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d}
[PROOF STEP]
apply (frule range_subset_lower [where x=a], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> b; {a..b} \<subseteq> {c..d}; c \<le> a\<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d
 2. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d}
[PROOF STEP]
apply (drule range_subset_upper [where x=a], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> b; c \<le> a; b \<le> d\<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d
 2. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma range_eq:
  fixes a::"'a::linorder"
  assumes non_empty: "a \<le> b"
  shows "({a..b} = {c..d}) = (a = c \<and> b = d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a..b} = {c..d}) = (a = c \<and> b = d)
[PROOF STEP]
by (metis atLeastatMost_subset_iff eq_iff non_empty)


[STATEMENT]
lemma range_strict_subset_eq:
  fixes a::"'a::linorder"
  assumes non_empty: "a \<le> b"
  shows "({a..b} \<subset> {c..d}) = (c \<le> a \<and> b \<le> d \<and> (a = c \<longrightarrow> b \<noteq> d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a..b} \<subset> {c..d}) = (c \<le> a \<and> b \<le> d \<and> (a = c \<longrightarrow> b \<noteq> d))
[PROOF STEP]
apply (insert non_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> ({a..b} \<subset> {c..d}) = (c \<le> a \<and> b \<le> d \<and> (a = c \<longrightarrow> b \<noteq> d))
[PROOF STEP]
apply (subst psubset_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> ({a..b} \<subseteq> {c..d} \<and> {a..b} \<noteq> {c..d}) = (c \<le> a \<and> b \<le> d \<and> (a = c \<longrightarrow> b \<noteq> d))
[PROOF STEP]
apply (subst range_subset_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> ((c \<le> a \<and> b \<le> d) \<and> {a..b} \<noteq> {c..d}) = (c \<le> a \<and> b \<le> d \<and> (a = c \<longrightarrow> b \<noteq> d))
[PROOF STEP]
apply (subst range_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> ((c \<le> a \<and> b \<le> d) \<and> \<not> (a = c \<and> b = d)) = (c \<le> a \<and> b \<le> d \<and> (a = c \<longrightarrow> b \<noteq> d))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma range_subsetI:
  fixes x :: "'a :: order"
  assumes xX: "X \<le> x"
  and     yY: "y \<le> Y"
  shows   "{x .. y} \<subseteq> {X .. Y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x..y} \<subseteq> {X..Y}
[PROOF STEP]
using xX yY
[PROOF STATE]
proof (prove)
using this:
X \<le> x
y \<le> Y

goal (1 subgoal):
 1. {x..y} \<subseteq> {X..Y}
[PROOF STEP]
by auto


[STATEMENT]
lemma set_False [simp]:
  "(set bs \<subseteq> {False}) = (True \<notin> set bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set bs \<subseteq> {False}) = (True \<notin> set bs)
[PROOF STEP]
by auto


[STATEMENT]
lemma int_not_emptyD:
  "A \<inter> B \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B
[PROOF STEP]
by (erule contrapos_np, clarsimp simp: disjoint_iff_not_equal)


[STATEMENT]
lemma sum_map_simps[simp]:
  "sum_map f g (Inl v) = Inl (f v)"
  "sum_map f g (Inr w) = Inr (g w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_map f g (Inl v) = Inl (f v) &&& sum_map f g (Inr w) = Inr (g w)
[PROOF STEP]
by (simp add: sum_map_def)+


[STATEMENT]
lemma if_Some_None_eq_None:
  "((if P then Some v else None) = None) = (\<not> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if P then Some v else None) = None) = (\<not> P)
[PROOF STEP]
by simp


[STATEMENT]
lemma CollectPairFalse [iff]:
  "{(a,b). False} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a, b). False} = {}
[PROOF STEP]
by (simp add: split_def)


[STATEMENT]
lemma if_conj_dist:
  "((if b then w else x) \<and> (if b then y else z) \<and> X) =
  ((if b then w \<and> y else x \<and> z) \<and> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if b then w else x) \<and> (if b then y else z) \<and> X) = ((if b then w \<and> y else x \<and> z) \<and> X)
[PROOF STEP]
by simp


[STATEMENT]
lemma if_P_True1:
  "Q \<Longrightarrow> (if P then True else Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<Longrightarrow> if P then True else Q
[PROOF STEP]
by simp


[STATEMENT]
lemma if_P_True2:
  "Q \<Longrightarrow> (if P then Q else True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<Longrightarrow> if P then Q else True
[PROOF STEP]
by simp


[STATEMENT]
lemma nat_min_simps:
  "(a::nat) \<le> b \<Longrightarrow> min b a = a"
  "a \<le> b \<Longrightarrow> min a b = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> min b a = a) &&& (a \<le> b \<Longrightarrow> min a b = a)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
  for a b c d :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b = c + d \<Longrightarrow> c \<le> a \<and> b \<le> d \<or> a \<le> c \<and> d \<le> b
[PROOF STEP]
by arith


[STATEMENT]
lemma iszero_minus:
  \<open>iszero (- z) \<longleftrightarrow> iszero z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iszero (- z) = iszero z
[PROOF STEP]
by (simp add: iszero_def)


[STATEMENT]
lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c"
  for a b c :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a - b \<le> c) = (a \<le> b + c)
[PROOF STEP]
by arith


[STATEMENT]
lemma zless2: "0 < (2 :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2
[PROOF STEP]
by (fact zero_less_numeral)


[STATEMENT]
lemma zless2p: "0 < (2 ^ n :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ n
[PROOF STEP]
by arith


[STATEMENT]
lemma zle2p: "0 \<le> (2 ^ n :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 2 ^ n
[PROOF STEP]
by arith


[STATEMENT]
lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>m. n = Suc m \<and> (m = k \<or> P m)) = (n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m))
[PROOF STEP]
by auto


[STATEMENT]
lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)
[PROOF STEP]
by (auto dest: gr0_implies_Suc)


[STATEMENT]
lemma n2s_ths:
  \<open>2 + n = Suc (Suc n)\<close>
  \<open>n + 2 = Suc (Suc n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 + n = Suc (Suc n) &&& n + 2 = Suc (Suc n)
[PROOF STEP]
by (fact add_2_eq_Suc add_2_eq_Suc')+


[STATEMENT]
lemma s2n_ths:
  \<open>Suc (Suc n) = 2 + n\<close>
  \<open>Suc (Suc n) = n + 2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Suc n) = 2 + n &&& Suc (Suc n) = n + 2
[PROOF STEP]
by simp_all


[STATEMENT]
lemma gt_or_eq_0: "0 < y \<or> 0 = y"
  for y :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < y \<or> 0 = y
[PROOF STEP]
by arith


[STATEMENT]
lemma sum_imp_diff: "j = k + i \<Longrightarrow> j - i = k"
  for k :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = k + i \<Longrightarrow> j - i = k
[PROOF STEP]
by simp


[STATEMENT]
lemma le_diff_eq': "a \<le> c - b \<longleftrightarrow> b + a \<le> c"
  for a b c :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> c - b) = (b + a \<le> c)
[PROOF STEP]
by arith


[STATEMENT]
lemma less_diff_eq': "a < c - b \<longleftrightarrow> b + a < c"
  for a b c :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < c - b) = (b + a < c)
[PROOF STEP]
by arith


[STATEMENT]
lemma diff_less_eq': "a - b < c \<longleftrightarrow> a < b + c"
  for a b c :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a - b < c) = (a < b + c)
[PROOF STEP]
by arith


[STATEMENT]
lemma axxbyy: "a + m + m = b + n + n \<Longrightarrow> a = 0 \<or> a = 1 \<Longrightarrow> b = 0 \<or> b = 1 \<Longrightarrow> a = b \<and> m = n"
  for a b m n :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + m + m = b + n + n; a = 0 \<or> a = 1; b = 0 \<or> b = 1\<rbrakk> \<Longrightarrow> a = b \<and> m = n
[PROOF STEP]
by arith


[STATEMENT]
lemma minus_eq: "m - k = m \<longleftrightarrow> k = 0 \<or> m = 0"
  for k m :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m - k = m) = (k = 0 \<or> m = 0)
[PROOF STEP]
by arith


[STATEMENT]
lemma pl_pl_mm: "a + b = c + d \<Longrightarrow> a - c = d - b"
  for a b c d :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b = c + d \<Longrightarrow> a - c = d - b
[PROOF STEP]
by arith


[STATEMENT]
lemma less_le_mult': "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> (w + 1) * c \<le> b * c"
  for b c w :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> (w + 1) * c \<le> b * c
[PROOF STEP]
apply (rule mult_right_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w + 1 \<le> b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c
[PROOF STEP]
apply (rule zless_imp_add1_zle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w < b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c
[PROOF STEP]
apply (erule (1) mult_right_less_imp_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma less_le_mult: "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * c"
  for b c w :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w * c + c \<le> b * c
[PROOF STEP]
using less_le_mult' [of w c b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> (w + 1) * c \<le> b * c

goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w * c + c \<le> b * c
[PROOF STEP]
by (simp add: algebra_simps)


[STATEMENT]
lemma gen_minus: "0 < n \<Longrightarrow> f n = f (Suc (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> f n = f (Suc (n - 1))
[PROOF STEP]
by auto


[STATEMENT]
lemma mpl_lem: "j \<le> i \<Longrightarrow> k < j \<Longrightarrow> i - j + k < i"
  for i j k :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> i; k < j\<rbrakk> \<Longrightarrow> i - j + k < i
[PROOF STEP]
by arith


[STATEMENT]
lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
  for f l :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < f \<Longrightarrow> (f * l + (f - 1)) div f = l
[PROOF STEP]
by (rule div_nat_eqI) (simp_all)


[STATEMENT]
lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
  for f l :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < f \<Longrightarrow> (l * f + f - Suc 0) div f = l
[PROOF STEP]
apply (frule given_quot)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = l
[PROOF STEP]
apply (rule trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = ?s2
 2. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> ?s2 = l
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> ?s2 = l
 2. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = ?s2
[PROOF STEP]
apply (erule asm_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < f; (f * l + (f - 1)) div f = l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = (f * l + (f - 1)) div f
[PROOF STEP]
apply (rule_tac f="\<lambda>n. n div f" in arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < f; (f * l + (f - 1)) div f = l\<rbrakk> \<Longrightarrow> l * f + f - Suc 0 = f * l + (f - 1)
[PROOF STEP]
apply (simp add : ac_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma x_power_minus_1:
  fixes x :: "'a :: {ab_group_add, power, numeral, one}"
  shows "x + (2::'a) ^ n - (1::'a) = x + (2 ^ n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + (2::'a) ^ n - (1::'a) = x + ((2::'a) ^ n - (1::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma nat_diff_add:
  fixes i :: nat
  shows "\<lbrakk> i + j = k \<rbrakk> \<Longrightarrow> i = k - j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + j = k \<Longrightarrow> i = k - j
[PROOF STEP]
by arith


[STATEMENT]
lemma pow_2_gt: "n \<ge> 2 \<Longrightarrow> (2::int) < 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> n \<Longrightarrow> 2 < 2 ^ n
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma sum_to_zero:
  "(a :: 'a :: ring) + b = 0 \<Longrightarrow> a = (- b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b = (0::'a) \<Longrightarrow> a = - b
[PROOF STEP]
by (drule arg_cong[where f="\<lambda> x. x - a"], simp)


[STATEMENT]
lemma arith_is_1:
  "\<lbrakk> x \<le> Suc 0; x > 0 \<rbrakk> \<Longrightarrow> x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> Suc 0; 0 < x\<rbrakk> \<Longrightarrow> x = 1
[PROOF STEP]
by arith


[STATEMENT]
lemma suc_le_pow_2:
  "1 < (n::nat) \<Longrightarrow> Suc n < 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> Suc n < 2 ^ n
[PROOF STEP]
by (induct n; clarsimp)
     (case_tac "n = 1"; clarsimp)


[STATEMENT]
lemma nat_le_Suc_less_imp:
  "x < y \<Longrightarrow> x \<le> y - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> x \<le> y - Suc 0
[PROOF STEP]
by arith


[STATEMENT]
lemma power_sub_int:
  "\<lbrakk> m \<le> n; 0 < b \<rbrakk> \<Longrightarrow> b ^ n div b ^ m = (b ^ (n - m) :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> b ^ n div b ^ m = b ^ (n - m)
[PROOF STEP]
apply (subgoal_tac "\<exists>n'. n = m + n'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<le> n; 0 < b; \<exists>n'. n = m + n'\<rbrakk> \<Longrightarrow> b ^ n div b ^ m = b ^ (n - m)
 2. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> \<exists>n'. n = m + n'
[PROOF STEP]
apply (clarsimp simp: power_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> \<exists>n'. n = m + n'
[PROOF STEP]
apply (rule exI[where x="n - m"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> n = m + (n - m)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nat_Suc_less_le_imp:
  "(k::nat) < Suc n \<Longrightarrow> k \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < Suc n \<Longrightarrow> k \<le> n
[PROOF STEP]
by auto


[STATEMENT]
lemma nat_add_less_by_max:
  "\<lbrakk> (x::nat) \<le> xmax ; y < k - xmax \<rbrakk> \<Longrightarrow> x + y < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> xmax; y < k - xmax\<rbrakk> \<Longrightarrow> x + y < k
[PROOF STEP]
by simp


[STATEMENT]
lemma nat_le_Suc_less:
  "0 < y \<Longrightarrow> (x \<le> y - Suc 0) = (x < y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < y \<Longrightarrow> (x \<le> y - Suc 0) = (x < y)
[PROOF STEP]
by arith


[STATEMENT]
lemma nat_power_minus_less:
  "a < 2 ^ (x - n) \<Longrightarrow> (a :: nat) < 2 ^ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < 2 ^ (x - n) \<Longrightarrow> a < 2 ^ x
[PROOF STEP]
by (erule order_less_le_trans) simp


[STATEMENT]
lemma less_le_mult_nat':
  "w * c < b * c ==> 0 \<le> c ==> Suc w * c \<le> b * (c::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> Suc w * c \<le> b * c
[PROOF STEP]
apply (rule mult_right_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> Suc w \<le> b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c
[PROOF STEP]
apply (rule Suc_leI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w < b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c
[PROOF STEP]
apply (erule (1) mult_right_less_imp_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma less_le_mult_nat:
  \<open>0 < c \<and> w < b \<Longrightarrow> c + w * c \<le> b * c\<close> for b c w :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c \<and> w < b \<Longrightarrow> c + w * c \<le> b * c
[PROOF STEP]
using less_le_mult_nat' [of w c b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> Suc w * c \<le> b * c

goal (1 subgoal):
 1. 0 < c \<and> w < b \<Longrightarrow> c + w * c \<le> b * c
[PROOF STEP]
by simp


[STATEMENT]
lemma p_assoc_help:
  fixes p :: "'a::{ring,power,numeral,one}"
  shows "p + 2^sz - 1 = p + (2^sz - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p + (2::'a) ^ sz - (1::'a) = p + ((2::'a) ^ sz - (1::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma pow_mono_leq_imp_lt:
  "x \<le> y \<Longrightarrow> x < 2 ^ y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x < 2 ^ y
[PROOF STEP]
by (simp add: le_less_trans)


[STATEMENT]
lemma small_powers_of_2:
  "x \<ge> 3 \<Longrightarrow> x < 2 ^ (x - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 \<le> x \<Longrightarrow> x < 2 ^ (x - 1)
[PROOF STEP]
by (induct x; simp add: suc_le_pow_2)


[STATEMENT]
lemma nat_less_power_trans2:
  fixes n :: nat
  shows "\<lbrakk>n < 2 ^ (m - k); k \<le> m\<rbrakk> \<Longrightarrow> n * 2 ^ k  < 2 ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m\<rbrakk> \<Longrightarrow> n * 2 ^ k < 2 ^ m
[PROOF STEP]
by (subst mult.commute, erule (1) nat_less_power_trans)


[STATEMENT]
lemma nat_move_sub_le: "(a::nat) + b \<le> c \<Longrightarrow> a \<le> c - b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b \<le> c \<Longrightarrow> a \<le> c - b
[PROOF STEP]
by arith


[STATEMENT]
lemma plus_minus_one_rewrite:
  "v + (- 1 :: ('a :: {ring, one, uminus})) \<equiv> v - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v + - (1::'a) \<equiv> v - (1::'a)
[PROOF STEP]
by (simp add: field_simps)


[STATEMENT]
lemma Suc_0_lt_2p_len_of: "Suc 0 < 2 ^ LENGTH('a :: len)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 < 2 ^ LENGTH('a)
[PROOF STEP]
by (metis One_nat_def len_gt_0 lessI numeral_2_eq_2 one_less_power)


[STATEMENT]
lemma bin_rest_code: "i div 2 = drop_bit 1 i" for i :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i div 2 = drop_bit 1 i
[PROOF STEP]
by (simp add: drop_bit_eq_div)


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment> \<open>model found: axioms are consistent\<close>


[STATEMENT]
lemma "\<lfloor>D\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<box>x \<^bold>\<rightarrow> \<^bold>\<diamond>x) w)\<rfloor>
[PROOF STEP]
using A1a A1b A2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> (\<^bold>\<rightharpoondown>x) \<^bold>\<rightarrow> \<^bold>\<not>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<^bold>\<rightharpoondown>x)) w)\<rfloor>
\<lfloor>(\<lambda>w. universal (\<lambda>x xa. (\<P> x \<^bold>\<and> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v) \<^bold>\<rightarrow> \<P> xa) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<box>x \<^bold>\<rightarrow> \<^bold>\<diamond>x) w)\<rfloor>
[PROOF STEP]
by blast \<comment> \<open>axioms already imply \emph{D} axiom\<close>


[STATEMENT]
lemma GodDefsAreEquivalent: "\<lfloor>\<^bold>\<forall>x. G x \<^bold>\<leftrightarrow> G* x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) = (\<forall>xa. \<P> xa w = xa x w))\<rfloor>
[PROOF STEP]
using A1b
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<^bold>\<rightharpoondown>x)) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) = (\<forall>xa. \<P> xa w = xa x w))\<rfloor>
[PROOF STEP]
by fastforce


[STATEMENT]
theorem T1: "\<lfloor>\<^bold>\<forall>X. \<P> X \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<exists>\<^sup>E X\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsActB x) w)\<rfloor>
[PROOF STEP]
using A1a A2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> (\<^bold>\<rightharpoondown>x) \<^bold>\<rightarrow> \<^bold>\<not>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. universal (\<lambda>x xa. (\<P> x \<^bold>\<and> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v) \<^bold>\<rightarrow> \<P> xa) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsActB x) w)\<rfloor>
[PROOF STEP]
by blast  \<comment> \<open>positive properties are possibly instantiated\<close>


[STATEMENT]
theorem T3: "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
[PROOF STEP]
using T1 T2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsActB x) w)\<rfloor>
\<lfloor>\<P> (\<lambda>x w. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w)\<rfloor>

goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
[PROOF STEP]
by simp  \<comment> \<open>God exists possibly\<close>


[STATEMENT]
lemma A4b: "\<lfloor>\<^bold>\<forall>X. \<^bold>\<not>(\<P> X) \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>(\<P> X)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>\<P> x) w)\<rfloor>
[PROOF STEP]
using A1a A1b A4a
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> (\<^bold>\<rightharpoondown>x) \<^bold>\<rightarrow> \<^bold>\<not>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<^bold>\<rightharpoondown>x)) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<P> x) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>\<P> x) w)\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
lemma "\<lfloor>rigidPred \<P>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<lambda>x. \<lparr>\<P> x w\<rparr>) = (\<lambda>x. \<lparr>\<P> x v\<rparr>))
[PROOF STEP]
using A4a A4b
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<P> x) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<not>\<P> x) w)\<rfloor>

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<lambda>x. \<lparr>\<P> x w\<rparr>) = (\<lambda>x. \<lparr>\<P> x v\<rparr>))
[PROOF STEP]
by blast \<comment> \<open>@{term "\<P>"} is therefore rigid\<close>


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment> \<open>model found: so far all axioms A1-4 consistent\<close>


[STATEMENT]
theorem GodIsEssential: "\<lfloor>\<^bold>\<forall>x. G x \<^bold>\<rightarrow> (\<E> G x)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w))\<rfloor>
[PROOF STEP]
using A1b A4a
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<^bold>\<not>\<P> x \<^bold>\<rightarrow> \<P> (\<^bold>\<rightharpoondown>x)) w)\<rfloor>
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<P> x) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w))\<rfloor>
[PROOF STEP]
by metis


[STATEMENT]
theorem "\<lfloor>\<^bold>\<forall>x. G* x \<^bold>\<rightarrow> (\<E> G* x)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w = xa x w) \<longrightarrow> (\<forall>xa. \<P> xa w = xa x w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa v = xa x v) \<longrightarrow> xa x v)) w))\<rfloor>
[PROOF STEP]
using A4a
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<P> x) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. \<P> xa w = xa x w) \<longrightarrow> (\<forall>xa. \<P> xa w = xa x w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. \<P> xa v = xa x v) \<longrightarrow> xa x v)) w))\<rfloor>
[PROOF STEP]
by meson


[STATEMENT]
theorem "\<lfloor>\<^bold>\<forall>X Y z. (\<E> X z \<^bold>\<and> \<E> Y z) \<^bold>\<rightarrow> (X \<Rrightarrow> Y)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. universal (\<lambda>x xa. \<forall>xb. (x xb w \<and> (\<forall>xa. (xa xb \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v)) w)) \<and> xa xb w \<and> (\<forall>x. (x xb \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> xa xb \<^bold>\<rightarrow> x xb) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v)) w))\<rfloor>
[PROOF STEP]
by meson


[STATEMENT]
theorem EssencesCharacterizeCompletely: "\<lfloor>\<^bold>\<forall>X y. \<E> X y \<^bold>\<rightarrow> (X \<Rrightarrow> (id y))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> \<lfloor>\<^bold>\<forall>X y. \<E> X y \<^bold>\<rightarrow> (X \<Rrightarrow> (id y))\<rfloor>"
[PROOF STATE]
proof (state)
this:
\<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence "\<exists>w. \<not>(( \<^bold>\<forall>X y. \<E> X y \<^bold>\<rightarrow> X \<Rrightarrow> id y) w)"
[PROOF STATE]
proof (prove)
using this:
\<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>\<^sup>c\<^sup>s\<^sup>a\<^sup>t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>\<^sup>c\<^sup>s\<^sup>a\<^sup>t

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>\<^sup>c\<^sup>s\<^sup>a\<^sup>t
[PROOF STEP]
obtain w where "\<not>(( \<^bold>\<forall>X y. \<E> X y \<^bold>\<rightarrow> X \<Rrightarrow> id y) w)"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>\<^sup>c\<^sup>s\<^sup>a\<^sup>t

goal (1 subgoal):
 1. (\<And>w. \<not> (\<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence "(\<^bold>\<exists>X y. \<E> X y \<^bold>\<and> \<^bold>\<not>(X \<Rrightarrow> id y)) w"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)

goal (1 subgoal):
 1. \<exists>x xa. (x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x xa. (x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence "\<exists>X y. \<E> X y w \<and> (\<^bold>\<not>(X \<Rrightarrow> id y)) w"
[PROOF STATE]
proof (prove)
using this:
\<exists>x xa. (x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w

goal (1 subgoal):
 1. \<exists>X y. (X y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> X xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> X x v \<longrightarrow> x = y)) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>X y. (X y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> X xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> X x v \<longrightarrow> x = y)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>X y. (X y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> X xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> X x v \<longrightarrow> x = y)) w
[PROOF STEP]
obtain P where "\<exists>y. \<E> P y w \<and> (\<^bold>\<not>(P \<Rrightarrow> id y)) w"
[PROOF STATE]
proof (prove)
using this:
\<exists>X y. (X y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> X xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> X x v \<longrightarrow> x = y)) w

goal (1 subgoal):
 1. (\<And>P. \<exists>y. (P y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = y)) w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>y. (P y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = y)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. (P y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = y)) w
[PROOF STEP]
obtain a where 1: "\<E> P a w \<and> (\<^bold>\<not>(P \<Rrightarrow> id a)) w"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. (P y w \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = y)) w

goal (1 subgoal):
 1. (\<And>a. (P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence 2: "\<E> P a w"
[PROOF STATE]
proof (prove)
using this:
(P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w

goal (1 subgoal):
 1. P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)
[PROOF STEP]
by (rule conjunct1)
[PROOF STATE]
proof (state)
this:
P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
(P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w
[PROOF STEP]
have "(\<^bold>\<not>(P \<Rrightarrow> id a)) w"
[PROOF STATE]
proof (prove)
using this:
(P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)) \<and> (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w

goal (1 subgoal):
 1. (\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w
[PROOF STEP]
by (rule conjunct2)
[PROOF STATE]
proof (state)
this:
(\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence "\<exists>x. \<exists>z. w r x \<and>  existsAt z x \<and> P z x \<and> \<not>(a = z)"
[PROOF STATE]
proof (prove)
using this:
(\<^bold>\<not>\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> x = a)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>x. \<exists>z. w r x \<and> existsAt z x \<and> P z x \<and> (\<rightharpoondown>(=) a) z)\<rfloor>\<^sup>s\<^sup>a\<^sup>t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>x. \<exists>z. w r x \<and> existsAt z x \<and> P z x \<and> (\<rightharpoondown>(=) a) z)\<rfloor>\<^sup>s\<^sup>a\<^sup>t

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>(\<lambda>x. \<exists>z. w r x \<and> existsAt z x \<and> P z x \<and> (\<rightharpoondown>(=) a) z)\<rfloor>\<^sup>s\<^sup>a\<^sup>t
[PROOF STEP]
obtain w1 where "\<exists>z. w r w1 \<and>  existsAt z w1 \<and> P z w1 \<and> \<not>(a = z)"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>x. \<exists>z. w r x \<and> existsAt z x \<and> P z x \<and> (\<rightharpoondown>(=) a) z)\<rfloor>\<^sup>s\<^sup>a\<^sup>t

goal (1 subgoal):
 1. (\<And>w1. \<exists>z. w r w1 \<and> existsAt z w1 \<and> P z w1 \<and> (\<rightharpoondown>(=) a) z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>z. w r w1 \<and> existsAt z w1 \<and> P z w1 \<and> (\<rightharpoondown>(=) a) z

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z. w r w1 \<and> existsAt z w1 \<and> P z w1 \<and> (\<rightharpoondown>(=) a) z
[PROOF STEP]
obtain b where 3: "w r w1 \<and>  existsAt b w1 \<and> P b w1 \<and> \<not>(a = b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>z. w r w1 \<and> existsAt z w1 \<and> P z w1 \<and> (\<rightharpoondown>(=) a) z

goal (1 subgoal):
 1. (\<And>b. w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence "w r w1"
[PROOF STATE]
proof (prove)
using this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. w r w1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w r w1

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b
[PROOF STEP]
have "existsAt b w1"
[PROOF STATE]
proof (prove)
using this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. existsAt b w1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
existsAt b w1

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b
[PROOF STEP]
have "P b w1"
[PROOF STATE]
proof (prove)
using this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. P b w1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P b w1

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b
[PROOF STEP]
have 4: " \<not>(a = b)"
[PROOF STATE]
proof (prove)
using this:
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. (\<rightharpoondown>(=) a) b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)
[PROOF STEP]
have "P a w"
[PROOF STATE]
proof (prove)
using this:
P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)

goal (1 subgoal):
 1. P a w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P a w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)
[PROOF STEP]
have "\<forall>Y. Y a w \<longrightarrow> ((P \<Rrightarrow> Y) w)"
[PROOF STATE]
proof (prove)
using this:
P a w \<and> (\<forall>x. (x a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> P xa \<^bold>\<rightarrow> x xa) v)) w)

goal (1 subgoal):
 1. \<forall>Y. (Y a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. (existsAt x \<^bold>\<rightarrow> P x \<^bold>\<rightarrow> Y x) v)) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Y. (Y a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. (existsAt x \<^bold>\<rightarrow> P x \<^bold>\<rightarrow> Y x) v)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence "(\<^bold>\<rightharpoondown>(id b)) a w \<longrightarrow> (P \<Rrightarrow> (\<^bold>\<rightharpoondown>(id b))) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>Y. (Y a \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. (existsAt x \<^bold>\<rightarrow> P x \<^bold>\<rightarrow> Y x) v)) w

goal (1 subgoal):
 1. (\<rightharpoondown>(=) a) b \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
(\<rightharpoondown>(=) a) b \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
hence "\<not>(\<^bold>\<rightharpoondown>(id b)) a w \<or> ((P \<Rrightarrow> (\<^bold>\<rightharpoondown>(id b))) w)"
[PROOF STATE]
proof (prove)
using this:
(\<rightharpoondown>(=) a) b \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w

goal (1 subgoal):
 1. (\<rightharpoondown>\<rightharpoondown>(=) a) b \<or> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<rightharpoondown>\<rightharpoondown>(=) a) b \<or> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w

goal (1 subgoal):
 1. \<not> \<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<rightharpoondown>\<rightharpoondown>(=) a) b \<or> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(\<rightharpoondown>\<rightharpoondown>(=) a) b \<or> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<rightharpoondown>\<rightharpoondown>(=) a) b \<Longrightarrow> False
 2. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(\<^bold>\<rightharpoondown>(id b)) a w"
[PROOF STATE]
proof (state)
this:
(\<rightharpoondown>\<rightharpoondown>(=) a) b

goal (2 subgoals):
 1. (\<rightharpoondown>\<rightharpoondown>(=) a) b \<Longrightarrow> False
 2. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
hence "a = b"
[PROOF STATE]
proof (prove)
using this:
(\<rightharpoondown>\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. (\<rightharpoondown>\<rightharpoondown>(=) a) b \<Longrightarrow> False
 2. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. False
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
a = b
(\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
assume "((P \<Rrightarrow> (\<^bold>\<rightharpoondown>(id b))) w)"
[PROOF STATE]
proof (state)
this:
(\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>x. \<forall>z. (w r x \<and> existsAt z x \<and> P z x) \<longrightarrow> (\<^bold>\<rightharpoondown>(id b)) z x"
[PROOF STATE]
proof (prove)
using this:
(\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>x. \<forall>z. ((r) w \<^bold>\<and> existsAt z \<^bold>\<and> P z) x \<longrightarrow> (\<rightharpoondown>(=) z) b)\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>x. \<forall>z. ((r) w \<^bold>\<and> existsAt z \<^bold>\<and> P z) x \<longrightarrow> (\<rightharpoondown>(=) z) b)\<rfloor>

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>z. (w r w1 \<and> existsAt z w1 \<and> P z w1) \<longrightarrow> (\<^bold>\<rightharpoondown>(id b)) z w1"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>x. \<forall>z. ((r) w \<^bold>\<and> existsAt z \<^bold>\<and> P z) x \<longrightarrow> (\<rightharpoondown>(=) z) b)\<rfloor>

goal (1 subgoal):
 1. \<forall>z. ((r) w \<^bold>\<and> existsAt z \<^bold>\<and> P z) w1 \<longrightarrow> (\<rightharpoondown>(=) z) b
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
\<forall>z. ((r) w \<^bold>\<and> existsAt z \<^bold>\<and> P z) w1 \<longrightarrow> (\<rightharpoondown>(=) z) b

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
hence "(w r w1 \<and> existsAt b w1 \<and> P b w1) \<longrightarrow> (\<^bold>\<rightharpoondown>(id b)) b w1"
[PROOF STATE]
proof (prove)
using this:
\<forall>z. ((r) w \<^bold>\<and> existsAt z \<^bold>\<and> P z) w1 \<longrightarrow> (\<rightharpoondown>(=) z) b

goal (1 subgoal):
 1. ((r) w \<^bold>\<and> existsAt b \<^bold>\<and> P b) w1 \<longrightarrow> (\<rightharpoondown>(=) b) b
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
((r) w \<^bold>\<and> existsAt b \<^bold>\<and> P b) w1 \<longrightarrow> (\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
hence  "\<not>(w r w1 \<and> existsAt b w1 \<and> P b w1) \<or> (\<^bold>\<rightharpoondown>(id b)) b w1"
[PROOF STATE]
proof (prove)
using this:
((r) w \<^bold>\<and> existsAt b \<^bold>\<and> P b) w1 \<longrightarrow> (\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. (\<^bold>\<not>((r) w \<^bold>\<and> existsAt b \<^bold>\<and> P b)) w1 \<or> (\<rightharpoondown>(=) b) b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<^bold>\<not>((r) w \<^bold>\<and> existsAt b \<^bold>\<and> P b)) w1 \<or> (\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
hence "(\<^bold>\<rightharpoondown>(id b)) b w"
[PROOF STATE]
proof (prove)
using this:
(\<^bold>\<not>((r) w \<^bold>\<and> existsAt b \<^bold>\<and> P b)) w1 \<or> (\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. (\<rightharpoondown>(=) b) b
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
(\<^bold>\<not>((r) w \<^bold>\<and> existsAt b \<^bold>\<and> P b)) w1 \<or> (\<rightharpoondown>(=) b) b
w r w1 \<and> existsAt b w1 \<and> P b w1 \<and> (\<rightharpoondown>(=) a) b

goal (1 subgoal):
 1. (\<rightharpoondown>(=) b) b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
hence "\<not>(b=b)"
[PROOF STATE]
proof (prove)
using this:
(\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. (\<rightharpoondown>(=) b) b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> P x v \<longrightarrow> (\<rightharpoondown>(=) x) b)) w \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
(\<rightharpoondown>(=) b) b

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment> \<open>model found: so far all axioms consistent\<close>