[STATEMENT]
lemma parallel:
  "\<phi> i x \<up> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<up>"
  "\<phi> i x \<down> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (0, the (\<phi> i x))"
  "\<phi> j x \<down> \<and> \<phi> i x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (1, the (\<phi> j x))"
  "\<phi> i x \<down> \<and> \<phi> j x \<down> \<Longrightarrow>
     parallel i j x \<down>= prod_encode (0, the (\<phi> i x)) \<or>
     parallel i j x \<down>= prod_encode (1, the (\<phi> j x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<phi> i x \<up> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<up>) &&& (\<phi> i x \<down> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (0, the (\<phi> i x)))) &&& (\<phi> j x \<down> \<and> \<phi> i x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (1, the (\<phi> j x))) &&& (\<phi> i x \<down> \<and> \<phi> j x \<down> \<Longrightarrow> parallel i j x \<down>= prod_encode (0, the (\<phi> i x)) \<or> parallel i j x \<down>= prod_encode (1, the (\<phi> j x)))
[PROOF STEP]
using phi_def r_parallel'' r_parallel parallel_def
[PROOF STATE]
proof (prove)
using this:
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]
eval r_phi [?i, ?x] \<up> \<and> eval r_phi [?j, ?x] \<up> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<up>
eval r_phi [?i, ?x] \<down> \<and> eval r_phi [?j, ?x] \<up> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (0, the (eval r_phi [?i, ?x]))
eval r_phi [?j, ?x] \<down> \<and> eval r_phi [?i, ?x] \<up> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (1, the (eval r_phi [?j, ?x]))
eval r_phi [?i, ?x] \<down> \<and> eval r_phi [?j, ?x] \<down> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (0, the (eval r_phi [?i, ?x])) \<or> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (1, the (eval r_phi [?j, ?x]))
\<lbrakk>\<And>x. eval r_phi [?i, x] = eval ?f [x]; \<And>x. eval r_phi [?j, x] = eval ?g [x]; eval ?f [?x] \<up> \<and> eval ?g [?x] \<up>\<rbrakk> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<up>
\<lbrakk>\<And>x. eval r_phi [?i, x] = eval ?f [x]; \<And>x. eval r_phi [?j, x] = eval ?g [x]; eval ?f [?x] \<down> \<and> eval ?g [?x] \<up>\<rbrakk> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (0, the (eval ?f [?x]))
\<lbrakk>\<And>x. eval r_phi [?i, x] = eval ?f [x]; \<And>x. eval r_phi [?j, x] = eval ?g [x]; eval ?g [?x] \<down> \<and> eval ?f [?x] \<up>\<rbrakk> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (1, the (eval ?g [?x]))
\<lbrakk>\<And>x. eval r_phi [?i, x] = eval ?f [x]; \<And>x. eval r_phi [?j, x] = eval ?g [x]; eval ?f [?x] \<down> \<and> eval ?g [?x] \<down>\<rbrakk> \<Longrightarrow> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (0, the (eval ?f [?x])) \<or> eval r_parallel [?i, ?j, ?x] \<down>= prod_encode (1, the (eval ?g [?x]))
parallel ?i ?j ?x \<equiv> eval r_parallel [?i, ?j, ?x]

goal (1 subgoal):
 1. ((\<phi> i x \<up> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<up>) &&& (\<phi> i x \<down> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (0, the (\<phi> i x)))) &&& (\<phi> j x \<down> \<and> \<phi> i x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (1, the (\<phi> j x))) &&& (\<phi> i x \<down> \<and> \<phi> j x \<down> \<Longrightarrow> parallel i j x \<down>= prod_encode (0, the (\<phi> i x)) \<or> parallel i j x \<down>= prod_encode (1, the (\<phi> j x)))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma parallel_converg_pdec1_0_or_1:
  assumes "parallel i j x \<down>"
  shows "pdec1 (the (parallel i j x)) = 0 \<or> pdec1 (the (parallel i j x)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdec1 (the (parallel i j x)) = 0 \<or> pdec1 (the (parallel i j x)) = 1
[PROOF STEP]
using assms parallel[of i x j] parallel(3)[of j x i]
[PROOF STATE]
proof (prove)
using this:
parallel i j x \<down>
\<phi> i x \<up> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<up>
\<phi> i x \<down> \<and> \<phi> j x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (0, the (\<phi> i x))
\<phi> i x \<down> \<and> \<phi> j x \<up> \<Longrightarrow> parallel j i x \<down>= prod_encode (1, the (\<phi> i x))
\<phi> i x \<down> \<and> \<phi> j x \<down> \<Longrightarrow> parallel i j x \<down>= prod_encode (0, the (\<phi> i x)) \<or> parallel i j x \<down>= prod_encode (1, the (\<phi> j x))
\<phi> j x \<down> \<and> \<phi> i x \<up> \<Longrightarrow> parallel i j x \<down>= prod_encode (1, the (\<phi> j x))

goal (1 subgoal):
 1. pdec1 (the (parallel i j x)) = 0 \<or> pdec1 (the (parallel i j x)) = 1
[PROOF STEP]
by (metis fst_eqD option.sel prod_encode_inverse)


[STATEMENT]
lemma parallel_converg_either: "(\<phi> i x \<down> \<or> \<phi> j x \<down>) = (parallel i j x \<down>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<phi> i x \<down> \<or> \<phi> j x \<down>) = (parallel i j x \<down>)
[PROOF STEP]
using parallel
[PROOF STATE]
proof (prove)
using this:
\<phi> ?i ?x \<up> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<up>
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x))
\<phi> ?j ?x \<down> \<and> \<phi> ?i ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<down> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x)) \<or> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))

goal (1 subgoal):
 1. (\<phi> i x \<down> \<or> \<phi> j x \<down>) = (parallel i j x \<down>)
[PROOF STEP]
by (metis option.simps(3))


[STATEMENT]
lemma parallel_0:
  assumes "parallel i j x \<down>= prod_encode (0, v)"
  shows "\<phi> i x \<down>= v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i x \<down>= v
