[STATEMENT]
lemma guha_deterministic2: "\<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a)\<rbrakk> \<Longrightarrow> x1 = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a)\<rbrakk> \<Longrightarrow> x1 = a
[PROOF STEP]
proof(rule ccontr, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
no_overlaps \<gamma> ft
guha_table_semantics \<gamma> ft p (Some x1)
guha_table_semantics \<gamma> ft p (Some a)
x1 \<noteq> a

goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note 1(2-3)[THEN guha_matched_rule_inversion]
[PROOF STATE]
proof (state)
this:
\<exists>fe\<in>set ft. x1 = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
\<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)

goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>fe\<in>set ft. x1 = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
\<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
obtain fe1 fe2 where fes:
	"fe1\<in>set ft" "x1 = ofe_action fe1" "\<gamma> (ofe_fields fe1) p" "(\<forall>fe'\<in>set ft. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)"
    "fe2\<in>set ft" "a  = ofe_action fe2" "\<gamma> (ofe_fields fe2) p" "(\<forall>fe'\<in>set ft. ofe_prio fe2 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)"
[PROOF STATE]
proof (prove)
using this:
\<exists>fe\<in>set ft. x1 = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
\<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)

goal (1 subgoal):
 1. (\<And>fe1 fe2. \<lbrakk>fe1 \<in> set ft; x1 = ofe_action fe1; \<gamma> (ofe_fields fe1) p; \<forall>fe'\<in>set ft. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p; fe2 \<in> set ft; a = ofe_action fe2; \<gamma> (ofe_fields fe2) p; \<forall>fe'\<in>set ft. ofe_prio fe2 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fe1 \<in> set ft
x1 = ofe_action fe1
\<gamma> (ofe_fields fe1) p
\<forall>fe'\<in>set ft. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
fe2 \<in> set ft
a = ofe_action fe2
\<gamma> (ofe_fields fe2) p
\<forall>fe'\<in>set ft. ofe_prio fe2 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p

goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>x1 \<noteq> a\<close>
[PROOF STATE]
proof (chain)
picking this:
x1 \<noteq> a
[PROOF STEP]
have fene: "fe1 \<noteq> fe2"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> a

goal (1 subgoal):
 1. fe1 \<noteq> fe2
[PROOF STEP]
using fes(2,6)
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> a
x1 = ofe_action fe1
a = ofe_action fe2

goal (1 subgoal):
 1. fe1 \<noteq> fe2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fe1 \<noteq> fe2

goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have pe: "ofe_prio fe1 = ofe_prio fe2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofe_prio fe1 = ofe_prio fe2
[PROOF STEP]
using fes(1,3-4,5,7-8) less_linear
[PROOF STATE]
proof (prove)
using this:
fe1 \<in> set ft
\<gamma> (ofe_fields fe1) p
\<forall>fe'\<in>set ft. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
fe2 \<in> set ft
\<gamma> (ofe_fields fe2) p
\<forall>fe'\<in>set ft. ofe_prio fe2 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
?x < ?y \<or> ?x = ?y \<or> ?y < ?x

goal (1 subgoal):
 1. ofe_prio fe1 = ofe_prio fe2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ofe_prio fe1 = ofe_prio fe2

goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note \<open>no_overlaps \<gamma> ft\<close>[THEN check_no_overlapI, unfolded check_no_overlap_def]
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set ft. \<forall>b\<in>set ft. \<forall>p\<in>UNIV. ofe_prio a = ofe_prio b \<and> \<gamma> (ofe_fields a) p \<and> a \<noteq> b \<longrightarrow> \<not> \<gamma> (ofe_fields b) p

goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note this[unfolded Ball_def, THEN spec, THEN mp, OF fes(1), THEN spec, THEN mp, OF fes(5),THEN spec, THEN mp, OF UNIV_I, of p] pe fene fes(3,7)
[PROOF STATE]
proof (state)
this:
ofe_prio fe1 = ofe_prio fe2 \<and> \<gamma> (ofe_fields fe1) p \<and> fe1 \<noteq> fe2 \<longrightarrow> \<not> \<gamma> (ofe_fields fe2) p
ofe_prio fe1 = ofe_prio fe2
fe1 \<noteq> fe2
\<gamma> (ofe_fields fe1) p
\<gamma> (ofe_fields fe2) p

goal (1 subgoal):
 1. \<lbrakk>no_overlaps \<gamma> ft; guha_table_semantics \<gamma> ft p (Some x1); guha_table_semantics \<gamma> ft p (Some a); x1 \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
ofe_prio fe1 = ofe_prio fe2 \<and> \<gamma> (ofe_fields fe1) p \<and> fe1 \<noteq> fe2 \<longrightarrow> \<not> \<gamma> (ofe_fields fe2) p
ofe_prio fe1 = ofe_prio fe2
fe1 \<noteq> fe2
\<gamma> (ofe_fields fe1) p
\<gamma> (ofe_fields fe2) p

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma guha_equal:
	assumes no: "no_overlaps \<gamma> ft"
	shows "OF_priority_match \<gamma> ft p = option_to_ftb d \<longleftrightarrow> guha_table_semantics \<gamma> ft p d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (OF_priority_match \<gamma> ft p = option_to_ftb d) = guha_table_semantics \<gamma> ft p d
[PROOF STEP]
using guha_equal_hlp[OF no, of p]
[PROOF STATE]
proof (prove)
using this:
guha_table_semantics \<gamma> ft p (ftb_to_option (OF_priority_match \<gamma> ft p))

goal (1 subgoal):
 1. (OF_priority_match \<gamma> ft p = option_to_ftb d) = guha_table_semantics \<gamma> ft p d
[PROOF STEP]
unfolding ftb_to_option_def option_to_ftb_def
[PROOF STATE]
proof (prove)
using this:
guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)

