[STATEMENT]
lemma sv01_converg_V01:
  assumes "f \<in> V\<^sub>0\<^sub>1"
  shows "s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
 2. n \<noteq> 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
 2. n \<noteq> 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
using assms sv01 R1_imp_total1 auxhyp_in_R1
[PROOF STATE]
proof (prove)
using this:
n = 0
f \<in> V\<^sub>0\<^sub>1
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0
?f \<in> \<R> \<Longrightarrow> total1 ?f
auxhyp \<in> \<R>

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
case n_gr_0: False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
proof (cases "inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
 2. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n

goal (2 subgoals):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
 2. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
using n_gr_0 assms sv01
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n
n \<noteq> 0
f \<in> V\<^sub>0\<^sub>1
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)
[PROOF STEP]
have "the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n"
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
[PROOF STEP]
using assms inconsist_bounded inconsist_for_V01 length_init
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)
f \<in> V\<^sub>0\<^sub>1
inconsist ?i ?e \<down> \<Longrightarrow> the (inconsist ?i ?e) \<le> e_length ?e
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?k = amalg01 ?f\<rbrakk> \<Longrightarrow> inconsist ?k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> ?k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> ?k x \<down>\<noteq> e_nth ?e x else e_length ?e)
e_length (?f \<triangleright> ?n) = Suc ?n

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
[PROOF STEP]
by (metis (no_types, lifting) le_neq_implies_less option.collapse option.simps(3))
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
using n_gr_0 assms sv01 R1_imp_total1 total1E V01_def
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
n \<noteq> 0
f \<in> V\<^sub>0\<^sub>1
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0
?f \<in> \<R> \<Longrightarrow> total1 ?f
total1 ?f \<Longrightarrow> ?f ?x \<down>
V\<^sub>0\<^sub>1 = {f \<in> \<R>. \<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f}

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>
[PROOF STEP]
by (metis (no_types, lifting) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sv01_consistent_V01:
  assumes "f \<in> V\<^sub>0\<^sub>1"
  shows "\<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
have "s\<^bsub>01\<^esub> (f \<triangleright> n) = auxhyp (f \<triangleright> n)"
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = auxhyp (f \<triangleright> n)
[PROOF STEP]
using sv01[OF assms]
[PROOF STATE]
proof (prove)
using this:
n = 0
s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
\<lbrakk>?n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> ?n) \<down>= amalg01 f
\<lbrakk>?n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> ?n) = f 1
\<lbrakk>?n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> ?n) = f 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = auxhyp (f \<triangleright> n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = auxhyp (f \<triangleright> n)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = auxhyp (f \<triangleright> n)
[PROOF STEP]
have "\<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) = prenum (f \<triangleright> n)"
[PROOF STATE]
proof (prove)
using this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = auxhyp (f \<triangleright> n)

goal (1 subgoal):
 1. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) = prenum (f \<triangleright> n)
[PROOF STEP]
using auxhyp_prenum
[PROOF STATE]
proof (prove)
using this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = auxhyp (f \<triangleright> n)
\<phi> (the (auxhyp ?e)) = prenum ?e

goal (1 subgoal):
 1. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) = prenum (f \<triangleright> n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) = prenum (f \<triangleright> n)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) = prenum (f \<triangleright> n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) = prenum (f \<triangleright> n)

goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
using R1_imp_total1 total1E assms
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) = prenum (f \<triangleright> n)
?f \<in> \<R> \<Longrightarrow> total1 ?f
total1 ?f \<Longrightarrow> ?f ?x \<down>
f \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
by (simp add: V01_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
case n_gr_0: False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
let ?m = "amalg01 f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
let ?e = "f \<triangleright> n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
let ?c = "the (inconsist ?m ?e)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
have c: "inconsist ?m ?e \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<down>
[PROOF STEP]
using assms inconsist_for_V01
[PROOF STATE]
proof (prove)
using this:
f \<in> V\<^sub>0\<^sub>1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?k = amalg01 ?f\<rbrakk> \<Longrightarrow> inconsist ?k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> ?k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> ?k x \<down>\<noteq> e_nth ?e x else e_length ?e)

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<down>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
proof (cases "inconsist ?m ?e \<down>= Suc n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n

goal (2 subgoals):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n

goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
using assms n_gr_0 sv01 R1_imp_total1 total1E V01_def is_init_of_def
        inconsist_consistent not_initial_imp_not_eq length_init inconsist_converg_eq
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n
f \<in> V\<^sub>0\<^sub>1
n \<noteq> 0
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0
?f \<in> \<R> \<Longrightarrow> total1 ?f
total1 ?f \<Longrightarrow> ?f ?x \<down>
V\<^sub>0\<^sub>1 = {f \<in> \<R>. \<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f}
is_init_of ?t ?f \<equiv> \<forall>i<e_length ?t. ?f i \<down>= e_nth ?t i
inconsist ?i ?e \<down> \<Longrightarrow> (inconsist ?i ?e \<down>= e_length ?e) = (\<forall>x<e_length ?e. \<phi> ?i x \<down>= e_nth ?e x)
\<lbrakk>\<And>x. x < Suc ?n \<Longrightarrow> ?f x \<down>; \<not> is_init_of (?f \<triangleright> ?n) ?g\<rbrakk> \<Longrightarrow> ?f \<noteq> ?g
e_length (?f \<triangleright> ?n) = Suc ?n
inconsist ?i ?e \<down>= e_length ?e \<Longrightarrow> \<forall>x<e_length ?e. \<phi> ?i x \<down>= e_nth ?e x

goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
by (metis (no_types, lifting) le_imp_less_Suc mem_Collect_eq option.sel)
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)
[PROOF STEP]
have less: "the (inconsist ?m ?e) < Suc n"
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
[PROOF STEP]
using c assms inconsist_bounded inconsist_for_V01 length_init
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n)
inconsist (amalg01 f) (f \<triangleright> n) \<down>
f \<in> V\<^sub>0\<^sub>1
inconsist ?i ?e \<down> \<Longrightarrow> the (inconsist ?i ?e) \<le> e_length ?e
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?k = amalg01 ?f\<rbrakk> \<Longrightarrow> inconsist ?k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> ?k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> ?k x \<down>\<noteq> e_nth ?e x else e_length ?e)
e_length (?f \<triangleright> ?n) = Suc ?n

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
[PROOF STEP]
by (metis le_neq_implies_less option.collapse)
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
[PROOF STEP]
have "the (inconsist ?m ?e) < e_length ?e"
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n)

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n)
[PROOF STEP]
have
      "\<exists>x<e_length ?e. \<phi> ?m x \<down>\<noteq> e_nth ?e x"
      "inconsist ?m ?e \<down>= (LEAST x. x < e_length ?e \<and> \<phi> ?m x \<down>\<noteq> e_nth ?e x)"
      (is "_ \<down>= Least ?P")
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n)

goal (1 subgoal):
 1. \<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x &&& inconsist (amalg01 f) (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)
[PROOF STEP]
using inconsist_converg_less[OF c]
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n)
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n) \<Longrightarrow> \<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n) \<Longrightarrow> inconsist (amalg01 f) (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)

goal (1 subgoal):
 1. \<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x &&& inconsist (amalg01 f) (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x
inconsist (amalg01 f) (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x
inconsist (amalg01 f) (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)
[PROOF STEP]
have "?P ?c" and "\<And>x. x < ?c \<Longrightarrow> \<not> ?P x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x
inconsist (amalg01 f) (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>\<noteq> e_nth (f \<triangleright> n) (the (inconsist (amalg01 f) (f \<triangleright> n))) &&& (\<And>x. x < the (inconsist (amalg01 f) (f \<triangleright> n)) \<Longrightarrow> \<not> (x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x))
[PROOF STEP]
using LeastI_ex[of ?P] not_less_Least[of _ ?P]
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x
inconsist (amalg01 f) (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)
\<exists>x<e_length (f \<triangleright> n). \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x \<Longrightarrow> (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x) < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x) \<down>\<noteq> e_nth (f \<triangleright> n) (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x)
?k < (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x) \<Longrightarrow> \<not> (?k < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) ?k \<down>\<noteq> e_nth (f \<triangleright> n) ?k)

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>\<noteq> e_nth (f \<triangleright> n) (the (inconsist (amalg01 f) (f \<triangleright> n))) &&& (\<And>x. x < the (inconsist (amalg01 f) (f \<triangleright> n)) \<Longrightarrow> \<not> (x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) x \<down>\<noteq> e_nth (f \<triangleright> n) x))
[PROOF STEP]
by (auto simp del: e_nth)
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>\<noteq> e_nth (f \<triangleright> n) (the (inconsist (amalg01 f) (f \<triangleright> n)))
?x < the (inconsist (amalg01 f) (f \<triangleright> n)) \<Longrightarrow> \<not> (?x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) ?x \<down>\<noteq> e_nth (f \<triangleright> n) ?x)

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>\<noteq> e_nth (f \<triangleright> n) (the (inconsist (amalg01 f) (f \<triangleright> n)))
?x < the (inconsist (amalg01 f) (f \<triangleright> n)) \<Longrightarrow> \<not> (?x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) ?x \<down>\<noteq> e_nth (f \<triangleright> n) ?x)
[PROOF STEP]
have "\<phi> ?m ?c \<noteq> f ?c"
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n)) < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>\<noteq> e_nth (f \<triangleright> n) (the (inconsist (amalg01 f) (f \<triangleright> n)))
?x < the (inconsist (amalg01 f) (f \<triangleright> n)) \<Longrightarrow> \<not> (?x < e_length (f \<triangleright> n) \<and> \<phi> (amalg01 f) ?x \<down>\<noteq> e_nth (f \<triangleright> n) ?x)

goal (1 subgoal):
 1. \<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
have "amalgamation (the (f 0)) (the (f 1)) ?c \<noteq> f ?c"
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. amalgamation (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
using amalgamate
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalg01 f) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
\<phi> (amalgamate ?i ?j) = amalgamation ?i ?j