[PROOF STEP]
using parallel assms
[PROOF STATE]
proof (prove)
using this:
\<phi> ?i ?x \<up> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<up>
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x))
\<phi> ?j ?x \<down> \<and> \<phi> ?i ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<down> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x)) \<or> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))
parallel i j x \<down>= prod_encode (0, v)

goal (1 subgoal):
 1. \<phi> i x \<down>= v
[PROOF STEP]
by (smt option.collapse option.sel option.simps(3) prod.inject prod_encode_eq zero_neq_one)


[STATEMENT]
lemma parallel_1:
  assumes "parallel i j x \<down>= prod_encode (1, v)"
  shows "\<phi> j x \<down>= v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> j x \<down>= v
[PROOF STEP]
using parallel assms
[PROOF STATE]
proof (prove)
using this:
\<phi> ?i ?x \<up> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<up>
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x))
\<phi> ?j ?x \<down> \<and> \<phi> ?i ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<down> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x)) \<or> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))
parallel i j x \<down>= prod_encode (1, v)

goal (1 subgoal):
 1. \<phi> j x \<down>= v
[PROOF STEP]
by (smt option.collapse option.sel option.simps(3) prod.inject prod_encode_eq zero_neq_one)


[STATEMENT]
lemma parallel_converg_V01:
  assumes "f \<in> V\<^sub>0\<^sub>1"
  shows "parallel (the (f 0)) (the (f 1)) x \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parallel (the (f 0)) (the (f 1)) x \<down>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. parallel (the (f 0)) (the (f 1)) x \<down>
[PROOF STEP]
have "f \<in> \<R> \<and> (\<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> \<R> \<and> (\<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f)
[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> \<and> (\<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> \<R> \<and> (\<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f)

goal (1 subgoal):
 1. parallel (the (f 0)) (the (f 1)) x \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> \<R> \<and> (\<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f)
[PROOF STEP]
have "\<phi> (the (f 0)) \<in> \<R> \<or> \<phi> (the (f 1)) \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R> \<and> (\<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f)

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

goal (1 subgoal):
 1. parallel (the (f 0)) (the (f 1)) x \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 0)) \<in> \<R> \<or> \<phi> (the (f 1)) \<in> \<R>
[PROOF STEP]
have "\<phi> (the (f 0)) x \<down> \<or> \<phi> (the (f 1)) x \<down>"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) \<in> \<R> \<or> \<phi> (the (f 1)) \<in> \<R>

goal (1 subgoal):
 1. \<phi> (the (f 0)) x \<down> \<or> \<phi> (the (f 1)) x \<down>
[PROOF STEP]
using R1_imp_total1
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) \<in> \<R> \<or> \<phi> (the (f 1)) \<in> \<R>
?f \<in> \<R> \<Longrightarrow> total1 ?f

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

goal (1 subgoal):
 1. parallel (the (f 0)) (the (f 1)) x \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f 0)) x \<down> \<or> \<phi> (the (f 1)) x \<down>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) x \<down> \<or> \<phi> (the (f 1)) x \<down>

goal (1 subgoal):
 1. parallel (the (f 0)) (the (f 1)) x \<down>
[PROOF STEP]
using parallel_converg_either
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f 0)) x \<down> \<or> \<phi> (the (f 1)) x \<down>
(\<phi> ?i ?x \<down> \<or> \<phi> ?j ?x \<down>) = (parallel ?i ?j ?x \<down>)

goal (1 subgoal):
 1. parallel (the (f 0)) (the (f 1)) x \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
parallel (the (f 0)) (the (f 1)) x \<down>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma amalgamation_diverg: "amalgamation i j x \<up> \<longleftrightarrow> \<phi> i x \<up> \<and> \<phi> j x \<up>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (amalgamation i j x \<up>) = (\<phi> i x \<up> \<and> \<phi> j x \<up>)
[PROOF STEP]
using amalgamation_def parallel
[PROOF STATE]
proof (prove)
using this:
amalgamation ?i ?j ?x \<equiv> if parallel ?i ?j ?x \<up> then None else Some (pdec2 (the (parallel ?i ?j ?x)))
\<phi> ?i ?x \<up> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<up>
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x))
\<phi> ?j ?x \<down> \<and> \<phi> ?i ?x \<up> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))
\<phi> ?i ?x \<down> \<and> \<phi> ?j ?x \<down> \<Longrightarrow> parallel ?i ?j ?x \<down>= prod_encode (0, the (\<phi> ?i ?x)) \<or> parallel ?i ?j ?x \<down>= prod_encode (1, the (\<phi> ?j ?x))

goal (1 subgoal):
 1. (amalgamation i j x \<up>) = (\<phi> i x \<up> \<and> \<phi> j x \<up>)
[PROOF STEP]
by (metis option.simps(3))


[STATEMENT]
lemma amalgamation_total:
  assumes "total1 (\<phi> i) \<or> total1 (\<phi> j)"
  shows "total1 (amalgamation i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total1 (amalgamation i j)
[PROOF STEP]
using assms amalgamation_diverg[of i j] total_def
[PROOF STATE]
proof (prove)
using this:
total1 (\<phi> i) \<or> total1 (\<phi> j)
(amalgamation i j ?x \<up>) = (\<phi> i ?x \<up> \<and> \<phi> j ?x \<up>)
Partial_Recursive.total ?f \<equiv> \<forall>xs. length xs = arity ?f \<longrightarrow> eval ?f xs \<down>

goal (1 subgoal):
 1. total1 (amalgamation i j)
[PROOF STEP]
by auto


[STATEMENT]
lemma amalgamation_V01_total:
  assumes "f \<in> V\<^sub>0\<^sub>1"
  shows "total1 (amalgamation (the (f 0)) (the (f 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total1 (amalgamation (the (f 0)) (the (f 1)))
[PROOF STEP]
using assms V01_def amalgamation_total R1_imp_total1 total1_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}
total1 (\<phi> ?i) \<or> total1 (\<phi> ?j) \<Longrightarrow> total1 (amalgamation ?i ?j)
?f \<in> \<R> \<Longrightarrow> total1 ?f
total1 ?f \<equiv> \<forall>x. ?f x \<down>