goal (1 subgoal):
 1. (OF_priority_match \<gamma> ft p = (case d of None \<Rightarrow> NoAction | Some a \<Rightarrow> Action a)) = guha_table_semantics \<gamma> ft p d
[PROOF STEP]
apply(cases "OF_priority_match \<gamma> ft p"; cases d)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x1. \<lbrakk>guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); OF_priority_match \<gamma> ft p = Action x1; guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); d = None\<rbrakk> \<Longrightarrow> (OF_priority_match \<gamma> ft p = (case d of None \<Rightarrow> NoAction | Some a \<Rightarrow> Action a)) = guha_table_semantics \<gamma> ft p d
 2. \<And>x1 a. \<lbrakk>guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); OF_priority_match \<gamma> ft p = Action x1; guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); d = Some a\<rbrakk> \<Longrightarrow> (OF_priority_match \<gamma> ft p = (case d of None \<Rightarrow> NoAction | Some a \<Rightarrow> Action a)) = guha_table_semantics \<gamma> ft p d
 3. \<lbrakk>guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); OF_priority_match \<gamma> ft p = NoAction; guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); d = None\<rbrakk> \<Longrightarrow> (OF_priority_match \<gamma> ft p = (case d of None \<Rightarrow> NoAction | Some a \<Rightarrow> Action a)) = guha_table_semantics \<gamma> ft p d
 4. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); OF_priority_match \<gamma> ft p = NoAction; guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); d = Some a\<rbrakk> \<Longrightarrow> (OF_priority_match \<gamma> ft p = (case d of None \<Rightarrow> NoAction | Some a \<Rightarrow> Action a)) = guha_table_semantics \<gamma> ft p d
 5. \<lbrakk>guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); OF_priority_match \<gamma> ft p = Undefined; guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); d = None\<rbrakk> \<Longrightarrow> (OF_priority_match \<gamma> ft p = (case d of None \<Rightarrow> NoAction | Some a \<Rightarrow> Action a)) = guha_table_semantics \<gamma> ft p d
 6. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); OF_priority_match \<gamma> ft p = Undefined; guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None); d = Some a\<rbrakk> \<Longrightarrow> (OF_priority_match \<gamma> ft p = (case d of None \<Rightarrow> NoAction | Some a \<Rightarrow> Action a)) = guha_table_semantics \<gamma> ft p d
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>guha_table_semantics \<gamma> ft p (Some x1); OF_priority_match \<gamma> ft p = Action x1; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 2. \<And>x1 a. \<lbrakk>guha_table_semantics \<gamma> ft p (Some x1); OF_priority_match \<gamma> ft p = Action x1; d = Some a\<rbrakk> \<Longrightarrow> (x1 = a) = guha_table_semantics \<gamma> ft p (Some a)
 3. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p None; OF_priority_match \<gamma> ft p = NoAction; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
 4. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 5. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
using guha_deterministic1
[PROOF STATE]
proof (prove)
using this:
guha_table_semantics ?\<gamma> ?ft ?p (Some ?x1.0) \<Longrightarrow> \<not> guha_table_semantics ?\<gamma> ?ft ?p None

goal (5 subgoals):
 1. \<And>x1. \<lbrakk>guha_table_semantics \<gamma> ft p (Some x1); OF_priority_match \<gamma> ft p = Action x1; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 2. \<And>x1 a. \<lbrakk>guha_table_semantics \<gamma> ft p (Some x1); OF_priority_match \<gamma> ft p = Action x1; d = Some a\<rbrakk> \<Longrightarrow> (x1 = a) = guha_table_semantics \<gamma> ft p (Some a)
 3. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p None; OF_priority_match \<gamma> ft p = NoAction; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
 4. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 5. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 a. \<lbrakk>guha_table_semantics \<gamma> ft p (Some x1); OF_priority_match \<gamma> ft p = Action x1; d = Some a\<rbrakk> \<Longrightarrow> (x1 = a) = guha_table_semantics \<gamma> ft p (Some a)
 2. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p None; OF_priority_match \<gamma> ft p = NoAction; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
 3. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 4. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
using guha_deterministic2[OF no]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>guha_table_semantics \<gamma> ft ?p (Some ?x1.0); guha_table_semantics \<gamma> ft ?p (Some ?a)\<rbrakk> \<Longrightarrow> ?x1.0 = ?a

goal (4 subgoals):
 1. \<And>x1 a. \<lbrakk>guha_table_semantics \<gamma> ft p (Some x1); OF_priority_match \<gamma> ft p = Action x1; d = Some a\<rbrakk> \<Longrightarrow> (x1 = a) = guha_table_semantics \<gamma> ft p (Some a)
 2. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p None; OF_priority_match \<gamma> ft p = NoAction; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
 3. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 4. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p None; OF_priority_match \<gamma> ft p = NoAction; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
 2. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 3. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
using guha_deterministic1
[PROOF STATE]
proof (prove)
using this:
guha_table_semantics ?\<gamma> ?ft ?p (Some ?x1.0) \<Longrightarrow> \<not> guha_table_semantics ?\<gamma> ?ft ?p None

goal (3 subgoals):
 1. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p None; OF_priority_match \<gamma> ft p = NoAction; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
 2. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 3. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 2. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