goal (1 subgoal):
 1. amalgamation (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
amalgamation (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
amalgamation (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
have *: "Some (pdec2 (the (parallel (the (f 0)) (the (f 1)) ?c))) \<noteq> f ?c"
[PROOF STATE]
proof (prove)
using this:
amalgamation (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. Some (pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
using amalgamation_def
[PROOF STATE]
proof (prove)
using this:
amalgamation (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
amalgamation ?i ?j ?x \<equiv> if parallel ?i ?j ?x \<up> then None else Some (pdec2 (the (parallel ?i ?j ?x)))

goal (1 subgoal):
 1. Some (pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
by (metis assms parallel_converg_V01)
[PROOF STATE]
proof (state)
this:
Some (pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
let ?p = "parallel (the (f 0)) (the (f 1)) ?c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n) \<noteq> Some (Suc n) \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
proof (cases "pdec1 (the ?p) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0

goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0
[PROOF STEP]
have "\<phi> (the (f 0)) ?c \<down>= pdec2 (the ?p)"
[PROOF STATE]
proof (prove)
using this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0

goal (1 subgoal):
 1. \<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
using assms parallel_0 parallel_converg_V01
[PROOF STATE]
proof (prove)
using this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0
f \<in> V\<^sub>0\<^sub>1
parallel ?i ?j ?x \<down>= prod_encode (0, ?v) \<Longrightarrow> \<phi> ?i ?x \<down>= ?v
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> parallel (the (?f 0)) (the (?f 1)) ?x \<down>

goal (1 subgoal):
 1. \<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
by (metis option.collapse prod.collapse prod_decode_inverse)
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))

goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
have "\<phi> (the (f 0)) ?c \<noteq> f ?c"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))

goal (1 subgoal):
 1. \<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
Some (pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. \<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
have "\<phi> (the (f 0)) \<noteq> f"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. \<phi> (the (f 0)) \<noteq> f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 0)) \<noteq> f

goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 0)) \<noteq> f
[PROOF STEP]
have "\<phi> (the (f 1)) = f"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) \<noteq> f

goal (1 subgoal):
 1. \<phi> (the (f 1)) = f
[PROOF STEP]
using assms V01_def
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) \<noteq> f
f \<in> V\<^sub>0\<^sub>1
V\<^sub>0\<^sub>1 = {f \<in> \<R>. \<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f}

goal (1 subgoal):
 1. \<phi> (the (f 1)) = f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 1)) = f

goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 1)) = f

goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
have "s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
[PROOF STEP]
using True less n_gr_0 sv01 assms
[PROOF STATE]
proof (prove)
using this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
n \<noteq> 0
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0
f \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1

goal (2 subgoals):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
 2. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 1)) = f
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 1)) = f
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1

goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0
[PROOF STEP]
have "pdec1 (the ?p) = 1"
[PROOF STATE]
proof (prove)
using this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 1
[PROOF STEP]
by (meson assms parallel_converg_V01 parallel_converg_pdec1_0_or_1)
[PROOF STATE]
proof (state)
this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 1

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 1
[PROOF STEP]
have "\<phi> (the (f 1)) ?c \<down>= pdec2 (the ?p)"
[PROOF STATE]
proof (prove)
using this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 1

goal (1 subgoal):
 1. \<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
using assms parallel_1 parallel_converg_V01
[PROOF STATE]
proof (prove)
using this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 1
f \<in> V\<^sub>0\<^sub>1
parallel ?i ?j ?x \<down>= prod_encode (1, ?v) \<Longrightarrow> \<phi> ?j ?x \<down>= ?v
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> parallel (the (?f 0)) (the (?f 1)) ?x \<down>

goal (1 subgoal):
 1. \<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
by (metis option.collapse prod.collapse prod_decode_inverse)
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
have "\<phi> (the (f 1)) ?c \<noteq> f ?c"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))

goal (1 subgoal):
 1. \<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<down>= pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
Some (pdec2 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. \<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
have "\<phi> (the (f 1)) \<noteq> f"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))) \<noteq> f (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. \<phi> (the (f 1)) \<noteq> f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 1)) \<noteq> f

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 1)) \<noteq> f
[PROOF STEP]
have "\<phi> (the (f 0)) = f"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 1)) \<noteq> f

goal (1 subgoal):
 1. \<phi> (the (f 0)) = f
[PROOF STEP]
using assms V01_def
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 1)) \<noteq> f
f \<in> V\<^sub>0\<^sub>1
V\<^sub>0\<^sub>1 = {f \<in> \<R>. \<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f}

goal (1 subgoal):
 1. \<phi> (the (f 0)) = f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 0)) = f

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (the (f 0)) = f

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
from False less n_gr_0 sv01 assms
[PROOF STATE]
proof (chain)
picking this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
n \<noteq> 0
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0
f \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
have "s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0"
[PROOF STATE]
proof (prove)
using this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
n \<noteq> 0
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0
f \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow> \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 0)) = f
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) = f
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0

