[STATEMENT]
lemma while_hyp_change:
  assumes "\<forall>x\<le>n. x > 0 \<longrightarrow> hyp_change z i j x"
  shows "\<forall>x\<le>Suc n. adverse z i j x = adverse z' i j x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<le>0. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc 0. local.adverse z i j x = local.adverse z' i j x
 2. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>0. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (2 subgoals):
 1. \<forall>x\<le>0. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc 0. local.adverse z i j x = local.adverse z' i j x
 2. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>0. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>0. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<forall>x\<le>Suc 0. local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
by (simp add: adverse_def le_Suc_eq)
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>Suc 0. local.adverse z i j x = local.adverse z' i j x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
have "\<forall>x\<le>n. x > 0 \<longrightarrow> hyp_change z i j x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
have "\<forall>x\<le>Suc n. x > 0 \<longrightarrow> adverse z i j x = adverse z' i j x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<forall>x\<le>Suc n. 0 < x \<longrightarrow> local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> local.adverse z i j x = local.adverse z' i j x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> local.adverse z i j x = local.adverse z' i j x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
have "adverse z i j 0 = adverse z' i j 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j 0 = local.adverse z' i j 0
[PROOF STEP]
using adverse_at_01
[PROOF STATE]
proof (prove)
using this:
local.adverse ?z ?i ?j 0 \<down>= ?i
local.adverse ?z ?i ?j 1 \<down>= ?j

goal (1 subgoal):
 1. local.adverse z i j 0 = local.adverse z' i j 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.adverse z i j 0 = local.adverse z' i j 0

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> local.adverse z i j x = local.adverse z' i j x
local.adverse z i j 0 = local.adverse z' i j 0
[PROOF STEP]
have zz': "\<forall>x\<le>Suc n. adverse z i j x = adverse z' i j x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> local.adverse z i j x = local.adverse z' i j x
local.adverse z i j 0 = local.adverse z' i j 0

goal (1 subgoal):
 1. \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
have "adverse z i j \<in> \<R>" "adverse z' i j \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j \<in> \<R> &&& local.adverse z' i j \<in> \<R>
[PROOF STEP]
using adverse_in_R1
[PROOF STATE]
proof (prove)
using this:
local.adverse ?z ?i ?j \<in> \<R>

goal (1 subgoal):
 1. local.adverse z i j \<in> \<R> &&& local.adverse z' i j \<in> \<R>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<in> \<R>
local.adverse z' i j \<in> \<R>

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
local.adverse z i j \<in> \<R>
local.adverse z' i j \<in> \<R>
[PROOF STEP]
have init_zz': "(adverse z i j) \<triangleright> (Suc n) = (adverse z' i j) \<triangleright> (Suc n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
local.adverse z i j \<in> \<R>
local.adverse z' i j \<in> \<R>

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> Suc n = local.adverse z' i j \<triangleright> Suc n
[PROOF STEP]
using init_eqI
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
local.adverse z i j \<in> \<R>
local.adverse z' i j \<in> \<R>
(\<And>x. x \<le> ?n \<Longrightarrow> ?f x = ?g x) \<Longrightarrow> ?f \<triangleright> ?n = ?g \<triangleright> ?n

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> Suc n = local.adverse z' i j \<triangleright> Suc n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<triangleright> Suc n = local.adverse z' i j \<triangleright> Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
have "adverse z i j (Suc (Suc n)) = adverse z' i j (Suc (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
proof (cases "s (e_snoc ((adverse z i j) \<triangleright> (Suc n)) 0) \<noteq> s ((adverse z i j) \<triangleright> (Suc n))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)
[PROOF STEP]
have "s (e_snoc ((adverse z' i j) \<triangleright> (Suc n)) 0) \<noteq> s ((adverse z' i j) \<triangleright> (Suc n))"
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)

goal (1 subgoal):
 1. s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z' i j \<triangleright> Suc n)
[PROOF STEP]
using init_zz'
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)
local.adverse z i j \<triangleright> Suc n = local.adverse z' i j \<triangleright> Suc n

goal (1 subgoal):
 1. s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z' i j \<triangleright> Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z' i j \<triangleright> Suc n)

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z' i j \<triangleright> Suc n)
[PROOF STEP]
have "adverse z' i j (Suc (Suc n)) \<down>= 0"
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z' i j \<triangleright> Suc n)

goal (1 subgoal):
 1. local.adverse z' i j (Suc (Suc n)) \<down>= 0