goal (1 subgoal):
 1. total1 (amalgamation (the (f 0)) (the (f 1)))
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq)


[STATEMENT]
lemma r_amalgamation_recfn: "recfn 3 r_amalgamation"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 3 r_amalgamation
[PROOF STEP]
unfolding r_amalgamation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 3 (Cn 3 r_pdec2 [r_parallel])
[PROOF STEP]
by simp


[STATEMENT]
lemma r_amalgamation: "eval r_amalgamation [i, j, x] = amalgamation i j x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
proof (cases "parallel i j x \<up>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. parallel i j x \<up> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
 2. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
parallel i j x \<up>

goal (2 subgoals):
 1. parallel i j x \<up> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
 2. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
parallel i j x \<up>
[PROOF STEP]
have "eval r_parallel [i, j, x] \<up>"
[PROOF STATE]
proof (prove)
using this:
parallel i j x \<up>

goal (1 subgoal):
 1. eval r_parallel [i, j, x] \<up>
[PROOF STEP]
by (simp add: r_parallel')
[PROOF STATE]
proof (state)
this:
eval r_parallel [i, j, x] \<up>

goal (2 subgoals):
 1. parallel i j x \<up> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
 2. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_parallel [i, j, x] \<up>
[PROOF STEP]
have "eval r_amalgamation [i, j, x] \<up>"
[PROOF STATE]
proof (prove)
using this:
eval r_parallel [i, j, x] \<up>

goal (1 subgoal):
 1. eval r_amalgamation [i, j, x] \<up>
[PROOF STEP]
unfolding r_amalgamation_def
[PROOF STATE]
proof (prove)
using this:
eval r_parallel [i, j, x] \<up>

goal (1 subgoal):
 1. eval (Cn 3 r_pdec2 [r_parallel]) [i, j, x] \<up>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_amalgamation [i, j, x] \<up>

goal (2 subgoals):
 1. parallel i j x \<up> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
 2. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval r_amalgamation [i, j, x] \<up>

goal (2 subgoals):
 1. parallel i j x \<up> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
 2. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
parallel i j x \<up>
[PROOF STEP]
have "amalgamation i j x \<up>"
[PROOF STATE]
proof (prove)
using this:
parallel i j x \<up>

goal (1 subgoal):
 1. amalgamation i j x \<up>
[PROOF STEP]
using amalgamation_def
[PROOF STATE]
proof (prove)
using this:
parallel i j x \<up>
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. amalgamation i j x \<up>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
amalgamation i j x \<up>

goal (2 subgoals):
 1. parallel i j x \<up> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
 2. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval r_amalgamation [i, j, x] \<up>
amalgamation i j x \<up>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval r_amalgamation [i, j, x] \<up>
amalgamation i j x \<up>

goal (1 subgoal):
 1. eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_amalgamation [i, j, x] = amalgamation i j x

goal (1 subgoal):
 1. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
parallel i j x \<down>

goal (1 subgoal):
 1. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
parallel i j x \<down>
[PROOF STEP]
have "eval r_parallel [i, j, x] \<down>"
[PROOF STATE]
proof (prove)
using this:
parallel i j x \<down>

goal (1 subgoal):
 1. eval r_parallel [i, j, x] \<down>
[PROOF STEP]
by (simp add: r_parallel')
[PROOF STATE]
proof (state)
this:
eval r_parallel [i, j, x] \<down>

goal (1 subgoal):
 1. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_parallel [i, j, x] \<down>
[PROOF STEP]
have "eval r_amalgamation [i, j, x] = eval r_pdec2 [the (eval r_parallel [i, j, x])]"
[PROOF STATE]
proof (prove)
using this:
eval r_parallel [i, j, x] \<down>

goal (1 subgoal):
 1. eval r_amalgamation [i, j, x] = eval r_pdec2 [the (eval r_parallel [i, j, x])]
[PROOF STEP]
unfolding r_amalgamation_def
[PROOF STATE]
proof (prove)
using this:
eval r_parallel [i, j, x] \<down>

goal (1 subgoal):
 1. eval (Cn 3 r_pdec2 [r_parallel]) [i, j, x] = eval r_pdec2 [the (eval r_parallel [i, j, x])]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_amalgamation [i, j, x] = eval r_pdec2 [the (eval r_parallel [i, j, x])]

goal (1 subgoal):
 1. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval r_amalgamation [i, j, x] = eval r_pdec2 [the (eval r_parallel [i, j, x])]

goal (1 subgoal):
 1. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
have "... \<down>= pdec2 (the (eval r_parallel [i, j, x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_pdec2 [the (eval r_parallel [i, j, x])] \<down>= pdec2 (the (eval r_parallel [i, j, x]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_pdec2 [the (eval r_parallel [i, j, x])] \<down>= pdec2 (the (eval r_parallel [i, j, x]))

goal (1 subgoal):
 1. parallel i j x \<down> \<Longrightarrow> eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval r_amalgamation [i, j, x] \<down>= pdec2 (the (eval r_parallel [i, j, x]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval r_amalgamation [i, j, x] \<down>= pdec2 (the (eval r_parallel [i, j, x]))

goal (1 subgoal):
 1. eval r_amalgamation [i, j, x] = amalgamation i j x
[PROOF STEP]
by (simp add: False amalgamation_def r_parallel')
[PROOF STATE]
proof (state)
this:
eval r_amalgamation [i, j, x] = amalgamation i j x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma amalgamate: "\<phi> (amalgamate i j) = amalgamation i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (amalgamate i j) = amalgamation i j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
have "\<phi> (amalgamate i j) x = eval r_phi [amalgamate i j, x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (amalgamate i j) x = eval r_phi [amalgamate i j, x]
[PROOF STEP]
by (simp add: phi_def)
[PROOF STATE]
proof (state)
this:
\<phi> (amalgamate i j) x = eval r_phi [amalgamate i j, x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (amalgamate i j) x = eval r_phi [amalgamate i j, x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
have "... = eval r_phi [smn 1 (encode r_amalgamation) [i, j], x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_phi [amalgamate i j, x] = eval r_phi [smn 1 (encode r_amalgamation) [i, j], x]
[PROOF STEP]
using amalgamate_def
[PROOF STATE]
proof (prove)
using this:
amalgamate ?i ?j \<equiv> smn 1 (encode r_amalgamation) [?i, ?j]

goal (1 subgoal):
 1. eval r_phi [amalgamate i j, x] = eval r_phi [smn 1 (encode r_amalgamation) [i, j], x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_phi [amalgamate i j, x] = eval r_phi [smn 1 (encode r_amalgamation) [i, j], x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval r_phi [amalgamate i j, x] = eval r_phi [smn 1 (encode r_amalgamation) [i, j], x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
have "... = eval r_phi
     [encode (Cn 1 (r_universal 3)
      (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (Id 1) [0])), x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_phi [smn 1 (encode r_amalgamation) [i, j], x] = eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (recf.Id 1) [0])), x]
[PROOF STEP]
using smn[of 1 "encode r_amalgamation" "[i, j]"]
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> smn 1 (encode r_amalgamation) [i, j] = encode (Cn 1 (r_universal (1 + length [i, j])) (r_constn (1 - 1) (encode r_amalgamation) # map (r_constn (1 - 1)) [i, j] @ map (recf.Id 1) [0..<1]))

goal (1 subgoal):
 1. eval r_phi [smn 1 (encode r_amalgamation) [i, j], x] = eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (recf.Id 1) [0])), x]
[PROOF STEP]
by (simp add: numeral_3_eq_3)
[PROOF STATE]
proof (state)
this:
eval r_phi [smn 1 (encode r_amalgamation) [i, j], x] = eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (recf.Id 1) [0])), x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval r_phi [smn 1 (encode r_amalgamation) [i, j], x] = eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (recf.Id 1) [0])), x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
have "... = eval r_phi
     [encode (Cn 1 (r_universal 3)
      (r_const (encode r_amalgamation) # [r_const i, r_const j, Id 1 0])), x]"
     (is "... = eval r_phi [encode ?f, x]")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (recf.Id 1) [0])), x] = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]
[PROOF STEP]
by (simp add: r_constn_def)
[PROOF STATE]
proof (state)
this:
eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (recf.Id 1) [0])), x] = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<phi> (amalgamate i j) x = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]
[PROOF STEP]
have "\<phi> (amalgamate i j) x = eval r_phi
     [encode (Cn 1 (r_universal 3)
      (r_const (encode r_amalgamation) # [r_const i, r_const j, Id 1 0])), x]"
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate i j) x = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]

goal (1 subgoal):
 1. \<phi> (amalgamate i j) x = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<phi> (amalgamate i j) x = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (amalgamate i j) x = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]