using no_overlaps_not_unefined[OF no]
[PROOF STATE]
proof (prove)
using this:
OF_priority_match \<gamma> ft ?p \<noteq> Undefined

goal (2 subgoals):
 1. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = None\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
 2. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
using no_overlaps_not_unefined[OF no]
[PROOF STATE]
proof (prove)
using this:
OF_priority_match \<gamma> ft ?p \<noteq> Undefined

goal (1 subgoal):
 1. \<And>a. \<lbrakk>guha_table_semantics \<gamma> ft p undefined; OF_priority_match \<gamma> ft p = Undefined; d = Some a\<rbrakk> \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma guha_nondeterministicD:
	assumes "\<not>check_no_overlap \<gamma> ft"
	shows "\<exists>fe1 fe2 p. fe1 \<in> set ft \<and> fe2 \<in> set ft
		\<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe1))
		\<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>fe1 fe2 p. fe1 \<in> set ft \<and> fe2 \<in> set ft \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> check_no_overlap \<gamma> ft

goal (1 subgoal):
 1. \<exists>fe1 fe2 p. fe1 \<in> set ft \<and> fe2 \<in> set ft \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(unfold check_no_overlap_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set ft. \<forall>b\<in>set ft. \<forall>p\<in>UNIV. ofe_prio a = ofe_prio b \<and> \<gamma> (ofe_fields a) p \<and> a \<noteq> b \<longrightarrow> \<not> \<gamma> (ofe_fields b) p) \<Longrightarrow> \<exists>fe1 fe2 p. fe1 \<in> set ft \<and> fe2 \<in> set ft \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b p. \<lbrakk>a \<in> set ft; b \<in> set ft; ofe_prio a = ofe_prio b; \<gamma> (ofe_fields a) p; a \<noteq> b; \<gamma> (ofe_fields b) p\<rbrakk> \<Longrightarrow> \<exists>fe1. fe1 \<in> set ft \<and> (\<exists>fe2. fe2 \<in> set ft \<and> (\<exists>p. guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))))
[PROOF STEP]
apply(rename_tac fe1 fe2 p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> \<exists>fe1. fe1 \<in> set ft \<and> (\<exists>fe2. fe2 \<in> set ft \<and> (\<exists>p. guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))))
[PROOF STEP]
apply(rule_tac x = fe1 in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> fe1 \<in> set ft \<and> (\<exists>fe2. fe2 \<in> set ft \<and> (\<exists>p. guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> \<exists>fe2. fe2 \<in> set ft \<and> (\<exists>p. guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2)))
[PROOF STEP]
apply(rule_tac x = fe2 in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> fe2 \<in> set ft \<and> (\<exists>p. guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> \<exists>p. guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(rule_tac x = p in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe1)) \<and> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe1))
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(subst guha_table_semantics.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> (\<exists>\<gamma>' fe pa ft1 ft2. \<gamma> = \<gamma>' \<and> ft = ft1 @ fe # ft2 \<and> p = pa \<and> Some (ofe_action fe1) = Some (ofe_action fe) \<and> \<gamma>' (ofe_fields fe) pa = True \<and> (\<forall>fe'\<in>set (ft1 @ ft2). ofe_prio fe < ofe_prio fe' \<longrightarrow> \<gamma>' (ofe_fields fe') pa = False)) \<or> (\<exists>fta \<gamma>' pa. \<gamma> = \<gamma>' \<and> ft = fta \<and> p = pa \<and> Some (ofe_action fe1) = None \<and> (\<forall>fe\<in>set fta. \<gamma>' (ofe_fields fe) pa = False))
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> \<exists>\<gamma>' fe pa ft1 ft2. \<gamma> = \<gamma>' \<and> ft = ft1 @ fe # ft2 \<and> p = pa \<and> Some (ofe_action fe1) = Some (ofe_action fe) \<and> \<gamma>' (ofe_fields fe) pa = True \<and> (\<forall>fe'\<in>set (ft1 @ ft2). ofe_prio fe < ofe_prio fe' \<longrightarrow> \<gamma>' (ofe_fields fe') pa = False)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> \<exists>fe ft1 ft2. ft = ft1 @ fe # ft2 \<and> ofe_action fe1 = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft1 \<union> set ft2. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(rule_tac x = fe1 in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> \<exists>ft1 ft2. ft = ft1 @ fe1 # ft2 \<and> ofe_action fe1 = ofe_action fe1 \<and> \<gamma> (ofe_fields fe1) p \<and> (\<forall>fe'\<in>set ft1 \<union> set ft2. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(drule split_list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p. \<lbrakk>fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p; \<exists>ys zs. ft = ys @ fe1 # zs\<rbrakk> \<Longrightarrow> \<exists>ft1 ft2. ft = ft1 @ fe1 # ft2 \<and> ofe_action fe1 = ofe_action fe1 \<and> \<gamma> (ofe_fields fe1) p \<and> (\<forall>fe'\<in>set ft1 \<union> set ft2. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p ys zs. \<lbrakk>fe2 \<in> set (ys @ fe1 # zs); ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p; ft = ys @ fe1 # zs\<rbrakk> \<Longrightarrow> \<exists>ft1 ft2. ys @ fe1 # zs = ft1 @ fe1 # ft2 \<and> ofe_action fe1 = ofe_action fe1 \<and> \<gamma> (ofe_fields fe1) p \<and> (\<forall>fe'\<in>set ft1 \<union> set ft2. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(rename_tac ft1 ft2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p ft1 ft2. \<lbrakk>fe2 \<in> set (ft1 @ fe1 # ft2); ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p; ft = ft1 @ fe1 # ft2\<rbrakk> \<Longrightarrow> \<exists>ft1a ft2a. ft1 @ fe1 # ft2 = ft1a @ fe1 # ft2a \<and> ofe_action fe1 = ofe_action fe1 \<and> \<gamma> (ofe_fields fe1) p \<and> (\<forall>fe'\<in>set ft1a \<union> set ft2a. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(rule_tac x = ft1 in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p ft1 ft2. \<lbrakk>fe2 \<in> set (ft1 @ fe1 # ft2); ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p; ft = ft1 @ fe1 # ft2\<rbrakk> \<Longrightarrow> \<exists>ft2a. ft1 @ fe1 # ft2 = ft1 @ fe1 # ft2a \<and> ofe_action fe1 = ofe_action fe1 \<and> \<gamma> (ofe_fields fe1) p \<and> (\<forall>fe'\<in>set ft1 \<union> set ft2a. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(rule_tac x = ft2 in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p ft1 ft2. \<lbrakk>fe2 \<in> set (ft1 @ fe1 # ft2); ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p; ft = ft1 @ fe1 # ft2\<rbrakk> \<Longrightarrow> ft1 @ fe1 # ft2 = ft1 @ fe1 # ft2 \<and> ofe_action fe1 = ofe_action fe1 \<and> \<gamma> (ofe_fields fe1) p \<and> (\<forall>fe'\<in>set ft1 \<union> set ft2. ofe_prio fe1 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fe1 fe2 p ft1 ft2. \<lbrakk>fe2 \<in> set ft1 \<or> fe2 \<in> set ft2; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p; ft = ft1 @ fe1 # ft2\<rbrakk> \<Longrightarrow> \<forall>fe'\<in>set ft1 \<union> set ft2. ofe_prio fe2 < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
 2. \<And>fe1 fe2 p. \<lbrakk>fe1 \<in> set ft; fe2 \<in> set ft; ofe_prio fe1 = ofe_prio fe2; \<gamma> (ofe_fields fe1) p; fe1 \<noteq> fe2; \<gamma> (ofe_fields fe2) p\<rbrakk> \<Longrightarrow> guha_table_semantics \<gamma> ft p (Some (ofe_action fe2))
[PROOF STEP]
oops


[STATEMENT]
lemma exe_impl_exists:
    "[\<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p), \<^bold>\<iota>y . \<phi> y x\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y . \<^bold>\<A>\<phi> y x) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x) in v]
[PROOF STEP]
proof (rule "\<^bold>\<equiv>I"; rule CP)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
 2. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
fix \<phi> :: "\<nu>\<Rightarrow>\<nu>\<Rightarrow>\<o>" and x :: \<nu> and v :: i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
 2. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
assume "[\<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p),\<^bold>\<iota>y . \<phi> y x\<rparr> in v]"
[PROOF STATE]
proof (state)
this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]

goal (2 subgoals):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
 2. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
hence "[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y)
              \<^bold>& \<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p), y\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