goal (1 subgoal):
 1. \<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) x = f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sv01_limit_V01:
 assumes "f \<in> V\<^sub>0\<^sub>1"
 shows "\<exists>i. \<forall>\<^sup>\<infinity>n. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
proof (cases "\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalgamate (the (f 0)) (the (f 1))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
 2. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f

goal (2 subgoals):
 1. \<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
 2. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
by (meson less_le_trans zero_less_one)
[PROOF STATE]
proof (state)
this:
\<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f)

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f)
[PROOF STEP]
obtain n\<^sub>0 where n0:
    "n\<^sub>0 \<noteq> 0"
    "s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f)

goal (1 subgoal):
 1. (\<And>n\<^sub>0. \<lbrakk>n\<^sub>0 \<noteq> 0; s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>f \<in> V\<^sub>0\<^sub>1\<close> sv01_converg_V01
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f)
f \<in> V\<^sub>0\<^sub>1
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>

goal (1 subgoal):
 1. (\<And>n\<^sub>0. \<lbrakk>n\<^sub>0 \<noteq> 0; s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n\<^sub>0 \<noteq> 0
s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>0 \<noteq> 0
s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f
[PROOF STEP]
have *: "the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0"
      (is "the (inconsist ?m (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0")
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 \<noteq> 0
s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0
[PROOF STEP]
using assms \<open>n\<^sub>0 \<noteq> 0\<close> sv01(2) inconsist_bounded inconsist_for_V01 length_init
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 \<noteq> 0
s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f
f \<in> V\<^sub>0\<^sub>1
n\<^sub>0 \<noteq> 0
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
inconsist ?i ?e \<down> \<Longrightarrow> the (inconsist ?i ?e) \<le> e_length ?e
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?k = amalg01 ?f\<rbrakk> \<Longrightarrow> inconsist ?k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> ?k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> ?k x \<down>\<noteq> e_nth ?e x else e_length ?e)
e_length (?f \<triangleright> ?n) = Suc ?n

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0
[PROOF STEP]
by (metis (no_types, lifting) le_neq_implies_less option.collapse option.simps(3))
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
have "f \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> \<R>
[PROOF STEP]
using assms V01_def
[PROOF STATE]
proof (prove)
using this:
f \<in> V\<^sub>0\<^sub>1
V\<^sub>0\<^sub>1 = {f \<in> \<R>. \<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f}

goal (1 subgoal):
 1. f \<in> \<R>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> \<R>

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> \<R>

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
have "\<phi> ?m \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (amalg01 f) \<in> \<R>
[PROOF STEP]
using amalgamate amalgamation_V01_R1 assms
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate ?i ?j) = amalgamation ?i ?j
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> amalgamation (the (?f 0)) (the (?f 1)) \<in> \<R>
f \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. \<phi> (amalg01 f) \<in> \<R>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (amalg01 f) \<in> \<R>

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (amalg01 f) \<in> \<R>

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
have "inconsist ?m (f \<triangleright> n\<^sub>0) \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n\<^sub>0) \<down>
[PROOF STEP]
using inconsist_for_V01 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?k = amalg01 ?f\<rbrakk> \<Longrightarrow> inconsist ?k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> ?k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> ?k x \<down>\<noteq> e_nth ?e x else e_length ?e)
f \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> n\<^sub>0) \<down>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inconsist (amalg01 f) (f \<triangleright> n\<^sub>0) \<down>

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0
f \<in> \<R>
\<phi> (amalg01 f) \<in> \<R>
inconsist (amalg01 f) (f \<triangleright> n\<^sub>0) \<down>
[PROOF STEP]
have **: "inconsist ?m (f \<triangleright> (n\<^sub>0 + m)) = inconsist ?m (f \<triangleright> n\<^sub>0)" for m
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0
f \<in> \<R>
\<phi> (amalg01 f) \<in> \<R>
inconsist (amalg01 f) (f \<triangleright> n\<^sub>0) \<down>

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + m)) = inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)
[PROOF STEP]
using inconsist_init_converg_less[of f ?m]
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0
f \<in> \<R>
\<phi> (amalg01 f) \<in> \<R>
inconsist (amalg01 f) (f \<triangleright> n\<^sub>0) \<down>
\<lbrakk>f \<in> \<R>; \<phi> (amalg01 f) \<in> \<R>; inconsist (amalg01 f) (f \<triangleright> ?n) \<down>; the (inconsist (amalg01 f) (f \<triangleright> ?n)) < Suc ?n\<rbrakk> \<Longrightarrow> inconsist (amalg01 f) (f \<triangleright> (?n + ?m)) = inconsist (amalg01 f) (f \<triangleright> ?n)

goal (1 subgoal):
 1. inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + m)) = inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)) = inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)) = inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)
[PROOF STEP]
have "the (inconsist ?m (f \<triangleright> (n\<^sub>0 + m))) < Suc n\<^sub>0 + m" for m
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)) = inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + m))) < Suc n\<^sub>0 + m
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)) = inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)
the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0