[PROOF STEP]
have "\<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]"
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate i j) x = eval r_phi [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]

goal (1 subgoal):
 1. \<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]
[PROOF STEP]
unfolding r_phi_def
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate i j) x = eval (r_universal 1) [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]

goal (1 subgoal):
 1. \<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]
[PROOF STEP]
using r_universal[of ?f 1] r_amalgamation_recfn
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate i j) x = eval (r_universal 1) [encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]), x]
\<lbrakk>recfn 1 (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]); length ?xs = 1\<rbrakk> \<Longrightarrow> eval (r_universal 1) (encode (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]) # ?xs) = eval (Cn 1 (r_universal 3) [r_const (encode r_amalgamation), r_const i, r_const j, recf.Id 1 0]) ?xs
recfn 3 r_amalgamation

goal (1 subgoal):
 1. \<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]

goal (1 subgoal):
 1. \<And>x. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]
[PROOF STEP]
show "\<phi> (amalgamate i j) x = amalgamation i j x"
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]

goal (1 subgoal):
 1. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
using r_amalgamation
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]
eval r_amalgamation [?i, ?j, ?x] = amalgamation ?i ?j ?x

goal (1 subgoal):
 1. \<phi> (amalgamate i j) x = amalgamation i j x
[PROOF STEP]
by (simp add: r_amalgamation_recfn r_universal)
[PROOF STATE]
proof (state)
this:
\<phi> (amalgamate i j) x = amalgamation i j x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma amalgamation_in_P1: "amalgamation i j \<in> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. amalgamation i j \<in> \

[PROOF STEP]
using amalgamate
[PROOF STATE]
proof (prove)
using this:
\<phi> (amalgamate ?i ?j) = amalgamation ?i ?j

goal (1 subgoal):
 1. amalgamation i j \<in> \

[PROOF STEP]
by (metis P2_proj_P1 phi_in_P2)


[STATEMENT]
lemma amalgamation_V01_R1:
  assumes "f \<in> V\<^sub>0\<^sub>1"
  shows "amalgamation (the (f 0)) (the (f 1)) \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. amalgamation (the (f 0)) (the (f 1)) \<in> \<R>
[PROOF STEP]
using assms amalgamation_V01_total amalgamation_in_P1
[PROOF STATE]
proof (prove)
using this:
f \<in> V\<^sub>0\<^sub>1
?f \<in> V\<^sub>0\<^sub>1 \<Longrightarrow> total1 (amalgamation (the (?f 0)) (the (?f 1)))
amalgamation ?i ?j \<in> \<P>

goal (1 subgoal):
 1. amalgamation (the (f 0)) (the (f 1)) \<in> \<R>
[PROOF STEP]
by (simp add: P1_total_imp_R1)


[STATEMENT]
lemma r_amalgamate_recfn: "recfn 2 r_amalgamate"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 r_amalgamate
[PROOF STEP]
unfolding r_amalgamate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r_amalgamation)), recf.Id 2 0, recf.Id 2 1])
[PROOF STEP]
by simp