using nec_russell_axiom[equiv_lr] SimpleExOrEnc.intros
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
\<lbrakk>SimpleExOrEnc ?\<psi>1; [?\<psi>1 (\<^bold>\<iota>x. ?\<phi>1 x) in ?v]\<rbrakk> \<Longrightarrow> [\<^bold>\<exists>x. \<^bold>\<A>?\<phi>1 x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>?\<phi>1 z \<^bold>\<rightarrow> z \<^bold>= x) \<^bold>& ?\<psi>1 (x\<^sup>P) in ?v]
SimpleExOrEnc (exe1 ?F)
SimpleExOrEnc (\<lambda>x. \<lparr>?F,x,?y\<rparr>)
SimpleExOrEnc (exe2 ?F ?y)
SimpleExOrEnc (\<lambda>x. \<lparr>?F,x,?y,?z\<rparr>)
SimpleExOrEnc (\<lambda>x. \<lparr>?F,?y,x,?z\<rparr>)
SimpleExOrEnc (exe3 ?F ?y ?z)
SimpleExOrEnc (\<lambda>x. \<lbrace>x,?F\<rbrace>)

goal (1 subgoal):
 1. [\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (2 subgoals):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
 2. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
obtain y where
        "[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y)
          \<^bold>& \<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p), y\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. (\<And>y. [\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (2 subgoals):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
 2. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
hence "[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[PROOF STEP]
using "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (2 subgoals):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
 2. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
hence "[\<^bold>\<exists>y . \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[PROOF STEP]
by (rule existential)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (2 subgoals):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
 2. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
thus "[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]
[PROOF STEP]
unfolding exists_unique_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> x \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> x \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
fix \<phi> :: "\<nu>\<Rightarrow>\<nu>\<Rightarrow>\<o>" and x :: \<nu> and v :: i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
assume "[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]"
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
hence "[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[PROOF STEP]
unfolding exists_unique_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> x \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> x \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[PROOF STEP]
obtain y where
        "[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (1 subgoal):
 1. (\<And>y. [\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
have "[\<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p),y\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
apply (rule beta_C_meta_1[equiv_rl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. IsProperInX (\<lambda>a. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p)
 2. [\<^bold>\<forall>p. p \<^bold>\<rightarrow> p in v]
[PROOF STEP]
apply show_proper
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<forall>p. p \<^bold>\<rightarrow> p in v]
[PROOF STEP]
by PLM_solver
[PROOF STATE]
proof (state)
this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
have "[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y)
                        \<^bold>& \<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p),y\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
using "\<^bold>&I"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) in v]
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
\<lbrakk>[?\<phi> in ?v]; [?\<psi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> \<^bold>& ?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
hence "[\<^bold>\<exists> y . \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y)
              \<^bold>& \<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p),y\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
[PROOF STEP]
by (rule existential)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y x in v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
thus "[\<lparr>(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p), \<^bold>\<iota>y. \<phi> y x\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
using nec_russell_axiom[equiv_rl]
          SimpleExOrEnc.intros
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>y. \<^bold>\<A>\<phi> y x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>\<phi> z x \<^bold>\<rightarrow> z \<^bold>= y) \<^bold>& \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,y\<^sup>P\<rparr> in v]
\<lbrakk>SimpleExOrEnc ?\<psi>1; [\<^bold>\<exists>x. \<^bold>\<A>?\<phi>1 x \<^bold>& (\<^bold>\<forall>z. \<^bold>\<A>?\<phi>1 z \<^bold>\<rightarrow> z \<^bold>= x) \<^bold>& ?\<psi>1 (x\<^sup>P) in ?v]\<rbrakk> \<Longrightarrow> [?\<psi>1 (\<^bold>\<iota>x. ?\<phi>1 x) in ?v]
SimpleExOrEnc (exe1 ?F)
SimpleExOrEnc (\<lambda>x. \<lparr>?F,x,?y\<rparr>)
SimpleExOrEnc (exe2 ?F ?y)
SimpleExOrEnc (\<lambda>x. \<lparr>?F,x,?y,?z\<rparr>)
SimpleExOrEnc (\<lambda>x. \<lparr>?F,?y,x,?z\<rparr>)
SimpleExOrEnc (exe3 ?F ?y ?z)
SimpleExOrEnc (\<lambda>x. \<lbrace>x,?F\<rbrace>)

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y x\<rparr> in v]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exists_unique_actual_equiv:
    "[(\<^bold>\<exists>!y . \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P))) \<^bold>\<equiv> \<^bold>\<A>\<psi> (x\<^sup>P) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P))) \<^bold>\<equiv> \<^bold>\<A>\<psi> (x\<^sup>P) in v]