goal (1 subgoal):
 1. the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + m))) < Suc n\<^sub>0 + m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m))) < Suc n\<^sub>0 + ?m

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m))) < Suc n\<^sub>0 + ?m

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
have
    "pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist ?m (f \<triangleright> (n\<^sub>0 + m)))))) =
      pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist ?m (f \<triangleright> n\<^sub>0)))))"
    for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)))))
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)) = inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)

goal (1 subgoal):
 1. pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)))))

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)))))

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
have "n\<^sub>0 + m \<noteq> 0" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n\<^sub>0 + m \<noteq> 0
[PROOF STEP]
using \<open>n\<^sub>0 \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 \<noteq> 0

goal (1 subgoal):
 1. n\<^sub>0 + m \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n\<^sub>0 + ?m \<noteq> 0

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m))) < Suc n\<^sub>0 + ?m
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)))))
n\<^sub>0 + ?m \<noteq> 0
[PROOF STEP]
have "s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)" for m
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m))) < Suc n\<^sub>0 + ?m
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)))))
n\<^sub>0 + ?m \<noteq> 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)
[PROOF STEP]
using assms sv01 * \<open>n\<^sub>0 \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m))) < Suc n\<^sub>0 + ?m
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> (n\<^sub>0 + ?m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)))))
n\<^sub>0 + ?m \<noteq> 0
f \<in> V\<^sub>0\<^sub>1
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> 0) = auxhyp (?f \<triangleright> 0)
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; inconsist (amalg01 ?f) (?f \<triangleright> ?n) \<down>= Suc ?n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) \<down>= amalg01 ?f
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 1
\<lbrakk>?f \<in> V\<^sub>0\<^sub>1; ?n \<noteq> 0; the (inconsist (amalg01 ?f) (?f \<triangleright> ?n)) < Suc ?n; pdec1 (the (parallel (the (?f 0)) (the (?f 1)) (the (inconsist (amalg01 ?f) (?f \<triangleright> ?n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (?f \<triangleright> ?n) = ?f 0
the (inconsist (amalg01 f) (f \<triangleright> n\<^sub>0)) < Suc n\<^sub>0
n\<^sub>0 \<noteq> 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)
[PROOF STEP]
by (metis add_Suc)
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + ?m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + ?m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
define i where "i = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)"
[PROOF STATE]
proof (state)
this:
i = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + ?m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)
i = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)
[PROOF STEP]
have "\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) = i"
[PROOF STATE]
proof (prove)
using this:
s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + ?m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)
i = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)

goal (1 subgoal):
 1. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) = i
[PROOF STEP]
using nat_le_iff_add
[PROOF STATE]
proof (prove)
using this:
s\<^bsub>01\<^esub> (f \<triangleright> (n\<^sub>0 + ?m)) = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)
i = s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0)
(?m \<le> ?n) = (\<exists>k. ?n = ?m + k)

goal (1 subgoal):
 1. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) = i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) = i

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) = i
[PROOF STEP]
have "\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= the i"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) = i

goal (1 subgoal):
 1. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= the i
[PROOF STEP]
using n0(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) = i
s\<^bsub>01\<^esub> (f \<triangleright> n\<^sub>0) \<down>\<noteq> amalg01 f

goal (1 subgoal):
 1. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= the i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= the i

goal (1 subgoal):
 1. \<not> (\<forall>n>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f) \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= the i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= the i

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma V01_learn_cons: "learn_cons \<phi> V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. learn_cons \<phi> V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>
[PROOF STEP]
proof (rule learn_consI2)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. environment \<phi> V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>
 2. \<And>f. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
 3. \<And>f n. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<forall>k\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) k = f k
[PROOF STEP]
show "environment \<phi> V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. environment \<phi> V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>
[PROOF STEP]
by (simp add: Collect_mono V01_def phi_in_P2 sv01_in_P1 sv01_converg_V01)
[PROOF STATE]
proof (state)
this:
environment \<phi> V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>

goal (2 subgoals):
 1. \<And>f. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
 2. \<And>f n. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<forall>k\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) k = f k
[PROOF STEP]
show "\<And>f n. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<forall>k\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) k = f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f n. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<forall>k\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) k = f k
[PROOF STEP]
using sv01_consistent_V01
[PROOF STATE]
proof (prove)
using this:
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<forall>x\<le>?n. \<phi> (the (s\<^bsub>01\<^esub> (?f \<triangleright> ?n))) x = ?f x

goal (1 subgoal):
 1. \<And>f n. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<forall>k\<le>n. \<phi> (the (s\<^bsub>01\<^esub> (f \<triangleright> n))) k = f k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<forall>k\<le>?n. \<phi> (the (s\<^bsub>01\<^esub> (?f \<triangleright> ?n))) k = ?f k

goal (1 subgoal):
 1. \<And>f. f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