[STATEMENT]
lemma r_amalgamate: "eval r_amalgamate [i, j] \<down>= amalgamate i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
let ?p = "encode r_amalgamation"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
have rs21: "eval (r_smn 1 2) [?p, i, j] \<down>= smn 1 ?p [i, j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (r_smn 1 2) [encode r_amalgamation, i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]
[PROOF STEP]
using r_smn
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?n; length ?cs = ?m\<rbrakk> \<Longrightarrow> eval (r_smn ?n ?m) (?p # ?cs) \<down>= smn ?n ?p ?cs

goal (1 subgoal):
 1. eval (r_smn 1 2) [encode r_amalgamation, i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_smn 1 2) [encode r_amalgamation, i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]

goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval (r_smn 1 2) [encode r_amalgamation, i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]

goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
have "eval r_amalgamate [i, j] = eval (r_smn 1 2) [?p, i, j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_amalgamate [i, j] = eval (r_smn 1 2) [encode r_amalgamation, i, j]
[PROOF STEP]
unfolding r_amalgamate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r_amalgamation)), recf.Id 2 0, recf.Id 2 1]) [i, j] = eval (r_smn 1 2) [encode r_amalgamation, i, j]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval r_amalgamate [i, j] = eval (r_smn 1 2) [encode r_amalgamation, i, j]

goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval (r_smn 1 2) [encode r_amalgamation, i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]
eval r_amalgamate [i, j] = eval (r_smn 1 2) [encode r_amalgamation, i, j]
[PROOF STEP]
have "eval r_amalgamate [i, j] \<down>= smn 1 ?p [i, j]"
[PROOF STATE]
proof (prove)
using this:
eval (r_smn 1 2) [encode r_amalgamation, i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]
eval r_amalgamate [i, j] = eval (r_smn 1 2) [encode r_amalgamation, i, j]

goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_amalgamate [i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]

goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_amalgamate [i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval r_amalgamate [i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]

goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
using amalgamate_def
[PROOF STATE]
proof (prove)
using this:
eval r_amalgamate [i, j] \<down>= smn 1 (encode r_amalgamation) [i, j]
amalgamate ?i ?j \<equiv> smn 1 (encode r_amalgamation) [?i, ?j]

goal (1 subgoal):
 1. eval r_amalgamate [i, j] \<down>= amalgamate i j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_amalgamate [i, j] \<down>= amalgamate i j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inconsist_converg:
  assumes "inconsist i e \<down>"
  shows "inconsist i e =
    (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
     then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)
     else Some (e_length e))"
    and "\<forall>x<e_length e. \<phi> i x \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsist i e = (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) &&& \<forall>x<e_length e. \<phi> i x \<down>
[PROOF STEP]
using inconsist_def assms
[PROOF STATE]
proof (prove)
using this:
inconsist ?i ?e \<equiv> if \<exists>x<e_length ?e. \<phi> ?i x \<up> then None else if \<exists>x<e_length ?e. \<phi> ?i x \<down>\<noteq> e_nth ?e x then Some (LEAST x. x < e_length ?e \<and> \<phi> ?i x \<down>\<noteq> e_nth ?e x) else Some (e_length ?e)
inconsist i e \<down>

goal (1 subgoal):
 1. inconsist i e = (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) &&& \<forall>x<e_length e. \<phi> i x \<down>
[PROOF STEP]
by (presburger, meson)


[STATEMENT]
lemma inconsist_bounded:
  assumes "inconsist i e \<down>"
  shows "the (inconsist i e) \<le> e_length e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (inconsist i e) \<le> e_length e