[PROOF STEP]
proof (rule "\<^bold>\<equiv>I"; rule CP)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
fix x v
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
let ?\<phi> = "\<lambda> y x. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
assume "[\<^bold>\<exists>!y. \<^bold>\<A>?\<phi> y x in v]"
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (2 subgoals):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
hence "[\<^bold>\<exists>\<alpha>. \<^bold>\<A>?\<phi> \<alpha> x \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>?\<phi> \<beta> x \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
unfolding exists_unique_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (2 subgoals):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
obtain \<alpha> where
      "[\<^bold>\<A>?\<phi> \<alpha> x \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>?\<phi> \<beta> x \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. (\<And>\<alpha>. [\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (2 subgoals):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
hence "[\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
using "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (2 subgoals):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
thus "[\<^bold>\<A>(\<psi> (x\<^sup>P)) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
[PROOF STEP]
using Act_Basic_2[equiv_lr] "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[\<^bold>\<A>(?\<phi>1 \<^bold>& ?\<psi>1) in ?v] \<Longrightarrow> [\<^bold>\<A>?\<phi>1 \<^bold>& \<^bold>\<A>?\<psi>1 in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<psi> (x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
fix x v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
let ?\<phi> = "\<lambda> y x. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
assume 1: "[\<^bold>\<A>\<psi> (x\<^sup>P) in v]"
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<psi> (x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
have "[x \<^bold>= x in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x \<^bold>= x in v]
[PROOF STEP]
using id_eq_1[where 'a=\<nu>]
[PROOF STATE]
proof (prove)
using this:
[?x \<^bold>= ?x in ?v]

goal (1 subgoal):
 1. [x \<^bold>= x in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[x \<^bold>= x in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
hence "[\<^bold>\<A>(x \<^bold>= x) in v]"
[PROOF STATE]
proof (prove)
using this:
[x \<^bold>= x in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x) in v]
[PROOF STEP]
using id_act_3[equiv_lr]
[PROOF STATE]
proof (prove)
using this:
[x \<^bold>= x in v]
[?\<alpha>1 \<^bold>= ?\<beta>1 in ?v] \<Longrightarrow> [\<^bold>\<A>(?\<alpha>1 \<^bold>= ?\<beta>1) in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x) in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(x \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
hence "[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
using 1 Act_Basic_2[equiv_rl] "\<^bold>&I"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x \<^bold>= x) in v]
[\<^bold>\<A>\<psi> (x\<^sup>P) in v]
[\<^bold>\<A>?\<phi>1 \<^bold>& \<^bold>\<A>?\<psi>1 in ?v] \<Longrightarrow> [\<^bold>\<A>(?\<phi>1 \<^bold>& ?\<psi>1) in ?v]
\<lbrakk>[?\<phi> in ?v]; [?\<psi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> \<^bold>& ?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
hence "[\<^bold>\<A>?\<phi> x x in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
have "[\<^bold>\<forall>\<beta>. \<^bold>\<A>?\<phi> \<beta> x \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]
[PROOF STEP]
proof (rule "\<^bold>\<forall>I"; rule CP)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
fix \<beta>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
assume "[\<^bold>\<A>?\<phi> \<beta> x in v]"
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
hence "[\<^bold>\<A>(\<beta> \<^bold>= x) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<beta> \<^bold>= x) in v]
[PROOF STEP]
using Act_Basic_2[equiv_lr] "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[\<^bold>\<A>(?\<phi>1 \<^bold>& ?\<psi>1) in ?v] \<Longrightarrow> [\<^bold>\<A>?\<phi>1 \<^bold>& \<^bold>\<A>?\<psi>1 in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<beta> \<^bold>= x) in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(\<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
thus "[\<beta> \<^bold>= x in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<beta> \<^bold>= x in v]
[PROOF STEP]
using id_act_3[equiv_rl]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta> \<^bold>= x) in v]
[\<^bold>\<A>(?\<alpha>1 \<^bold>= ?\<beta>1) in ?v] \<Longrightarrow> [?\<alpha>1 \<^bold>= ?\<beta>1 in ?v]

goal (1 subgoal):
 1. [\<beta> \<^bold>= x in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<beta> \<^bold>= x in v]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]