show "\<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i" if "f \<in> V\<^sub>0\<^sub>1" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
using sv01_limit_V01 that
[PROOF STATE]
proof (prove)
using this:
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (?f \<triangleright> n) \<down>= i
f \<in> V\<^sub>0\<^sub>1

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> \<exists>i n\<^sub>0. \<forall>n\<ge>n\<^sub>0. s\<^bsub>01\<^esub> (?f \<triangleright> n) \<down>= i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_lemma_R_for_CONS: "\<exists>U. U \<in> CONS \<and> (\<not> (\<exists>s. s \<in> \<R> \<and> learn_cons \<phi> U s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>U. U \<in> CONS \<and> (\<nexists>s. s \<in> \<R> \<and> learn_cons \<phi> U s)
[PROOF STEP]
using V01_in_CONS V01_not_in_R_cons
[PROOF STATE]
proof (prove)
using this:
V\<^sub>0\<^sub>1 \<in> CONS
?s \<in> \<R> \<Longrightarrow> \<not> learn_cons \<phi> V\<^sub>0\<^sub>1 ?s

goal (1 subgoal):
 1. \<exists>U. U \<in> CONS \<and> (\<nexists>s. s \<in> \<R> \<and> learn_cons \<phi> U s)
[PROOF STEP]
by auto


[STATEMENT]
lemma symm_preorder_is_equivalence:
  fixes Rel :: "('a \<times> 'a) set"
  assumes "preorder Rel"
      and "sym Rel"
  shows "equivalence Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivalence Rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
preorder Rel
sym Rel

goal (1 subgoal):
 1. equivalence Rel
[PROOF STEP]
unfolding preorder_on_def equiv_def
[PROOF STATE]
proof (prove)
using this:
refl Rel \<and> trans Rel
sym Rel

goal (1 subgoal):
 1. refl Rel \<and> sym Rel \<and> trans Rel
[PROOF STEP]
by simp


[STATEMENT]
lemma elem_of_symcl:
  fixes Rel :: "('a \<times> 'a) set"
    and a b :: "'a"
  assumes elem: "(a, b) \<in> Rel"
  shows "(a, b) \<in> symcl Rel"
    and "(b, a) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> symcl Rel &&& (b, a) \<in> symcl Rel
[PROOF STEP]
by (auto simp add: elem symcl_def)


[STATEMENT]
lemma sym_symcl:
  fixes Rel :: "('a \<times> 'a) set"
  shows "sym (symcl Rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (symcl Rel)
[PROOF STEP]
by (simp add: symcl_def sym_Un_converse)


[STATEMENT]
lemma refl_symm_closure_is_symm_refl_closure:
  fixes Rel :: "('a \<times> 'a) set"
  shows "symcl (Rel\<^sup>=) = (symcl Rel)\<^sup>="
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symcl (Rel\<^sup>=) = (symcl Rel)\<^sup>=
[PROOF STEP]
by (auto simp add: symcl_def refl)


[STATEMENT]
lemma refl_symcl_of_refl_rel:
  fixes Rel :: "('a \<times> 'a) set"
    and A   :: "'a set"
  assumes "refl_on A Rel"
  shows "refl_on A (symcl Rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on A (symcl Rel)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
refl_on A Rel

goal (1 subgoal):
 1. refl_on A (symcl Rel)
[PROOF STEP]
by (auto simp add: refl_on_def' symcl_def)


[STATEMENT]
lemma refl_symm_trans_closure_is_symm_refl_trans_closure:
  fixes Rel :: "('a \<times> 'a) set"
  shows "(symcl (Rel\<^sup>=))\<^sup>+ = (symcl Rel)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (symcl (Rel\<^sup>=))\<^sup>+ = (symcl Rel)\<^sup>*
[PROOF STEP]
using refl_symm_closure_is_symm_refl_closure[where Rel="Rel"]
[PROOF STATE]
proof (prove)
using this:
symcl (Rel\<^sup>=) = (symcl Rel)\<^sup>=

goal (1 subgoal):
 1. (symcl (Rel\<^sup>=))\<^sup>+ = (symcl Rel)\<^sup>*
[PROOF STEP]
by simp


[STATEMENT]
lemma sym_reflcl_of_symm_rel:
  fixes Rel :: "('a \<times> 'a) set"
  assumes "sym Rel"
  shows "sym (Rel\<^sup>=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (Rel\<^sup>=)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sym Rel

goal (1 subgoal):
 1. sym (Rel\<^sup>=)
[PROOF STEP]
by (simp add: sym_Id sym_Un)


[STATEMENT]
lemma reflcl_of_refl_rel:
  fixes Rel :: "('a \<times> 'a) set"
  assumes "refl Rel"
  shows "Rel\<^sup>= = Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel\<^sup>= = Rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
refl Rel

goal (1 subgoal):
 1. Rel\<^sup>= = Rel
[PROOF STEP]
unfolding refl_on_def
[PROOF STATE]
proof (prove)
using this:
Rel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> Rel)

goal (1 subgoal):
 1. Rel\<^sup>= = Rel
[PROOF STEP]
by auto