[PROOF STEP]
proof (cases "\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x \<Longrightarrow> the (inconsist i e) \<le> e_length e
 2. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> the (inconsist i e) \<le> e_length e
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x

goal (2 subgoals):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x \<Longrightarrow> the (inconsist i e) \<le> e_length e
 2. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> the (inconsist i e) \<le> e_length e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x

goal (1 subgoal):
 1. the (inconsist i e) \<le> e_length e
[PROOF STEP]
using inconsist_converg[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
inconsist i e = (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
\<forall>x<e_length e. \<phi> i x \<down>

goal (1 subgoal):
 1. the (inconsist i e) \<le> e_length e
[PROOF STEP]
by (smt Least_le dual_order.strict_implies_order dual_order.strict_trans2 option.sel)
[PROOF STATE]
proof (state)
this:
the (inconsist i e) \<le> e_length e

goal (1 subgoal):
 1. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> the (inconsist i e) \<le> e_length e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> the (inconsist i e) \<le> e_length e
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> the (inconsist i e) \<le> e_length e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. the (inconsist i e) \<le> e_length e
[PROOF STEP]
using inconsist_converg[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)
inconsist i e = (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
\<forall>x<e_length e. \<phi> i x \<down>

goal (1 subgoal):
 1. the (inconsist i e) \<le> e_length e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (inconsist i e) \<le> e_length e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inconsist_consistent:
  assumes "inconsist i e \<down>"
  shows "inconsist i e \<down>= e_length e \<longleftrightarrow> (\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inconsist i e \<down>= e_length e) = (\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inconsist i e \<down>= e_length e \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
 2. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x \<Longrightarrow> inconsist i e \<down>= e_length e
[PROOF STEP]
show "\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x" if "inconsist i e \<down>= e_length e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
proof (cases "\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
 2. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x

goal (2 subgoals):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
 2. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x

goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
using that inconsist_converg[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
inconsist i e \<down>= e_length e
inconsist i e = (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
\<forall>x<e_length e. \<phi> i x \<down>

goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
by (metis (mono_tags, lifting) not_less_Least option.inject)
[PROOF STATE]
proof (state)
this:
\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x

goal (1 subgoal):
 1. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. \<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x) \<Longrightarrow> \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
using that inconsist_converg[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x)
inconsist i e \<down>= e_length e
inconsist i e = (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
\<forall>x<e_length e. \<phi> i x \<down>

goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
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<e_length e. \<phi> i x \<down>= e_nth e x \<Longrightarrow> inconsist i e \<down>= e_length e
[PROOF STEP]
show "\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x \<Longrightarrow> inconsist i e \<down>= e_length e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x \<Longrightarrow> inconsist i e \<down>= e_length e
[PROOF STEP]
unfolding inconsist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x \<Longrightarrow> (if \<exists>x<e_length e. \<phi> i x \<up> then None else if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= e_length e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inconsist i e \<down>

goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x \<Longrightarrow> (if \<exists>x<e_length e. \<phi> i x \<up> then None else if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= e_length e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x \<Longrightarrow> inconsist i e \<down>= e_length e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inconsist_converg_eq:
  assumes "inconsist i e \<down>= e_length e"
  shows "\<forall>x<e_length e. \<phi> i x \<down>= e_nth e x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
using assms inconsist_consistent
[PROOF STATE]
proof (prove)
using this:
inconsist i e \<down>= e_length e
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)

goal (1 subgoal):
 1. \<forall>x<e_length e. \<phi> i x \<down>= e_nth e x
[PROOF STEP]
by auto


[STATEMENT]
lemma inconsist_converg_less:
  assumes "inconsist i e \<down>" and "the (inconsist i e) < e_length e"
  shows "\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x"
    and "inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x &&& inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
 2. inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
show "\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inconsist i e \<down>
the (inconsist i e) < e_length e

goal (1 subgoal):
 1. \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
by (metis (no_types, lifting) inconsist_converg(1) nat_neq_iff option.sel)
[PROOF STATE]
proof (state)
this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x

goal (1 subgoal):
 1. inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
show "inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x

goal (1 subgoal):
 1. inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
using assms inconsist_converg
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
inconsist i e \<down>
the (inconsist i e) < e_length e
inconsist ?i ?e \<down> \<Longrightarrow> inconsist ?i ?e = (if \<exists>x<e_length ?e. \<phi> ?i x \<down>\<noteq> e_nth ?e x then Some (LEAST x. x < e_length ?e \<and> \<phi> ?i x \<down>\<noteq> e_nth ?e x) else Some (e_length ?e))
inconsist ?i ?e \<down> \<Longrightarrow> \<forall>x<e_length ?e. \<phi> ?i x \<down>

goal (1 subgoal):
 1. inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
inconsist i e \<down>= (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_bounded_Suc:
  assumes "\<exists>x. x < upper \<and> P x"
  shows "(LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
let ?Q = "\<lambda>x. x < upper \<and> P x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
let ?x = "Least ?Q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<upper. P x
[PROOF STEP]
have "?x < upper \<and> P ?x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<upper. P x

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) < upper \<and> P (LEAST x. x < upper \<and> P x)
[PROOF STEP]
using LeastI_ex[of ?Q]
[PROOF STATE]
proof (prove)
using this:
\<exists>x<upper. P x
\<exists>x<upper. P x \<Longrightarrow> (LEAST x. x < upper \<and> P x) < upper \<and> P (LEAST x. x < upper \<and> P x)

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) < upper \<and> P (LEAST x. x < upper \<and> P x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) < upper \<and> P (LEAST x. x < upper \<and> P x)

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(LEAST x. x < upper \<and> P x) < upper \<and> P (LEAST x. x < upper \<and> P x)
[PROOF STEP]
have 1: "?x < Suc upper \<and> P ?x"
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < upper \<and> P x) < upper \<and> P (LEAST x. x < upper \<and> P x)

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<upper. P x
[PROOF STEP]
have 2: "\<forall>y<?x. \<not> P y"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<upper. P x

goal (1 subgoal):
 1. \<forall>y<LEAST x. x < upper \<and> P x. \<not> P y
[PROOF STEP]
using Least_le[of ?Q] not_less_Least
[PROOF STATE]
proof (prove)
using this:
\<exists>x<upper. P x
?k < upper \<and> P ?k \<Longrightarrow> (LEAST x. x < upper \<and> P x) \<le> ?k
?k < (LEAST x. ?P x) \<Longrightarrow> \<not> ?P ?k

goal (1 subgoal):
 1. \<forall>y<LEAST x. x < upper \<and> P x. \<not> P y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>y<LEAST x. x < upper \<and> P x. \<not> P y

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
have "(LEAST x. x < Suc upper \<and> P x) = ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST x. x < Suc upper \<and> P x) = (LEAST x. x < upper \<and> P x)
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)
 2. \<And>y. y < Suc upper \<and> P y \<Longrightarrow> (LEAST x. x < upper \<and> P x) \<le> y
[PROOF STEP]
show "?x < Suc upper \<and> P ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)
\<forall>y<LEAST x. x < upper \<and> P x. \<not> P y

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)

goal (1 subgoal):
 1. \<And>y. y < Suc upper \<and> P y \<Longrightarrow> (LEAST x. x < upper \<and> P x) \<le> y
[PROOF STEP]
show "\<And>y. y < Suc upper \<and> P y \<Longrightarrow> ?x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y < Suc upper \<and> P y \<Longrightarrow> (LEAST x. x < upper \<and> P x) \<le> y
[PROOF STEP]
using 1 2 leI
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < upper \<and> P x) < Suc upper \<and> P (LEAST x. x < upper \<and> P x)
\<forall>y<LEAST x. x < upper \<and> P x. \<not> P y
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x

goal (1 subgoal):
 1. \<And>y. y < Suc upper \<and> P y \<Longrightarrow> (LEAST x. x < upper \<and> P x) \<le> y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?y < Suc upper \<and> P ?y \<Longrightarrow> (LEAST x. x < upper \<and> P x) \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST x. x < Suc upper \<and> P x) = (LEAST x. x < upper \<and> P x)

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(LEAST x. x < Suc upper \<and> P x) = (LEAST x. x < upper \<and> P x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < Suc upper \<and> P x) = (LEAST x. x < upper \<and> P x)

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < Suc upper \<and> P x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_bounded_gr:
  fixes P :: "nat \<Rightarrow> bool" and m :: nat
  assumes "\<exists>x. x < upper \<and> P x"
  shows "(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x)
[PROOF STEP]
proof (induction m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + 0 \<and> P x)
 2. \<And>m. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x) \<Longrightarrow> (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + 0 \<and> P x)
 2. \<And>m. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x) \<Longrightarrow> (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + 0 \<and> P x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + 0 \<and> P x)