[PROOF STEP]
by (simp add: adverse_Suc)
[PROOF STATE]
proof (state)
this:
local.adverse z' i j (Suc (Suc n)) \<down>= 0

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.adverse z' i j (Suc (Suc n)) \<down>= 0

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
have "adverse z i j (Suc (Suc n)) \<down>= 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j (Suc (Suc n)) \<down>= 0
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)

goal (1 subgoal):
 1. local.adverse z i j (Suc (Suc n)) \<down>= 0
[PROOF STEP]
by (simp add: adverse_Suc)
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc (Suc n)) \<down>= 0

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.adverse z' i j (Suc (Suc n)) \<down>= 0
local.adverse z i j (Suc (Suc n)) \<down>= 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.adverse z' i j (Suc (Suc n)) \<down>= 0
local.adverse z i j (Suc (Suc n)) \<down>= 0

goal (1 subgoal):
 1. local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)
[PROOF STEP]
have "s (e_snoc ((adverse z' i j) \<triangleright> (Suc n)) 0) = s ((adverse z' i j) \<triangleright> (Suc n))"
[PROOF STATE]
proof (prove)
using this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)

goal (1 subgoal):
 1. s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) = s (local.adverse z' i j \<triangleright> Suc n)
[PROOF STEP]
using init_zz'
[PROOF STATE]
proof (prove)
using this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)
local.adverse z i j \<triangleright> Suc n = local.adverse z' i j \<triangleright> Suc n

goal (1 subgoal):
 1. s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) = s (local.adverse z' i j \<triangleright> Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) = s (local.adverse z' i j \<triangleright> Suc n)

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) = s (local.adverse z' i j \<triangleright> Suc n)
[PROOF STEP]
have "adverse z' i j (Suc (Suc n)) \<down>= 1"
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) = s (local.adverse z' i j \<triangleright> Suc n)

goal (1 subgoal):
 1. local.adverse z' i j (Suc (Suc n)) \<down>= 1
[PROOF STEP]
using init_zz' Suc.prems adverse_Suc
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z' i j \<triangleright> Suc n) 0) = s (local.adverse z' i j \<triangleright> Suc n)
local.adverse z i j \<triangleright> Suc n = local.adverse z' i j \<triangleright> Suc n
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
0 < ?x \<Longrightarrow> local.adverse ?z ?i ?j (Suc ?x) \<down>= (if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 0) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 0 else if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 1) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 1 else ?z)

goal (1 subgoal):
 1. local.adverse z' i j (Suc (Suc n)) \<down>= 1
[PROOF STEP]
by (smt le_refl zero_less_Suc)
[PROOF STATE]
proof (state)
this:
local.adverse z' i j (Suc (Suc n)) \<down>= 1

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.adverse z' i j (Suc (Suc n)) \<down>= 1

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
have "adverse z i j (Suc (Suc n)) \<down>= 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j (Suc (Suc n)) \<down>= 1
[PROOF STEP]
using False Suc.prems adverse_Suc
[PROOF STATE]
proof (prove)
using this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n)
\<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
0 < ?x \<Longrightarrow> local.adverse ?z ?i ?j (Suc ?x) \<down>= (if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 0) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 0 else if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 1) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 1 else ?z)

goal (1 subgoal):
 1. local.adverse z i j (Suc (Suc n)) \<down>= 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc (Suc n)) \<down>= 1

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> Suc n) 0) \<noteq> s (local.adverse z i j \<triangleright> Suc n) \<Longrightarrow> local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.adverse z' i j (Suc (Suc n)) \<down>= 1
local.adverse z i j (Suc (Suc n)) \<down>= 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.adverse z' i j (Suc (Suc n)) \<down>= 1
local.adverse z i j (Suc (Suc n)) \<down>= 1

goal (1 subgoal):
 1. local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<le>n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x; \<forall>x\<le>Suc n. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)\<rbrakk> \<Longrightarrow> \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
with zz'
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))

goal (1 subgoal):
 1. \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
using le_SucE
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>Suc n. local.adverse z i j x = local.adverse z' i j x
local.adverse z i j (Suc (Suc n)) = local.adverse z' i j (Suc (Suc n))
\<lbrakk>?m \<le> Suc ?n; ?m \<le> ?n \<Longrightarrow> ?R; ?m = Suc ?n \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R

goal (1 subgoal):
 1. \<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>Suc (Suc n). local.adverse z i j x = local.adverse z' i j x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma always_hyp_change_no_lim:
  assumes "\<forall>x>0. hyp_change z i j x"
  shows "\<not> learn_lim \<phi> {adverse z i j} s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> learn_lim \<phi> {local.adverse z i j} s