[PROOF STEP]
have "[\<^bold>\<A>?\<phi> x x \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>?\<phi> \<beta> x \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]
[PROOF STEP]
using "\<^bold>&I"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]
\<lbrakk>[?\<phi> in ?v]; [?\<psi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> \<^bold>& ?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
hence "[\<^bold>\<exists>\<alpha>. \<^bold>\<A>?\<phi> \<alpha> x \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>?\<phi> \<beta> x \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
by (rule existential)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
thus "[\<^bold>\<exists>!y. \<^bold>\<A>?\<phi> y x in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
unfolding exists_unique_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>(\<alpha> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta> \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fake_beta:
    assumes "\<And> G \<phi>. IsProperInX (\<lambda>x . \<lparr>G,\<^bold>\<iota>y . \<phi> y x\<rparr>)"
    shows "[\<lparr>backdoor (\<lambda> x . \<psi> x), x\<^sup>P\<rparr> \<^bold>\<equiv> \<^bold>\<A>\<psi> (x\<^sup>P) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> \<^bold>\<equiv> \<^bold>\<A>\<psi> (x\<^sup>P) in v]
[PROOF STEP]
proof (rule "\<^bold>\<equiv>I"; rule CP)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
assume "[\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (state)
this:
[\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]

goal (2 subgoals):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
hence "[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[PROOF STEP]
using beta_C_meta_1[equiv_lr, OF assms]
[PROOF STATE]
proof (prove)
using this:
[\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[\<lparr>\<^bold>\<lambda>y. \<lparr>?G2,\<^bold>\<iota>ya. ?\<phi>2 ya (y\<^sup>P)\<rparr>,?x1\<^sup>P\<rparr> in ?v] \<Longrightarrow> [\<lparr>?G2,\<^bold>\<iota>y. ?\<phi>2 y (?x1\<^sup>P)\<rparr> in ?v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[PROOF STEP]
unfolding backdoor_def identity_\<nu>_def
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<psi> (x\<^sup>P)\<rparr>,x\<^sup>P\<rparr> in v]
[\<lparr>\<^bold>\<lambda>y. \<lparr>?G2,\<^bold>\<iota>ya. ?\<phi>2 ya (y\<^sup>P)\<rparr>,?x1\<^sup>P\<rparr> in ?v] \<Longrightarrow> [\<lparr>?G2,\<^bold>\<iota>y. ?\<phi>2 y (?x1\<^sup>P)\<rparr> in ?v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]

goal (2 subgoals):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
hence "[\<^bold>\<exists>!y. \<^bold>\<A> (y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
using exe_impl_exists[equiv_lr]
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. ?\<phi>1 y ?x1\<rparr> in ?v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>?\<phi>1 y ?x1 in ?v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (2 subgoals):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v] \<Longrightarrow> [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
 2. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
thus "[\<^bold>\<A>\<psi> (x\<^sup>P) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
[PROOF STEP]
using exists_unique_actual_equiv[equiv_lr]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= ?x1 \<^bold>& ?\<psi>1 (?x1\<^sup>P)) in ?v] \<Longrightarrow> [\<^bold>\<A>?\<psi>1 (?x1\<^sup>P) in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<psi> (x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
assume "[\<^bold>\<A>\<psi> (x\<^sup>P) in v]"
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<psi> (x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
hence "[\<^bold>\<exists>!y. \<^bold>\<A> (y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<psi> (x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
using exists_unique_actual_equiv[equiv_rl]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<psi> (x\<^sup>P) in v]
[\<^bold>\<A>?\<psi>1 (?x1\<^sup>P) in ?v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= ?x1 \<^bold>& ?\<psi>1 (?x1\<^sup>P)) in ?v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
hence "[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[PROOF STEP]
using exe_impl_exists[equiv_rl]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>!y. \<^bold>\<A>(y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)) in v]
[\<^bold>\<exists>!y. \<^bold>\<A>?\<phi>1 y ?x1 in ?v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. ?\<phi>1 y ?x1\<rparr> in ?v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<psi> (x\<^sup>P) in v] \<Longrightarrow> [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
thus "[\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]

goal (1 subgoal):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
using beta_C_meta_1[equiv_rl, OF assms]
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[\<lparr>?G2,\<^bold>\<iota>y. ?\<phi>2 y (?x1\<^sup>P)\<rparr> in ?v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>y. \<lparr>?G2,\<^bold>\<iota>ya. ?\<phi>2 ya (y\<^sup>P)\<rparr>,?x1\<^sup>P\<rparr> in ?v]

goal (1 subgoal):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
unfolding backdoor_def
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[\<lparr>?G2,\<^bold>\<iota>y. ?\<phi>2 y (?x1\<^sup>P)\<rparr> in ?v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>y. \<lparr>?G2,\<^bold>\<iota>ya. ?\<phi>2 ya (y\<^sup>P)\<rparr>,?x1\<^sup>P\<rparr> in ?v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y \<^bold>= x \<^bold>& \<psi> (x\<^sup>P)\<rparr>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
unfolding identity_\<nu>_def
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<psi> (x\<^sup>P)\<rparr> in v]
[\<lparr>?G2,\<^bold>\<iota>y. ?\<phi>2 y (?x1\<^sup>P)\<rparr> in ?v] \<Longrightarrow> [\<lparr>\<^bold>\<lambda>y. \<lparr>?G2,\<^bold>\<iota>ya. ?\<phi>2 ya (y\<^sup>P)\<rparr>,?x1\<^sup>P\<rparr> in ?v]

goal (1 subgoal):
 1. [\<lparr>\<^bold>\<lambda>x. \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. y\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<psi> (x\<^sup>P)\<rparr>,x\<^sup>P\<rparr> in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> in v]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fake_beta_act:
    assumes "\<And> G \<phi>. IsProperInX (\<lambda>x . \<lparr>G,\<^bold>\<iota>y . \<phi> y x\<rparr>)"
    shows "[\<lparr>backdoor (\<lambda> x . \<psi> x), x\<^sup>P\<rparr> \<^bold>\<equiv> \<psi> (x\<^sup>P) in dw]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> \<^bold>\<equiv> \<psi> (x\<^sup>P) in dw]
[PROOF STEP]
using fake_beta[OF assms]
      logic_actual[necessitation_averse_axiom_instance]
      intro_elim_6_e
[PROOF STATE]
proof (prove)
using this:
[\<lparr>backdoor ?\<psi>,?x\<^sup>P\<rparr> \<^bold>\<equiv> \<^bold>\<A>?\<psi> (?x\<^sup>P) in ?v]
[\<^bold>\<A>?\<phi>1 \<^bold>\<equiv> ?\<phi>1 in dw]
\<lbrakk>[?\<phi> \<^bold>\<equiv> ?\<psi> in ?v]; [?\<psi> \<^bold>\<equiv> ?\<chi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> \<^bold>\<equiv> ?\<chi> in ?v]

goal (1 subgoal):
 1. [\<lparr>backdoor \<psi>,x\<^sup>P\<rparr> \<^bold>\<equiv> \<psi> (x\<^sup>P) in dw]
[PROOF STEP]
by blast


[STATEMENT]
lemma paradox:
    assumes "\<And> G \<phi>. IsProperInX (\<lambda>x . \<lparr>G,\<^bold>\<iota>y . \<phi> y x\<rparr>)"
    shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
obtain K where K_def:
      "K = backdoor (\<lambda> x . \<^bold>\<exists> F . \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. K = backdoor (\<lambda>x. \<^bold>\<exists>F. \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K = backdoor (\<lambda>x. \<^bold>\<exists>F. \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>)

goal (1 subgoal):
 1. False
[PROOF STEP]
have "[\<^bold>\<exists>x. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> (F \<^bold>= K)) in dw]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<exists>x. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw]
[PROOF STEP]
using A_objects[axiom_instance]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>x. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> ?\<phi>1 F) in ?v]