goal (1 subgoal):
 1. \<And>m. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x) \<Longrightarrow> (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x) \<Longrightarrow> (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x)

goal (1 subgoal):
 1. \<And>m. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x) \<Longrightarrow> (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x)

goal (1 subgoal):
 1. \<And>m. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x) \<Longrightarrow> (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
have "\<exists>x. x < upper + m \<and> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x<upper + m. P x
[PROOF STEP]
using assms trans_less_add1
[PROOF STATE]
proof (prove)
using this:
\<exists>x<upper. P x
?i < ?j \<Longrightarrow> ?i < ?j + ?m

goal (1 subgoal):
 1. \<exists>x<upper + m. P x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x<upper + m. P x

goal (1 subgoal):
 1. \<And>m. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x) \<Longrightarrow> (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x)
\<exists>x<upper + m. P x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x)
\<exists>x<upper + m. P x

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
using least_bounded_Suc
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + m \<and> P x)
\<exists>x<upper + m. P x
\<exists>x<?upper. ?P x \<Longrightarrow> (LEAST x. x < ?upper \<and> ?P x) = (LEAST x. x < Suc ?upper \<and> ?P x)

goal (1 subgoal):
 1. (LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST x. x < upper \<and> P x) = (LEAST x. x < upper + Suc m \<and> P x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inconsist_init_converg_less:
  assumes "f \<in> \<R>"
    and "\<phi> i \<in> \<R>"
    and "inconsist i (f \<triangleright> n) \<down>"
    and "the (inconsist i (f \<triangleright> n)) < Suc n"
  shows "inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
have phi_i_total: "\<phi> i x \<down>" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i x \<down>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
\<phi> i \<in> \<R>
inconsist i (f \<triangleright> n) \<down>
the (inconsist i (f \<triangleright> n)) < Suc n

goal (1 subgoal):
 1. \<phi> i x \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> i ?x \<down>

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> i ?x \<down>

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
have f_nth: "f x \<down>= e_nth (f \<triangleright> n) x" if "x < Suc n" for x n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<down>= e_nth (f \<triangleright> n) x
[PROOF STEP]
using that assms(1)
[PROOF STATE]
proof (prove)
using this:
x < Suc n
f \<in> \<R>

goal (1 subgoal):
 1. f x \<down>= e_nth (f \<triangleright> n) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x < Suc ?n \<Longrightarrow> f ?x \<down>= e_nth (f \<triangleright> ?n) ?x

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> i ?x \<down>
?x < Suc ?n \<Longrightarrow> f ?x \<down>= e_nth (f \<triangleright> ?n) ?x
[PROOF STEP]
have "(\<phi> i x \<noteq> f x) = (\<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x)" if "x < Suc n" for x n
[PROOF STATE]
proof (prove)
using this:
\<phi> i ?x \<down>
?x < Suc ?n \<Longrightarrow> f ?x \<down>= e_nth (f \<triangleright> ?n) ?x

goal (1 subgoal):
 1. (\<phi> i x \<noteq> f x) = (\<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<phi> i ?x \<down>
?x < Suc ?n \<Longrightarrow> f ?x \<down>= e_nth (f \<triangleright> ?n) ?x
x < Suc n

goal (1 subgoal):
 1. (\<phi> i x \<noteq> f x) = (\<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x < Suc ?n \<Longrightarrow> (\<phi> i ?x \<noteq> f ?x) = (\<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x < Suc ?n \<Longrightarrow> (\<phi> i ?x \<noteq> f ?x) = (\<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)
[PROOF STEP]
have cond: "(x < Suc n \<and> \<phi> i x \<noteq> f x) =
      (x < e_length (f \<triangleright> n) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x)" for x n
[PROOF STATE]
proof (prove)
using this:
?x < Suc ?n \<Longrightarrow> (\<phi> i ?x \<noteq> f ?x) = (\<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)

goal (1 subgoal):
 1. (x < Suc n \<and> \<phi> i x \<noteq> f x) = (x < e_length (f \<triangleright> n) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x)
[PROOF STEP]
using length_init
[PROOF STATE]
proof (prove)
using this:
?x < Suc ?n \<Longrightarrow> (\<phi> i ?x \<noteq> f ?x) = (\<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)
e_length (?f \<triangleright> ?n) = Suc ?n

goal (1 subgoal):
 1. (x < Suc n \<and> \<phi> i x \<noteq> f x) = (x < e_length (f \<triangleright> n) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(?x < Suc ?n \<and> \<phi> i ?x \<noteq> f ?x) = (?x < e_length (f \<triangleright> ?n) \<and> \<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?x < Suc ?n \<and> \<phi> i ?x \<noteq> f ?x) = (?x < e_length (f \<triangleright> ?n) \<and> \<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)
[PROOF STEP]
have
    1: "\<exists>x<Suc n. \<phi> i x \<noteq> f x" and
    2: "inconsist i (f \<triangleright> n) \<down>= (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x)"
[PROOF STATE]
proof (prove)
using this:
(?x < Suc ?n \<and> \<phi> i ?x \<noteq> f ?x) = (?x < e_length (f \<triangleright> ?n) \<and> \<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)

goal (1 subgoal):
 1. \<exists>x<Suc n. \<phi> i x \<noteq> f x &&& inconsist i (f \<triangleright> n) \<down>= (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
using assms(3,4) inconsist_converg_less[of i "f \<triangleright> n"]
[PROOF STATE]
proof (prove)
using this:
(?x < Suc ?n \<and> \<phi> i ?x \<noteq> f ?x) = (?x < e_length (f \<triangleright> ?n) \<and> \<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)
inconsist i (f \<triangleright> n) \<down>
the (inconsist i (f \<triangleright> n)) < Suc n
\<lbrakk>inconsist i (f \<triangleright> n) \<down>; the (inconsist i (f \<triangleright> n)) < e_length (f \<triangleright> n)\<rbrakk> \<Longrightarrow> \<exists>x<e_length (f \<triangleright> n). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x
\<lbrakk>inconsist i (f \<triangleright> n) \<down>; the (inconsist i (f \<triangleright> n)) < e_length (f \<triangleright> n)\<rbrakk> \<Longrightarrow> inconsist i (f \<triangleright> n) \<down>= (LEAST x. x < e_length (f \<triangleright> n) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> n) x)

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

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<Suc n. \<phi> i x \<noteq> f x
inconsist i (f \<triangleright> n) \<down>= (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
have 3: "\<exists>x<Suc (n + m). \<phi> i x \<noteq> f x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<Suc n. \<phi> i x \<noteq> f x
inconsist i (f \<triangleright> n) \<down>= (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x)

goal (1 subgoal):
 1. \<exists>x<Suc (n + m). \<phi> i x \<noteq> f x
[PROOF STEP]
using not_add_less1
[PROOF STATE]
proof (prove)
using this:
\<exists>x<Suc n. \<phi> i x \<noteq> f x
inconsist i (f \<triangleright> n) \<down>= (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x)
\<not> ?i + ?j < ?i

goal (1 subgoal):
 1. \<exists>x<Suc (n + m). \<phi> i x \<noteq> f x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>x<Suc (n + m). \<phi> i x \<noteq> f x

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<Suc (n + m). \<phi> i x \<noteq> f x
[PROOF STEP]
have "\<exists>x<Suc (n + m). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<Suc (n + m). \<phi> i x \<noteq> f x

goal (1 subgoal):
 1. \<exists>x<Suc (n + m). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x
[PROOF STEP]
using cond
[PROOF STATE]
proof (prove)
using this:
\<exists>x<Suc (n + m). \<phi> i x \<noteq> f x
(?x < Suc ?n \<and> \<phi> i ?x \<noteq> f ?x) = (?x < e_length (f \<triangleright> ?n) \<and> \<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> ?n) ?x)

goal (1 subgoal):
 1. \<exists>x<Suc (n + m). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x<Suc (n + m). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<Suc (n + m). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x
[PROOF STEP]
have "\<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<Suc (n + m). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x

goal (1 subgoal):
 1. \<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
have 4: "inconsist i (f \<triangleright> (n + m)) \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) \<down>
[PROOF STEP]
using assms(2) R1_imp_total1 inconsist_def
[PROOF STATE]
proof (prove)
using this:
\<phi> i \<in> \<R>
?f \<in> \<R> \<Longrightarrow> total1 ?f
inconsist ?i ?e \<equiv> if \<exists>x<e_length ?e. \<phi> ?i x \<up> then None else if \<exists>x<e_length ?e. \<phi> ?i x \<down>\<noteq> e_nth ?e x then Some (LEAST x. x < e_length ?e \<and> \<phi> ?i x \<down>\<noteq> e_nth ?e x) else Some (e_length ?e)

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

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x
inconsist i (f \<triangleright> (n + m)) \<down>
[PROOF STEP]
have "inconsist i (f \<triangleright> (n + m)) \<down>=
      (LEAST x. x < e_length (f \<triangleright> (n + m)) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x
inconsist i (f \<triangleright> (n + m)) \<down>

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < e_length (f \<triangleright> (n + m)) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x)
[PROOF STEP]
using inconsist_converg[OF 4]
[PROOF STATE]
proof (prove)
using this:
\<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x
inconsist i (f \<triangleright> (n + m)) \<down>
inconsist i (f \<triangleright> (n + m)) = (if \<exists>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x then Some (LEAST x. x < e_length (f \<triangleright> (n + m)) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x) else Some (e_length (f \<triangleright> (n + m))))
\<forall>x<e_length (f \<triangleright> (n + m)). \<phi> i x \<down>

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

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < e_length (f \<triangleright> (n + m)) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x)
[PROOF STEP]
have 5: "inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)"
[PROOF STATE]
proof (prove)
using this:
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < e_length (f \<triangleright> (n + m)) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x)

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
using cond[of _ "n + m"]
[PROOF STATE]
proof (prove)
using this:
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < e_length (f \<triangleright> (n + m)) \<and> \<phi> i x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) x)
(?x < Suc (n + m) \<and> \<phi> i ?x \<noteq> f ?x) = (?x < e_length (f \<triangleright> (n + m)) \<and> \<phi> i ?x \<down>\<noteq> e_nth (f \<triangleright> (n + m)) ?x)

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
have "(LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x) =
      (LEAST x. x < Suc n + m \<and> \<phi> i x \<noteq> f x)"
[PROOF STATE]
proof (prove)
using this:
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)