[PROOF STEP]
proof (rule infinite_hyp_changes_not_Lim[of "adverse z i j"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. local.adverse z i j \<in> {local.adverse z i j}
 2. \<forall>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
show "adverse z i j \<in> {adverse z i j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j \<in> {local.adverse z i j}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<in> {local.adverse z i j}

goal (1 subgoal):
 1. \<forall>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
show "\<forall>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (adverse z i j \<triangleright> m\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x>0. s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
obtain m\<^sub>1 where m1: "m\<^sub>1 > n" "hyp_change z i j m\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<forall>x>0. s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. (\<And>m\<^sub>1. \<lbrakk>n < m\<^sub>1; s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<or> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < m\<^sub>1
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<or> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)

goal (1 subgoal):
 1. \<And>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
have "s (adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (adverse z i j \<triangleright> (Suc m\<^sub>1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
proof (cases "s (e_snoc ((adverse z i j) \<triangleright> m\<^sub>1) 0) \<noteq> s ((adverse z i j) \<triangleright> m\<^sub>1)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
[PROOF STEP]
have "adverse z i j (Suc m\<^sub>1) \<down>= 0"
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)

goal (1 subgoal):
 1. local.adverse z i j (Suc m\<^sub>1) \<down>= 0
[PROOF STEP]
using m1 adverse_Suc
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
n < m\<^sub>1
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<or> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
0 < ?x \<Longrightarrow> local.adverse ?z ?i ?j (Suc ?x) \<down>= (if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 0) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 0 else if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 1) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 1 else ?z)

goal (1 subgoal):
 1. local.adverse z i j (Suc m\<^sub>1) \<down>= 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc m\<^sub>1) \<down>= 0

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.adverse z i j (Suc m\<^sub>1) \<down>= 0
[PROOF STEP]
have "(adverse z i j) \<triangleright> (Suc m\<^sub>1) = e_snoc ((adverse z i j) \<triangleright> m\<^sub>1) 0"
[PROOF STATE]
proof (prove)
using this:
local.adverse z i j (Suc m\<^sub>1) \<down>= 0

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0
[PROOF STEP]
by (simp add: init_Suc_snoc)
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0

goal (2 subgoals):
 1. s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
 2. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0

goal (1 subgoal):
 1. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
[PROOF STEP]
have "adverse z i j (Suc m\<^sub>1) \<down>= 1"
[PROOF STATE]
proof (prove)
using this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)

goal (1 subgoal):
 1. local.adverse z i j (Suc m\<^sub>1) \<down>= 1
[PROOF STEP]
using m1 adverse_Suc
[PROOF STATE]
proof (prove)
using this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
n < m\<^sub>1
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<or> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
0 < ?x \<Longrightarrow> local.adverse ?z ?i ?j (Suc ?x) \<down>= (if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 0) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 0 else if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 1) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 1 else ?z)

goal (1 subgoal):
 1. local.adverse z i j (Suc m\<^sub>1) \<down>= 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc m\<^sub>1) \<down>= 1

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.adverse z i j (Suc m\<^sub>1) \<down>= 1
[PROOF STEP]
have "(adverse z i j) \<triangleright> (Suc m\<^sub>1) = e_snoc ((adverse z i j) \<triangleright> m\<^sub>1) 1"
[PROOF STATE]
proof (prove)
using this:
local.adverse z i j (Suc m\<^sub>1) \<down>= 1

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1
[PROOF STEP]
by (simp add: init_Suc_snoc)
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1

goal (1 subgoal):
 1. \<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<Longrightarrow> s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
with False m1(2)
[PROOF STATE]
proof (chain)
picking this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<or> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 0) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1) \<or> s (e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>1)
local.adverse z i j \<triangleright> Suc m\<^sub>1 = e_snoc (local.adverse z i j \<triangleright> m\<^sub>1) 1

goal (1 subgoal):
 1. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)

goal (1 subgoal):
 1. \<And>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
[PROOF STEP]
show "\<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (adverse z i j \<triangleright> m\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)

goal (1 subgoal):
 1. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
using less_SucI m1(1)
[PROOF STATE]
proof (prove)
using this:
s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> Suc m\<^sub>1)
?m < ?n \<Longrightarrow> ?m < Suc ?n
n < m\<^sub>1