[STATEMENT]
lemma symm_closure_of_symm_rel:
  fixes Rel :: "('a \<times> 'a) set"
  assumes "sym Rel"
  shows "symcl Rel = Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symcl Rel = Rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sym Rel

goal (1 subgoal):
 1. symcl Rel = Rel
[PROOF STEP]
unfolding symcl_def sym_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. (x, y) \<in> Rel \<longrightarrow> (y, x) \<in> Rel

goal (1 subgoal):
 1. Rel \<union> Rel\<inverse> = Rel
[PROOF STEP]
by auto


[STATEMENT]
lemma rtrancl_of_preorder:
  fixes Rel :: "('a \<times> 'a) set"
  assumes "preorder Rel"
  shows "Rel\<^sup>* = Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel\<^sup>* = Rel
[PROOF STEP]
using assms reflcl_of_refl_rel[of Rel] trancl_id[of "Rel\<^sup>="] trancl_reflcl[of Rel]
[PROOF STATE]
proof (prove)
using this:
preorder Rel
refl Rel \<Longrightarrow> Rel\<^sup>= = Rel
trans (Rel\<^sup>=) \<Longrightarrow> (Rel\<^sup>=)\<^sup>+ = Rel\<^sup>=
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. Rel\<^sup>* = Rel
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
using this:
refl Rel \<and> trans Rel
refl Rel \<Longrightarrow> Rel\<^sup>= = Rel
trans (Rel\<^sup>=) \<Longrightarrow> (Rel\<^sup>=)\<^sup>+ = Rel\<^sup>=
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. Rel\<^sup>* = Rel
[PROOF STEP]
by auto