goal (1 subgoal):
 1. [\<^bold>\<exists>x. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>x. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>x. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw]
[PROOF STEP]
obtain x where x_prop:
      "[\<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> (F \<^bold>= K)) in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>x. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw]

goal (1 subgoal):
 1. (\<And>x. [\<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
[\<lparr>A!,x\<^sup>P\<rparr> \<^bold>& (\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<equiv> F \<^bold>= K) in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
assume "[\<lparr>K,x\<^sup>P\<rparr> in dw]"
[PROOF STATE]
proof (state)
this:
[\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "[\<^bold>\<exists> F . \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
using this:
[\<lparr>backdoor (\<lambda>x. \<^bold>\<exists>F. \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>),x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
using fake_beta_act[OF assms, equiv_lr]
[PROOF STATE]
proof (prove)
using this:
[\<lparr>backdoor (\<lambda>x. \<^bold>\<exists>F. \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>),x\<^sup>P\<rparr> in dw]
[\<lparr>backdoor ?\<psi>1,?x1\<^sup>P\<rparr> in dw] \<Longrightarrow> [?\<psi>1 (?x1\<^sup>P) in dw]

goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
obtain F where F_def:
        "[\<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. (\<And>F. [\<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "[F \<^bold>= K in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. [F \<^bold>= K in dw]
[PROOF STEP]
using x_prop[conj2, THEN "\<^bold>\<forall>E"[where \<beta>=F], equiv_lr]
          "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]
[\<lbrace>x\<^sup>P,F\<rbrace> in dw] \<Longrightarrow> [F \<^bold>= K in dw]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [F \<^bold>= K in dw]
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
using this:
[\<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]
[\<lbrace>x\<^sup>P,F\<rbrace> in dw] \<Longrightarrow> [F \<^bold>= backdoor (\<lambda>x. \<^bold>\<exists>F. \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>) in dw]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [F \<^bold>= backdoor (\<lambda>x. \<^bold>\<exists>F. \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>) in dw]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[F \<^bold>= K in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "[\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]"
[PROOF STATE]
proof (prove)
using this:
[F \<^bold>= K in dw]

goal (1 subgoal):
 1. [\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
using l_identity[axiom_instance,deduction,deduction]
             F_def[conj2]
[PROOF STATE]
proof (prove)
using this:
[F \<^bold>= K in dw]
\<lbrakk>[?\<alpha>3 \<^bold>= ?\<beta>3 in ?v]; [?\<phi>3 ?\<alpha>3 in ?v]\<rbrakk> \<Longrightarrow> [?\<phi>3 ?\<beta>3 in ?v]
[\<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. [\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
[\<lparr>K,x\<^sup>P\<rparr> in dw] \<Longrightarrow> [\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
hence 1: "[\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<lparr>K,x\<^sup>P\<rparr> in dw] \<Longrightarrow> [\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. [\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
using reductio_aa_1
[PROOF STATE]
proof (prove)
using this:
[\<lparr>K,x\<^sup>P\<rparr> in dw] \<Longrightarrow> [\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]
\<lbrakk>[\<^bold>\<not>?\<phi> in ?v] \<Longrightarrow> [\<^bold>\<not>?\<psi> in ?v]; [\<^bold>\<not>?\<phi> in ?v] \<Longrightarrow> [?\<psi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "[\<^bold>\<not>(\<^bold>\<exists> F . \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr>) in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. [\<^bold>\<not>(\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr>) in dw]
[PROOF STEP]
using fake_beta_act[OF assms,
            THEN oth_class_taut_5_d[equiv_lr],
            equiv_lr]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]
[\<^bold>\<not>\<lparr>backdoor ?\<psi>3,?x3\<^sup>P\<rparr> in dw] \<Longrightarrow> [\<^bold>\<not>?\<psi>3 (?x3\<^sup>P) in dw]

goal (1 subgoal):
 1. [\<^bold>\<not>(\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr>) in dw]
[PROOF STEP]
unfolding K_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<not>\<lparr>backdoor (\<lambda>x. \<^bold>\<exists>F. \<lbrace>x,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<rparr>),x\<^sup>P\<rparr> in dw]
[\<^bold>\<not>\<lparr>backdoor ?\<psi>3,?x3\<^sup>P\<rparr> in dw] \<Longrightarrow> [\<^bold>\<not>?\<psi>3 (?x3\<^sup>P) in dw]

goal (1 subgoal):
 1. [\<^bold>\<not>(\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr>) in dw]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<not>(\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr>) in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "[\<^bold>\<forall> F . \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<not>(\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr>) in dw]

goal (1 subgoal):
 1. [\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<not>(\<^bold>\<exists>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>F,x\<^sup>P\<rparr>) in dw] \<Longrightarrow> [\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
unfolding exists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<not>\<^bold>\<not>(\<^bold>\<forall>xa. \<^bold>\<not>(\<lbrace>x\<^sup>P,xa\<rbrace> \<^bold>& \<^bold>\<not>\<lparr>xa,x\<^sup>P\<rparr>)) in dw] \<Longrightarrow> [\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
by PLM_solver
[PROOF STATE]
proof (state)
this:
[\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
have "[\<lbrace>x\<^sup>P,K\<rbrace> in dw]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lbrace>x\<^sup>P,K\<rbrace> in dw]
[PROOF STEP]
using x_prop[conj2, THEN "\<^bold>\<forall>E"[where \<beta>=K], equiv_rl]
            id_eq_1
[PROOF STATE]
proof (prove)
using this:
[K \<^bold>= K in dw] \<Longrightarrow> [\<lbrace>x\<^sup>P,K\<rbrace> in dw]
[?x \<^bold>= ?x in ?v]

goal (1 subgoal):
 1. [\<lbrace>x\<^sup>P,K\<rbrace> in dw]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<lbrace>x\<^sup>P,K\<rbrace> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]
[\<lbrace>x\<^sup>P,K\<rbrace> in dw]
[PROOF STEP]
have "[\<lparr>K,x\<^sup>P\<rparr> in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]
[\<lbrace>x\<^sup>P,K\<rbrace> in dw]

goal (1 subgoal):
 1. [\<lparr>K,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
using "\<^bold>\<forall>E" vdash_properties_10
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<forall>F. \<lbrace>x\<^sup>P,F\<rbrace> \<^bold>\<rightarrow> \<lparr>F,x\<^sup>P\<rparr> in dw]
[\<lbrace>x\<^sup>P,K\<rbrace> in dw]
[\<^bold>\<forall>\<alpha>. ?\<phi> \<alpha> in ?v] \<Longrightarrow> [?\<phi> ?\<beta> in ?v]
\<lbrakk>[?\<phi> \<^bold>\<rightarrow> ?\<psi> in ?v]; [?\<phi> in ?v]\<rbrakk> \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<lparr>K,x\<^sup>P\<rparr> in dw]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
hence "\<And>\<phi>. [\<phi> in dw]"
[PROOF STATE]
proof (prove)
using this:
[\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. \<And>\<phi>. [\<phi> in dw]
[PROOF STEP]
using raa_cor_2 1
[PROOF STATE]
proof (prove)
using this:
[\<lparr>K,x\<^sup>P\<rparr> in dw]
\<lbrakk>[\<^bold>\<not>?\<phi> in ?v]; [\<^bold>\<not>?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]; [\<^bold>\<not>?\<phi> in ?v]\<rbrakk> \<Longrightarrow> [?\<psi> in ?v]
[\<^bold>\<not>\<lparr>K,x\<^sup>P\<rparr> in dw]

goal (1 subgoal):
 1. \<And>\<phi>. [\<phi> in dw]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[?\<phi> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
[?\<phi> in dw]

goal (1 subgoal):
 1. False
[PROOF STEP]
using Semantics.T4
[PROOF STATE]
proof (prove)
using this:
[?\<phi> in dw]
[\<^bold>\<not>?\<psi> in ?w] = (\<not> [?\<psi> in ?w])

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

goal:
No subgoals!
[PROOF STEP]
qed