goal (1 subgoal):
 1. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>m\<^sub>1>n. \<exists>m\<^sub>2>n. s (local.adverse z i j \<triangleright> m\<^sub>1) \<noteq> s (local.adverse z i j \<triangleright> m\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_hyp_change_no_cons:
  assumes "x > 0" and "\<not> hyp_change z i j x"
  shows "\<not> learn_cons \<phi> {adverse 0 i j, adverse 1 i j} s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
let ?P = "\<lambda>x. x > 0 \<and> \<not> hyp_change z i j x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
define xmin where "xmin = Least ?P"
[PROOF STATE]
proof (state)
this:
xmin = (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < x
\<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))
xmin = (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))
[PROOF STEP]
have xmin:
    "?P xmin"
    "\<And>x. x < xmin \<Longrightarrow> \<not> ?P x"
[PROOF STATE]
proof (prove)
using this:
0 < x
\<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))
xmin = (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))

goal (1 subgoal):
 1. 0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin)) &&& (\<And>x. x < xmin \<Longrightarrow> \<not> (0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))))
[PROOF STEP]
using LeastI[of ?P] not_less_Least[of _ ?P]
[PROOF STATE]
proof (prove)
using this:
0 < x
\<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))
xmin = (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))
0 < ?k \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> ?k) 0) \<noteq> s (local.adverse z i j \<triangleright> ?k) \<or> s (e_snoc (local.adverse z i j \<triangleright> ?k) 1) \<noteq> s (local.adverse z i j \<triangleright> ?k)) \<Longrightarrow> 0 < (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))) \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))) 0) \<noteq> s (local.adverse z i j \<triangleright> (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))) \<or> s (e_snoc (local.adverse z i j \<triangleright> (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))) 1) \<noteq> s (local.adverse z i j \<triangleright> (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)))))
?k < (LEAST x. 0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))) \<Longrightarrow> \<not> (0 < ?k \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> ?k) 0) \<noteq> s (local.adverse z i j \<triangleright> ?k) \<or> s (e_snoc (local.adverse z i j \<triangleright> ?k) 1) \<noteq> s (local.adverse z i j \<triangleright> ?k)))

goal (1 subgoal):
 1. 0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin)) &&& (\<And>x. x < xmin \<Longrightarrow> \<not> (0 < x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin))
?x < xmin \<Longrightarrow> \<not> (0 < ?x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> ?x) 0) \<noteq> s (local.adverse z i j \<triangleright> ?x) \<or> s (e_snoc (local.adverse z i j \<triangleright> ?x) 1) \<noteq> s (local.adverse z i j \<triangleright> ?x)))

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin))
?x < xmin \<Longrightarrow> \<not> (0 < ?x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> ?x) 0) \<noteq> s (local.adverse z i j \<triangleright> ?x) \<or> s (e_snoc (local.adverse z i j \<triangleright> ?x) 1) \<noteq> s (local.adverse z i j \<triangleright> ?x)))
[PROOF STEP]
have "xmin > 0"
[PROOF STATE]
proof (prove)
using this:
0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin))
?x < xmin \<Longrightarrow> \<not> (0 < ?x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> ?x) 0) \<noteq> s (local.adverse z i j \<triangleright> ?x) \<or> s (e_snoc (local.adverse z i j \<triangleright> ?x) 1) \<noteq> s (local.adverse z i j \<triangleright> ?x)))

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

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
have "\<forall>x\<le>xmin - 1. x > 0 \<longrightarrow> hyp_change z i j x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
using xmin
[PROOF STATE]
proof (prove)
using this:
0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin))
?x < xmin \<Longrightarrow> \<not> (0 < ?x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> ?x) 0) \<noteq> s (local.adverse z i j \<triangleright> ?x) \<or> s (e_snoc (local.adverse z i j \<triangleright> ?x) 1) \<noteq> s (local.adverse z i j \<triangleright> ?x)))

goal (1 subgoal):
 1. \<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
by (metis One_nat_def Suc_pred le_imp_less_Suc)
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
[PROOF STEP]
have
    "\<forall>x\<le>xmin. adverse z i j x = adverse 0 i j x"
    "\<forall>x\<le>xmin. adverse z i j x = adverse 1 i j x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)

goal (1 subgoal):
 1. \<forall>x\<le>xmin. local.adverse z i j x = local.adverse 0 i j x &&& \<forall>x\<le>xmin. local.adverse z i j x = local.adverse 1 i j x
[PROOF STEP]
using while_hyp_change[of "xmin - 1" z i j 0]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc (xmin - 1). local.adverse z i j x = local.adverse 0 i j x

goal (1 subgoal):
 1. \<forall>x\<le>xmin. local.adverse z i j x = local.adverse 0 i j x &&& \<forall>x\<le>xmin. local.adverse z i j x = local.adverse 1 i j x