[STATEMENT]
lemma refl_trans_closure_subset_of_refl_symm_trans_closure:
  fixes Rel :: "('a \<times> 'a) set"
  shows "Rel\<^sup>* \<subseteq> (symcl (Rel\<^sup>=))\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel\<^sup>* \<subseteq> (symcl (Rel\<^sup>=))\<^sup>+
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> Rel\<^sup>* \<Longrightarrow> (a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> Rel\<^sup>* \<Longrightarrow> (a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+
[PROOF STEP]
assume "(a, b) \<in> Rel\<^sup>*"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel\<^sup>*

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> Rel\<^sup>* \<Longrightarrow> (a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+
[PROOF STEP]
hence "(a, b) \<in> (symcl Rel)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel\<^sup>*

goal (1 subgoal):
 1. (a, b) \<in> (symcl Rel)\<^sup>*
[PROOF STEP]
using in_rtrancl_UnI[of "(a, b)" "Rel" "Rel\<inverse>"]
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel\<^sup>*
(a, b) \<in> Rel\<^sup>* \<or> (a, b) \<in> (Rel\<inverse>)\<^sup>* \<Longrightarrow> (a, b) \<in> (Rel \<union> Rel\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (a, b) \<in> (symcl Rel)\<^sup>*
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (symcl Rel)\<^sup>*

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> Rel\<^sup>* \<Longrightarrow> (a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+
[PROOF STEP]
thus "(a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> (symcl Rel)\<^sup>*

goal (1 subgoal):
 1. (a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+
[PROOF STEP]
using refl_symm_trans_closure_is_symm_refl_trans_closure[of Rel]
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> (symcl Rel)\<^sup>*
(symcl (Rel\<^sup>=))\<^sup>+ = (symcl Rel)\<^sup>*

goal (1 subgoal):
 1. (a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (symcl (Rel\<^sup>=))\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma symm_relation_impl_preservation_equals_reflection:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> bool"
  assumes symm: "sym Rel"
  shows "rel_preserves_pred Rel Pred = rel_reflects_pred Rel Pred"
    and "rel_preserves_pred Rel Pred = rel_respects_pred Rel Pred"
    and "rel_reflects_pred Rel Pred = rel_respects_pred Rel Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_preserves_pred Rel Pred = rel_reflects_pred Rel Pred &&& rel_preserves_pred Rel Pred = rel_respects_pred Rel Pred &&& rel_reflects_pred Rel Pred = rel_respects_pred Rel Pred
[PROOF STEP]
using symm
[PROOF STATE]
proof (prove)
using this:
sym Rel

goal (1 subgoal):
 1. rel_preserves_pred Rel Pred = rel_reflects_pred Rel Pred &&& rel_preserves_pred Rel Pred = rel_respects_pred Rel Pred &&& rel_reflects_pred Rel Pred = rel_respects_pred Rel Pred
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. (x, y) \<in> Rel \<longrightarrow> (y, x) \<in> Rel

goal (1 subgoal):
 1. rel_preserves_pred Rel Pred = rel_reflects_pred Rel Pred &&& rel_preserves_pred Rel Pred = rel_respects_pred Rel Pred &&& rel_reflects_pred Rel Pred = rel_respects_pred Rel Pred
[PROOF STEP]
by blast+


[STATEMENT]
lemma symm_relation_impl_preservation_equals_reflection_of_binary_predicates:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  assumes symm: "sym Rel"
  shows "rel_preserves_binary_pred Rel Pred = rel_reflects_binary_pred Rel Pred"
    and "rel_preserves_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred"
    and "rel_reflects_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_preserves_binary_pred Rel Pred = rel_reflects_binary_pred Rel Pred &&& rel_preserves_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred &&& rel_reflects_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred
[PROOF STEP]
using symm
[PROOF STATE]
proof (prove)
using this:
sym Rel

goal (1 subgoal):
 1. rel_preserves_binary_pred Rel Pred = rel_reflects_binary_pred Rel Pred &&& rel_preserves_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred &&& rel_reflects_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. (x, y) \<in> Rel \<longrightarrow> (y, x) \<in> Rel

goal (1 subgoal):
 1. rel_preserves_binary_pred Rel Pred = rel_reflects_binary_pred Rel Pred &&& rel_preserves_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred &&& rel_reflects_binary_pred Rel Pred = rel_respects_binary_pred Rel Pred
[PROOF STEP]
by blast+


[STATEMENT]
lemma preservation_and_closures:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> bool"
  assumes preservation: "rel_preserves_pred Rel Pred"
  shows "rel_preserves_pred (Rel\<^sup>=) Pred"
    and "rel_preserves_pred (Rel\<^sup>+) Pred"
    and "rel_preserves_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_preserves_pred (Rel\<^sup>=) Pred &&& rel_preserves_pred (Rel\<^sup>+) Pred &&& rel_preserves_pred (Rel\<^sup>*) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_preserves_pred (Rel\<^sup>=) Pred
 2. rel_preserves_pred (Rel\<^sup>+) Pred
 3. rel_preserves_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from preservation
[PROOF STATE]
proof (chain)
picking this:
rel_preserves_pred Rel Pred
[PROOF STEP]
show A: "rel_preserves_pred (Rel\<^sup>=) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_preserves_pred Rel Pred

goal (1 subgoal):
 1. rel_preserves_pred (Rel\<^sup>=) Pred
[PROOF STEP]
by (auto simp add: refl)
[PROOF STATE]
proof (state)
this:
rel_preserves_pred (Rel\<^sup>=) Pred

goal (2 subgoals):
 1. rel_preserves_pred (Rel\<^sup>+) Pred
 2. rel_preserves_pred (Rel\<^sup>*) Pred
[PROOF STEP]
have B: "\<And>Rel. rel_preserves_pred Rel Pred \<Longrightarrow> rel_preserves_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_preserves_pred Rel Pred \<Longrightarrow> rel_preserves_pred (Rel\<^sup>+) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b. rel_preserves_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
fix Rel a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b. rel_preserves_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
assume "(a, b) \<in> Rel\<^sup>+" and "rel_preserves_pred Rel Pred" and "Pred a"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel\<^sup>+
rel_preserves_pred Rel Pred
Pred a

goal (1 subgoal):
 1. \<And>Rel a b. rel_preserves_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
thus "Pred b"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel\<^sup>+
rel_preserves_pred Rel Pred
Pred a

goal (1 subgoal):
 1. Pred b
[PROOF STEP]
by (induct, blast+)
[PROOF STATE]
proof (state)
this:
Pred b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_preserves_pred ?Rel Pred \<Longrightarrow> rel_preserves_pred (?Rel\<^sup>+) Pred

goal (2 subgoals):
 1. rel_preserves_pred (Rel\<^sup>+) Pred
 2. rel_preserves_pred (Rel\<^sup>*) Pred
[PROOF STEP]
with preservation
[PROOF STATE]
proof (chain)
picking this:
rel_preserves_pred Rel Pred
rel_preserves_pred ?Rel Pred \<Longrightarrow> rel_preserves_pred (?Rel\<^sup>+) Pred
[PROOF STEP]
show "rel_preserves_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_preserves_pred Rel Pred
rel_preserves_pred ?Rel Pred \<Longrightarrow> rel_preserves_pred (?Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_preserves_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_preserves_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_preserves_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from preservation A B[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_preserves_pred Rel Pred
rel_preserves_pred (Rel\<^sup>=) Pred
rel_preserves_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_preserves_pred ((Rel\<^sup>=)\<^sup>+) Pred
[PROOF STEP]
show "rel_preserves_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_preserves_pred Rel Pred
rel_preserves_pred (Rel\<^sup>=) Pred
rel_preserves_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_preserves_pred ((Rel\<^sup>=)\<^sup>+) Pred

goal (1 subgoal):
 1. rel_preserves_pred (Rel\<^sup>*) Pred
[PROOF STEP]
using trancl_reflcl[of Rel]
[PROOF STATE]
proof (prove)
using this:
rel_preserves_pred Rel Pred
rel_preserves_pred (Rel\<^sup>=) Pred
rel_preserves_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_preserves_pred ((Rel\<^sup>=)\<^sup>+) Pred
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. rel_preserves_pred (Rel\<^sup>*) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_preserves_pred (Rel\<^sup>*) Pred

goal:
No subgoals!
[PROOF STEP]
qed