goal (1 subgoal):
 1. (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x) = (LEAST x. x < Suc n + m \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
using least_bounded_gr[where ?upper="Suc n"] 1 3
[PROOF STATE]
proof (prove)
using this:
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)
\<exists>x<Suc n. ?P x \<Longrightarrow> (LEAST x. x < Suc n \<and> ?P x) = (LEAST x. x < Suc n + ?m \<and> ?P x)
\<exists>x<Suc n. \<phi> i x \<noteq> f x
\<exists>x<Suc (n + m). \<phi> i x \<noteq> f x

goal (1 subgoal):
 1. (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x) = (LEAST x. x < Suc n + m \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x) = (LEAST x. x < Suc n + m \<and> \<phi> i x \<noteq> f x)

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x) = (LEAST x. x < Suc n + m \<and> \<phi> i x \<noteq> f x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x) = (LEAST x. x < Suc n + m \<and> \<phi> i x \<noteq> f x)

goal (1 subgoal):
 1. inconsist i (f \<triangleright> (n + m)) = inconsist i (f \<triangleright> n)
[PROOF STEP]
using 2 5
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x) = (LEAST x. x < Suc n + m \<and> \<phi> i x \<noteq> f x)
inconsist i (f \<triangleright> n) \<down>= (LEAST x. x < Suc n \<and> \<phi> i x \<noteq> f x)
inconsist i (f \<triangleright> (n + m)) \<down>= (LEAST x. x < Suc (n + m) \<and> \<phi> i x \<noteq> f x)

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

goal:
No subgoals!
[PROOF STEP]
qed