[PROOF STEP]
using while_hyp_change[of "xmin - 1" z i j 1]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x)
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc (xmin - 1). local.adverse z i j x = local.adverse 0 i j x
\<forall>x\<le>xmin - 1. 0 < x \<longrightarrow> s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) \<Longrightarrow> \<forall>x\<le>Suc (xmin - 1). local.adverse z i j x = local.adverse 1 i j x

goal (1 subgoal):
 1. \<forall>x\<le>xmin. local.adverse z i j x = local.adverse 0 i j x &&& \<forall>x\<le>xmin. local.adverse z i j x = local.adverse 1 i j x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 0 i j x
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 1 i j x

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 0 i j x
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 1 i j x
[PROOF STEP]
have
    init_z0: "(adverse z i j) \<triangleright> xmin = (adverse 0 i j) \<triangleright> xmin" and
    init_z1: "(adverse z i j) \<triangleright> xmin = (adverse 1 i j) \<triangleright> xmin"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 0 i j x
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 1 i j x

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> xmin = local.adverse 0 i j \<triangleright> xmin &&& local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin
[PROOF STEP]
using adverse_in_R1 init_eqI
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 0 i j x
\<forall>x\<le>xmin. local.adverse z i j x = local.adverse 1 i j x
local.adverse ?z ?i ?j \<in> \<R>
(\<And>x. x \<le> ?n \<Longrightarrow> ?f x = ?g x) \<Longrightarrow> ?f \<triangleright> ?n = ?g \<triangleright> ?n

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> xmin = local.adverse 0 i j \<triangleright> xmin &&& local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<triangleright> xmin = local.adverse 0 i j \<triangleright> xmin
local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.adverse z i j \<triangleright> xmin = local.adverse 0 i j \<triangleright> xmin
local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin
[PROOF STEP]
have
    a0: "adverse 0 i j (Suc xmin) \<down>= 0" and
    a1: "adverse 1 i j (Suc xmin) \<down>= 1"
[PROOF STATE]
proof (prove)
using this:
local.adverse z i j \<triangleright> xmin = local.adverse 0 i j \<triangleright> xmin
local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin

goal (1 subgoal):
 1. local.adverse 0 i j (Suc xmin) \<down>= 0 &&& local.adverse 1 i j (Suc xmin) \<down>= 1
[PROOF STEP]
using adverse_Suc_not_hyp_change xmin(1) init_z1
[PROOF STATE]
proof (prove)
using this:
local.adverse z i j \<triangleright> xmin = local.adverse 0 i j \<triangleright> xmin
local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin
\<lbrakk>0 < ?x; \<not> (s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 0) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) \<or> s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 1) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x))\<rbrakk> \<Longrightarrow> local.adverse ?z ?i ?j (Suc ?x) \<down>= ?z
0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin))
local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin

goal (1 subgoal):
 1. local.adverse 0 i j (Suc xmin) \<down>= 0 &&& local.adverse 1 i j (Suc xmin) \<down>= 1
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
local.adverse 0 i j (Suc xmin) \<down>= 0
local.adverse 1 i j (Suc xmin) \<down>= 1

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.adverse 0 i j (Suc xmin) \<down>= 0
local.adverse 1 i j (Suc xmin) \<down>= 1
[PROOF STEP]
have
    i0: "(adverse 0 i j) \<triangleright> (Suc xmin) = e_snoc ((adverse z i j) \<triangleright> xmin) 0" and
    i1: "(adverse 1 i j) \<triangleright> (Suc xmin) = e_snoc ((adverse z i j) \<triangleright> xmin) 1"
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 i j (Suc xmin) \<down>= 0
local.adverse 1 i j (Suc xmin) \<down>= 1

goal (1 subgoal):
 1. local.adverse 0 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 0 &&& local.adverse 1 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 1
[PROOF STEP]
using init_z0 init_z1
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 i j (Suc xmin) \<down>= 0
local.adverse 1 i j (Suc xmin) \<down>= 1
local.adverse z i j \<triangleright> xmin = local.adverse 0 i j \<triangleright> xmin
local.adverse z i j \<triangleright> xmin = local.adverse 1 i j \<triangleright> xmin

goal (1 subgoal):
 1. local.adverse 0 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 0 &&& local.adverse 1 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 1
[PROOF STEP]
by (simp_all add: init_Suc_snoc)
[PROOF STATE]
proof (state)
this:
local.adverse 0 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 0
local.adverse 1 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 1

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.adverse 0 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 0
local.adverse 1 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 1

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
have
    "s (e_snoc ((adverse z i j) \<triangleright> xmin) 0) = s ((adverse z i j) \<triangleright> xmin)"
    "s (e_snoc ((adverse z i j) \<triangleright> xmin) 1) = s ((adverse z i j) \<triangleright> xmin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) = s (local.adverse z i j \<triangleright> xmin) &&& s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) = s (local.adverse z i j \<triangleright> xmin)
[PROOF STEP]
using xmin
[PROOF STATE]
proof (prove)
using this:
0 < xmin \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) \<noteq> s (local.adverse z i j \<triangleright> xmin) \<or> s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) \<noteq> s (local.adverse z i j \<triangleright> xmin))
?x < xmin \<Longrightarrow> \<not> (0 < ?x \<and> \<not> (s (e_snoc (local.adverse z i j \<triangleright> ?x) 0) \<noteq> s (local.adverse z i j \<triangleright> ?x) \<or> s (e_snoc (local.adverse z i j \<triangleright> ?x) 1) \<noteq> s (local.adverse z i j \<triangleright> ?x)))

goal (1 subgoal):
 1. s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) = s (local.adverse z i j \<triangleright> xmin) &&& s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) = s (local.adverse z i j \<triangleright> xmin)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) = s (local.adverse z i j \<triangleright> xmin)
s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) = s (local.adverse z i j \<triangleright> xmin)

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.adverse 0 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 0
local.adverse 1 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 1
s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) = s (local.adverse z i j \<triangleright> xmin)
s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) = s (local.adverse z i j \<triangleright> xmin)
[PROOF STEP]
have
    "s ((adverse 0 i j) \<triangleright> (Suc xmin)) = s ((adverse z i j) \<triangleright> xmin)"
    "s ((adverse 1 i j) \<triangleright> (Suc xmin)) = s ((adverse z i j) \<triangleright> xmin)"
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 0
local.adverse 1 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 1
s (e_snoc (local.adverse z i j \<triangleright> xmin) 0) = s (local.adverse z i j \<triangleright> xmin)
s (e_snoc (local.adverse z i j \<triangleright> xmin) 1) = s (local.adverse z i j \<triangleright> xmin)

goal (1 subgoal):
 1. s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin) &&& s (local.adverse 1 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin)
s (local.adverse 1 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin)

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin)
s (local.adverse 1 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin)
[PROOF STEP]
have
    "s ((adverse 0 i j) \<triangleright> (Suc xmin)) = s ((adverse 1 i j) \<triangleright> (Suc xmin))"
[PROOF STATE]
proof (prove)
using this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin)
s (local.adverse 1 i j \<triangleright> Suc xmin) = s (local.adverse z i j \<triangleright> xmin)

goal (1 subgoal):
 1. s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse 1 i j \<triangleright> Suc xmin)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse 1 i j \<triangleright> Suc xmin)

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse 1 i j \<triangleright> Suc xmin)

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
have "(adverse 0 i j) \<triangleright> (Suc xmin) \<noteq> (adverse 1 i j) \<triangleright> (Suc xmin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse 0 i j \<triangleright> Suc xmin \<noteq> local.adverse 1 i j \<triangleright> Suc xmin
[PROOF STEP]
using a0 a1 i0 i1
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 i j (Suc xmin) \<down>= 0
local.adverse 1 i j (Suc xmin) \<down>= 1
local.adverse 0 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 0
local.adverse 1 i j \<triangleright> Suc xmin = e_snoc (local.adverse z i j \<triangleright> xmin) 1

goal (1 subgoal):
 1. local.adverse 0 i j \<triangleright> Suc xmin \<noteq> local.adverse 1 i j \<triangleright> Suc xmin
[PROOF STEP]
by (metis append1_eq_conv list_decode_encode zero_neq_one)
[PROOF STATE]
proof (state)
this:
local.adverse 0 i j \<triangleright> Suc xmin \<noteq> local.adverse 1 i j \<triangleright> Suc xmin

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse 1 i j \<triangleright> Suc xmin)
local.adverse 0 i j \<triangleright> Suc xmin \<noteq> local.adverse 1 i j \<triangleright> Suc xmin
[PROOF STEP]
show "\<not> learn_cons \<phi> {adverse 0 i j, adverse 1 i j} s"
[PROOF STATE]
proof (prove)
using this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse 1 i j \<triangleright> Suc xmin)
local.adverse 0 i j \<triangleright> Suc xmin \<noteq> local.adverse 1 i j \<triangleright> Suc xmin

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
using same_hyp_different_init_not_cons
[PROOF STATE]
proof (prove)
using this:
s (local.adverse 0 i j \<triangleright> Suc xmin) = s (local.adverse 1 i j \<triangleright> Suc xmin)
local.adverse 0 i j \<triangleright> Suc xmin \<noteq> local.adverse 1 i j \<triangleright> Suc xmin
\<lbrakk>?f \<in> ?U; ?g \<in> ?U; ?f \<triangleright> ?n \<noteq> ?g \<triangleright> ?n; ?s (?f \<triangleright> ?n) = ?s (?g \<triangleright> ?n)\<rbrakk> \<Longrightarrow> \<not> learn_cons \<phi> ?U ?s

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> learn_cons \<phi> {local.adverse 0 i j, local.adverse 1 i j} s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma V01_not_in_R_cons: "\<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
obtain m n where
    mn0: "adverse 0 m n \<in> V\<^sub>0\<^sub>1" and
    mn1: "adverse 1 m n \<in> V\<^sub>0\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>local.adverse 0 m n \<in> V\<^sub>0\<^sub>1; local.adverse 1 m n \<in> V\<^sub>0\<^sub>1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using adverse_in_V01
[PROOF STATE]
proof (prove)
using this:
\<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>local.adverse 0 m n \<in> V\<^sub>0\<^sub>1; local.adverse 1 m n \<in> V\<^sub>0\<^sub>1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.adverse 0 m n \<in> V\<^sub>0\<^sub>1
local.adverse 1 m n \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
show "\<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
proof (cases "\<forall>x>0. hyp_change 0 m n x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
 2. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)

goal (2 subgoals):
 1. \<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
 2. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)
[PROOF STEP]
have "\<not> learn_lim \<phi> {adverse 0 m n} s"
[PROOF STATE]
proof (prove)
using this:
\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)

goal (1 subgoal):
 1. \<not> learn_lim \<phi> {local.adverse 0 m n} s
[PROOF STEP]
using always_hyp_change_no_lim
[PROOF STATE]
proof (prove)
using this:
\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)
\<forall>x>0. s (e_snoc (local.adverse ?z ?i ?j \<triangleright> x) 0) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> x) \<or> s (e_snoc (local.adverse ?z ?i ?j \<triangleright> x) 1) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> x) \<Longrightarrow> \<not> learn_lim \<phi> {local.adverse ?z ?i ?j} s

goal (1 subgoal):
 1. \<not> learn_lim \<phi> {local.adverse 0 m n} s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> learn_lim \<phi> {local.adverse 0 m n} s

goal (2 subgoals):
 1. \<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
 2. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
with mn0
[PROOF STATE]
proof (chain)
picking this:
local.adverse 0 m n \<in> V\<^sub>0\<^sub>1
\<not> learn_lim \<phi> {local.adverse 0 m n} s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 m n \<in> V\<^sub>0\<^sub>1
\<not> learn_lim \<phi> {local.adverse 0 m n} s

goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
using learn_cons_def learn_lim_closed_subseteq
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 m n \<in> V\<^sub>0\<^sub>1
\<not> learn_lim \<phi> {local.adverse 0 m n} s
learn_cons ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n k. k \<le> n \<longrightarrow> ?\<psi> (the (?s (f \<triangleright> n))) k = f k)
\<lbrakk>learn_lim ?\<psi> ?U ?s; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> learn_lim ?\<psi> ?V ?s

goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s

goal (1 subgoal):
 1. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))

goal (1 subgoal):
 1. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))
[PROOF STEP]
obtain x where x: "x > 0" "\<not> hyp_change 0 m n x"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>0 < x; \<not> (s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x
\<not> (s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))

goal (1 subgoal):
 1. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < x
\<not> (s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))
[PROOF STEP]
have "\<not> learn_cons \<phi> {adverse 0 m n, adverse 1 m n} s"
[PROOF STATE]
proof (prove)
using this:
0 < x
\<not> (s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 m n, local.adverse 1 m n} s
[PROOF STEP]
using no_hyp_change_no_cons[OF x]
[PROOF STATE]
proof (prove)
using this:
0 < x
\<not> (s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x))
\<not> learn_cons \<phi> {local.adverse 0 m n, local.adverse 1 m n} s

goal (1 subgoal):
 1. \<not> learn_cons \<phi> {local.adverse 0 m n, local.adverse 1 m n} s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> learn_cons \<phi> {local.adverse 0 m n, local.adverse 1 m n} s

goal (1 subgoal):
 1. \<not> (\<forall>x>0. s (e_snoc (local.adverse 0 m n \<triangleright> x) 0) \<noteq> s (local.adverse 0 m n \<triangleright> x) \<or> s (e_snoc (local.adverse 0 m n \<triangleright> x) 1) \<noteq> s (local.adverse 0 m n \<triangleright> x)) \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
with mn0 mn1
[PROOF STATE]
proof (chain)
picking this:
local.adverse 0 m n \<in> V\<^sub>0\<^sub>1
local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
\<not> learn_cons \<phi> {local.adverse 0 m n, local.adverse 1 m n} s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 m n \<in> V\<^sub>0\<^sub>1
local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
\<not> learn_cons \<phi> {local.adverse 0 m n, local.adverse 1 m n} s

goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
using learn_cons_closed_subseteq
[PROOF STATE]
proof (prove)
using this:
local.adverse 0 m n \<in> V\<^sub>0\<^sub>1
local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
\<not> learn_cons \<phi> {local.adverse 0 m n, local.adverse 1 m n} s
\<lbrakk>learn_cons ?\<psi> ?U ?s; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> learn_cons ?\<psi> ?V ?s

goal (1 subgoal):
 1. \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> learn_cons \<phi> V\<^sub>0\<^sub>1 s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_parallel': "eval r_parallel [i, j, x] = parallel i j x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_parallel [i, j, x] = parallel i j x
[PROOF STEP]
using parallel_def
[PROOF STATE]
proof (prove)
using this:
parallel ?i ?j ?x \<equiv> eval r_parallel [?i, ?j, ?x]

goal (1 subgoal):
 1. eval r_parallel [i, j, x] = parallel i j x
[PROOF STEP]
by simp


[STATEMENT]
lemma r_parallel'':
  shows "eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>"
    and "eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow>
      eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x]))"
    and "eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow>
      eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))"
    and "eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow>
      eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or>
      eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>) &&& (eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])))) &&& (eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))) &&& (eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x])))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>
 2. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x]))
 3. eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
 4. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
[PROOF STEP]
let ?f = "Cn 1 r_phi [r_const i, Id 1 0]"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>
 2. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x]))
 3. eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
 4. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
[PROOF STEP]
let ?g = "Cn 1 r_phi [r_const j, Id 1 0]"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>
 2. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x]))
 3. eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
 4. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
[PROOF STEP]
have *: "\<And>x. eval r_phi [i, x] = eval ?f [x]" "\<And>x. eval r_phi [j, x] = eval ?g [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. eval r_phi [i, x] = eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [x]) &&& (\<And>x. eval r_phi [j, x] = eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [x])
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
eval r_phi [i, ?x] = eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [?x]
eval r_phi [j, ?x] = eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [?x]

goal (4 subgoals):
 1. eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>
 2. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x]))
 3. eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
 4. eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
[PROOF STEP]
show "eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>"
    and "eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow>
      eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x]))"
    and "eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow>
      eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))"
    and "eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow>
      eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or>
      eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>) &&& (eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])))) &&& (eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))) &&& (eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x])))
[PROOF STEP]
using r_parallel[OF *]
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [?x] \<up> \<and> eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [?x] \<up> \<Longrightarrow> eval r_parallel [i, j, ?x] \<up>
eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [?x] \<down> \<and> eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [?x] \<up> \<Longrightarrow> eval r_parallel [i, j, ?x] \<down>= prod_encode (0, the (eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [?x]))
eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [?x] \<down> \<and> eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [?x] \<up> \<Longrightarrow> eval r_parallel [i, j, ?x] \<down>= prod_encode (1, the (eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [?x]))
eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [?x] \<down> \<and> eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [?x] \<down> \<Longrightarrow> eval r_parallel [i, j, ?x] \<down>= prod_encode (0, the (eval (Cn 1 r_phi [r_const i, recf.Id 1 0]) [?x])) \<or> eval r_parallel [i, j, ?x] \<down>= prod_encode (1, the (eval (Cn 1 r_phi [r_const j, recf.Id 1 0]) [?x]))

goal (1 subgoal):
 1. ((eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>) &&& (eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])))) &&& (eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))) &&& (eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x])))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
eval r_phi [i, x] \<up> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<up>
eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x]))
eval r_phi [j, x] \<down> \<and> eval r_phi [i, x] \<up> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))
eval r_phi [i, x] \<down> \<and> eval r_phi [j, x] \<down> \<Longrightarrow> eval r_parallel [i, j, x] \<down>= prod_encode (0, the (eval r_phi [i, x])) \<or> eval r_parallel [i, j, x] \<down>= prod_encode (1, the (eval r_phi [j, x]))

goal:
No subgoals!
[PROOF STEP]
qed