[STATEMENT]
lemma delay_gr0_converg:
  assumes "the (delay i x) > 0"
  shows "\<phi> i (e_take (the (delay i x)) x) \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
let ?P = "\<lambda>j. j < e_length x \<and> the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
have "\<exists>j. ?P j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<exists>j. ?P j)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
[PROOF STEP]
have "delay i x \<down>= 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. delay i x \<down>= 0
[PROOF STEP]
using delay_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)

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

goal (1 subgoal):
 1. \<not> (\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < the (delay i x)
delay i x \<down>= 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
0 < the (delay i x)
delay i x \<down>= 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
[PROOF STEP]
have d: "the (delay i x) = Suc (Greatest ?P)"
[PROOF STATE]
proof (prove)
using this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])

goal (1 subgoal):
 1. the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
[PROOF STEP]
using delay_def
[PROOF STATE]
proof (prove)
using this:
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)

goal (1 subgoal):
 1. the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
have "\<And>y. ?P y \<Longrightarrow> y \<le> e_length x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc y) x]) \<Longrightarrow> y \<le> e_length x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x
[PROOF STEP]
have "?P (Greatest ?P)"
[PROOF STATE]
proof (prove)
using this:
the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x

goal (1 subgoal):
 1. (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
using \<open>\<exists>j. ?P j\<close> GreatestI_ex_nat[where ?P="?P"]
[PROOF STATE]
proof (prove)
using this:
the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))
?y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc ?y) x]) \<Longrightarrow> ?y \<le> e_length x
\<exists>j<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])
\<lbrakk>\<exists>k<e_length x. 0 < the (eval r_result1 [e_length x, i, e_take (Suc k) x]); \<And>y. y < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc y) x]) \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (1 subgoal):
 1. (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
have "the (eval r_result1 [e_length x, i, e_take (Suc (Greatest ?P)) x]) > 0"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x])) < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (1 subgoal):
 1. 0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
[PROOF STEP]
have "the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x]) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])

goal (1 subgoal):
 1. 0 < the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x])
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [e_length x, i, e_take (Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))) x])
the (delay i x) = Suc (GREATEST j. j < e_length x \<and> 0 < the (eval r_result1 [e_length x, i, e_take (Suc j) x]))

goal (1 subgoal):
 1. 0 < the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x])

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x])

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
using r_result1_diverg_phi
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x])
\<phi> ?i ?x \<up> \<Longrightarrow> eval r_result1 [?t, ?i, ?x] \<down>= 0

goal (1 subgoal):
 1. \<phi> i (e_take (the (delay i x)) x) \<down>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<phi> i (e_take (the (delay i x)) x) \<down>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delay_unbounded:
  fixes n :: nat
  assumes "f \<in> \<R>" and "\<forall>n. \<phi> i (f \<triangleright> n) \<down>"
  shows "\<exists>m. the (delay i (f \<triangleright> m)) > n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
f \<in> \<R>
\<forall>n. \<phi> i (f \<triangleright> n) \<down>
[PROOF STEP]
have "\<exists>t. the (eval r_result1 [t, i, f \<triangleright> n]) > 0"
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
\<forall>n. \<phi> i (f \<triangleright> n) \<down>

goal (1 subgoal):
 1. \<exists>t. 0 < the (eval r_result1 [t, i, f \<triangleright> n])
[PROOF STEP]
using r_result1_converg_phi
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
\<forall>n. \<phi> i (f \<triangleright> n) \<down>
\<phi> ?i ?x \<down>= ?v \<Longrightarrow> \<exists>t. (\<forall>t'\<ge>t. eval r_result1 [t', ?i, ?x] \<down>= Suc ?v) \<and> (\<forall>t'<t. eval r_result1 [t', ?i, ?x] \<down>= 0)

goal (1 subgoal):
 1. \<exists>t. 0 < the (eval r_result1 [t, i, f \<triangleright> n])
[PROOF STEP]
by (metis le_refl option.exhaust_sel option.sel zero_less_Suc)
[PROOF STATE]
proof (state)
this:
\<exists>t. 0 < the (eval r_result1 [t, i, f \<triangleright> n])

goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. 0 < the (eval r_result1 [t, i, f \<triangleright> n])
[PROOF STEP]
obtain t where t: "the (eval r_result1 [t, i, f \<triangleright> n]) > 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. 0 < the (eval r_result1 [t, i, f \<triangleright> n])

goal (1 subgoal):
 1. (\<And>t. 0 < the (eval r_result1 [t, i, f \<triangleright> n]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [t, i, f \<triangleright> n])

goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
let ?m = "max n t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
have "Suc ?m \<ge> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<le> Suc (max n t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<le> Suc (max n t)

goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
have m: "the (eval r_result1 [Suc ?m, i, f \<triangleright> n]) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])
[PROOF STEP]
let ?w = "eval r_result1 [t, i, f \<triangleright> n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])
[PROOF STEP]
obtain v where v: "?w \<down>= Suc v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. eval r_result1 [t, i, f \<triangleright> n] \<down>= Suc v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using t assms(2) r_result1_bivalent_phi
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [t, i, f \<triangleright> n])
\<forall>n. \<phi> i (f \<triangleright> n) \<down>
\<phi> ?i ?x \<down>= ?v \<Longrightarrow> eval r_result1 [?t, ?i, ?x] \<down>= Suc ?v \<or> eval r_result1 [?t, ?i, ?x] \<down>= 0

goal (1 subgoal):
 1. (\<And>v. eval r_result1 [t, i, f \<triangleright> n] \<down>= Suc v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eval r_result1 [t, i, f \<triangleright> n] \<down>= Suc v

goal (1 subgoal):
 1. 0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])
[PROOF STEP]
have "eval r_result1 [Suc ?m, i, f \<triangleright> n] = ?w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_result1 [Suc (max n t), i, f \<triangleright> n] = eval r_result1 [t, i, f \<triangleright> n]
[PROOF STEP]
using v t r_result1_saturating' \<open>Suc ?m \<ge> t\<close> le_Suc_ex
[PROOF STATE]
proof (prove)
using this:
eval r_result1 [t, i, f \<triangleright> n] \<down>= Suc v
0 < the (eval r_result1 [t, i, f \<triangleright> n])
eval r_result1 [?t, ?i, ?x] \<down>= Suc ?v \<Longrightarrow> eval r_result1 [?t + ?d, ?i, ?x] \<down>= Suc ?v
t \<le> Suc (max n t)
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

goal (1 subgoal):
 1. eval r_result1 [Suc (max n t), i, f \<triangleright> n] = eval r_result1 [t, i, f \<triangleright> n]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eval r_result1 [Suc (max n t), i, f \<triangleright> n] = eval r_result1 [t, i, f \<triangleright> n]

goal (1 subgoal):
 1. 0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_result1 [Suc (max n t), i, f \<triangleright> n] = eval r_result1 [t, i, f \<triangleright> n]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval r_result1 [Suc (max n t), i, f \<triangleright> n] = eval r_result1 [t, i, f \<triangleright> n]

goal (1 subgoal):
 1. 0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
eval r_result1 [Suc (max n t), i, f \<triangleright> n] = eval r_result1 [t, i, f \<triangleright> n]
0 < the (eval r_result1 [t, i, f \<triangleright> n])

goal (1 subgoal):
 1. 0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])

goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
let ?x = "f \<triangleright> ?m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
have "the (delay i ?x) > n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
let ?P = "\<lambda>j. j < e_length ?x \<and> the (eval r_result1 [e_length ?x, i, e_take (Suc j) ?x]) > 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
have "e_length ?x = Suc ?m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_length (f \<triangleright> max n t) = Suc (max n t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e_length (f \<triangleright> max n t) = Suc (max n t)

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e_length (f \<triangleright> max n t) = Suc (max n t)

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
have "e_take (Suc n) ?x = f \<triangleright> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_take (Suc n) (f \<triangleright> max n t) = f \<triangleright> n
[PROOF STEP]
using assms(1) e_take_init
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
\<lbrakk>?f \<in> \<R>; ?k < Suc ?n\<rbrakk> \<Longrightarrow> e_take (Suc ?k) (?f \<triangleright> ?n) = ?f \<triangleright> ?k

goal (1 subgoal):
 1. e_take (Suc n) (f \<triangleright> max n t) = f \<triangleright> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e_take (Suc n) (f \<triangleright> max n t) = f \<triangleright> n

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e_length (f \<triangleright> max n t) = Suc (max n t)
e_take (Suc n) (f \<triangleright> max n t) = f \<triangleright> n
[PROOF STEP]
have "?P n"
[PROOF STATE]
proof (prove)
using this:
e_length (f \<triangleright> max n t) = Suc (max n t)
e_take (Suc n) (f \<triangleright> max n t) = f \<triangleright> n

goal (1 subgoal):
 1. n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)])
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
e_length (f \<triangleright> max n t) = Suc (max n t)
e_take (Suc n) (f \<triangleright> max n t) = f \<triangleright> n
0 < the (eval r_result1 [Suc (max n t), i, f \<triangleright> n])

goal (1 subgoal):
 1. n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)])

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
have "\<And>y. ?P y \<Longrightarrow> y \<le> e_length ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc y) (f \<triangleright> max n t)]) \<Longrightarrow> y \<le> e_length (f \<triangleright> max n t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?y < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc ?y) (f \<triangleright> max n t)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> max n t)

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
with \<open>?P n\<close>
[PROOF STATE]
proof (chain)
picking this:
n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)])
?y < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc ?y) (f \<triangleright> max n t)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> max n t)
[PROOF STEP]
have "n \<le> (Greatest ?P)"
[PROOF STATE]
proof (prove)
using this:
n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)])
?y < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc ?y) (f \<triangleright> max n t)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> max n t)

goal (1 subgoal):
 1. n \<le> (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))
[PROOF STEP]
using Greatest_le_nat[of ?P n "e_length ?x"]
[PROOF STATE]
proof (prove)
using this:
n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)])
?y < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc ?y) (f \<triangleright> max n t)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> max n t)
\<lbrakk>n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)]); \<And>y. y < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc y) (f \<triangleright> max n t)]) \<Longrightarrow> y \<le> e_length (f \<triangleright> max n t)\<rbrakk> \<Longrightarrow> n \<le> (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))

goal (1 subgoal):
 1. n \<le> (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<le> (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
have "the (delay i ?x) = Suc (Greatest ?P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> max n t)) = Suc (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))
[PROOF STEP]
using delay_def \<open>?P n\<close>
[PROOF STATE]
proof (prove)
using this:
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
n < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc n) (f \<triangleright> max n t)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> max n t)) = Suc (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> max n t)) = Suc (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<le> (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))
the (delay i (f \<triangleright> max n t)) = Suc (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))
the (delay i (f \<triangleright> max n t)) = Suc (GREATEST j. j < e_length (f \<triangleright> max n t) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> max n t), i, e_take (Suc j) (f \<triangleright> max n t)]))

goal (1 subgoal):
 1. n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < the (delay i (f \<triangleright> max n t))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n < the (delay i (f \<triangleright> max n t))

goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < the (delay i (f \<triangleright> max n t))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < the (delay i (f \<triangleright> max n t))

goal (1 subgoal):
 1. \<exists>m. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m. n < the (delay i (f \<triangleright> m))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delay_monotone:
  assumes "f \<in> \<R>" and "n\<^sub>1 \<le> n\<^sub>2"
  shows "the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))"
    (is "the (delay i ?x1) \<le> the (delay i ?x2)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
proof (cases "the (delay i (f \<triangleright> n\<^sub>1)) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. the (delay i (f \<triangleright> n\<^sub>1)) = 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
 2. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n\<^sub>1)) = 0

goal (2 subgoals):
 1. the (delay i (f \<triangleright> n\<^sub>1)) = 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
 2. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (delay i (f \<triangleright> n\<^sub>1)) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n\<^sub>1)) = 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
let ?P1 = "\<lambda>j. j < e_length ?x1 \<and> the (eval r_result1 [e_length ?x1, i, e_take (Suc j) ?x1]) > 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
let ?P2 = "\<lambda>j. j < e_length ?x2 \<and> the (eval r_result1 [e_length ?x2, i, e_take (Suc j) ?x2]) > 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0
[PROOF STEP]
have d1: "the (delay i ?x1) = Suc (Greatest ?P1)" "\<exists>j. ?P1 j"
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) &&& \<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])
[PROOF STEP]
using delay_def option.collapse
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
?option \<noteq> None \<Longrightarrow> Some (the ?option) = ?option

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) &&& \<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))
\<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))
\<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
have "\<And>y. ?P1 y \<Longrightarrow> y \<le> e_length ?x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc y) (f \<triangleright> n\<^sub>1)]) \<Longrightarrow> y \<le> e_length (f \<triangleright> n\<^sub>1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?y < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>1)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>1)

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))
\<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])
?y < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>1)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>1)
[PROOF STEP]
have *: "?P1 (Greatest ?P1)"
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))
\<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])
?y < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>1)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>1)

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])
[PROOF STEP]
using GreatestI_ex_nat[of ?P1]
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))
\<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])
?y < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>1)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>1)
\<lbrakk>\<exists>k<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc k) (f \<triangleright> n\<^sub>1)]); \<And>y. y < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc y) (f \<triangleright> n\<^sub>1)]) \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
let ?j = "Greatest ?P1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])
[PROOF STEP]
have "?j < e_length ?x1"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1)

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1)
[PROOF STEP]
have 1: "e_take (Suc ?j) ?x1 = e_take (Suc ?j) ?x2"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1)

goal (1 subgoal):
 1. e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1) = e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)
[PROOF STEP]
using assms e_take_init
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1)
f \<in> \<R>
n\<^sub>1 \<le> n\<^sub>2
\<lbrakk>?f \<in> \<R>; ?k < Suc ?n\<rbrakk> \<Longrightarrow> e_take (Suc ?k) (?f \<triangleright> ?n) = ?f \<triangleright> ?k

goal (1 subgoal):
 1. e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1) = e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1) = e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])
[PROOF STEP]
have 2: "?j < e_length ?x2"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])
n\<^sub>1 \<le> n\<^sub>2

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2)

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
with 1 *
[PROOF STATE]
proof (chain)
picking this:
e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1) = e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
have "the (eval r_result1 [e_length ?x1, i, e_take (Suc ?j) ?x2]) > 0"
[PROOF STATE]
proof (prove)
using this:
e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1) = e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>1)])
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2)

goal (1 subgoal):
 1. 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
have "e_length ?x1 \<le> e_length ?x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_length (f \<triangleright> n\<^sub>1) \<le> e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 \<le> n\<^sub>2

goal (1 subgoal):
 1. e_length (f \<triangleright> n\<^sub>1) \<le> e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e_length (f \<triangleright> n\<^sub>1) \<le> e_length (f \<triangleright> n\<^sub>2)

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
e_length (f \<triangleright> n\<^sub>1) \<le> e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
have "the (eval r_result1 [e_length ?x2, i, e_take (Suc ?j) ?x2]) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
e_length (f \<triangleright> n\<^sub>1) \<le> e_length (f \<triangleright> n\<^sub>2)

goal (1 subgoal):
 1. 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
[PROOF STEP]
using r_result1_saturating_the
[PROOF STATE]
proof (prove)
using this:
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
e_length (f \<triangleright> n\<^sub>1) \<le> e_length (f \<triangleright> n\<^sub>2)
\<lbrakk>0 < the (eval r_result1 [?t, ?i, ?x]); ?t \<le> ?t'\<rbrakk> \<Longrightarrow> 0 < the (eval r_result1 [?t', ?i, ?x])

goal (1 subgoal):
 1. 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2)
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
[PROOF STEP]
have "?P2 ?j"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2)
0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
[PROOF STEP]
have d2: "the (delay i ?x2) = Suc (Greatest ?P2)"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>2)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))
[PROOF STEP]
using delay_def
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>2)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n\<^sub>2)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
have "\<And>y. ?P2 y \<Longrightarrow> y \<le> e_length ?x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc y) (f \<triangleright> n\<^sub>2)]) \<Longrightarrow> y \<le> e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?y < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>2)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>2)

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
with \<open>?P2 ?j\<close>
[PROOF STATE]
proof (chain)
picking this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
?y < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>2)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>2)
[PROOF STEP]
have "?j \<le> (Greatest ?P2)"
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
?y < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>2)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>2)

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) \<le> (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))
[PROOF STEP]
using Greatest_le_nat[of ?P2]
[PROOF STATE]
proof (prove)
using this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))) (f \<triangleright> n\<^sub>2)])
?y < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc ?y) (f \<triangleright> n\<^sub>2)]) \<Longrightarrow> ?y \<le> e_length (f \<triangleright> n\<^sub>2)
\<lbrakk>?k < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc ?k) (f \<triangleright> n\<^sub>2)]); \<And>y. y < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc y) (f \<triangleright> n\<^sub>2)]) \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> ?k \<le> (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))

goal (1 subgoal):
 1. (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) \<le> (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) \<le> (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<noteq> 0 \<Longrightarrow> the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
with d1 d2
[PROOF STATE]
proof (chain)
picking this:
the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))
\<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])
the (delay i (f \<triangleright> n\<^sub>2)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) \<le> (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n\<^sub>1)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)]))
\<exists>j<e_length (f \<triangleright> n\<^sub>1). 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])
the (delay i (f \<triangleright> n\<^sub>2)) = Suc (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))
(GREATEST j. j < e_length (f \<triangleright> n\<^sub>1) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>1), i, e_take (Suc j) (f \<triangleright> n\<^sub>1)])) \<le> (GREATEST j. j < e_length (f \<triangleright> n\<^sub>2) \<and> 0 < the (eval r_result1 [e_length (f \<triangleright> n\<^sub>2), i, e_take (Suc j) (f \<triangleright> n\<^sub>2)]))

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n\<^sub>1)) \<le> the (delay i (f \<triangleright> n\<^sub>2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delay_unbounded_monotone:
  fixes n :: nat
  assumes "f \<in> \<R>" and "\<forall>n. \<phi> i (f \<triangleright> n) \<down>"
  shows "\<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. the (delay i (f \<triangleright> m)) > n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
from assms delay_unbounded
[PROOF STATE]
proof (chain)
picking this:
f \<in> \<R>
\<forall>n. \<phi> i (f \<triangleright> n) \<down>
\<lbrakk>?f \<in> \<R>; \<forall>n. \<phi> ?i (?f \<triangleright> n) \<down>\<rbrakk> \<Longrightarrow> \<exists>m. ?n < the (delay ?i (?f \<triangleright> m))
[PROOF STEP]
obtain m\<^sub>0 where "the (delay i (f \<triangleright> m\<^sub>0)) > n"
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
\<forall>n. \<phi> i (f \<triangleright> n) \<down>
\<lbrakk>?f \<in> \<R>; \<forall>n. \<phi> ?i (?f \<triangleright> n) \<down>\<rbrakk> \<Longrightarrow> \<exists>m. ?n < the (delay ?i (?f \<triangleright> m))

goal (1 subgoal):
 1. (\<And>m\<^sub>0. n < the (delay i (f \<triangleright> m\<^sub>0)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n < the (delay i (f \<triangleright> m\<^sub>0))

goal (1 subgoal):
 1. \<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < the (delay i (f \<triangleright> m\<^sub>0))
[PROOF STEP]
have "\<forall>m\<ge>m\<^sub>0. the (delay i (f \<triangleright> m)) > n"
[PROOF STATE]
proof (prove)
using this:
n < the (delay i (f \<triangleright> m\<^sub>0))

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
using assms(1) delay_monotone order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
n < the (delay i (f \<triangleright> m\<^sub>0))
f \<in> \<R>
\<lbrakk>?f \<in> \<R>; ?n\<^sub>1 \<le> ?n\<^sub>2\<rbrakk> \<Longrightarrow> the (delay ?i (?f \<triangleright> ?n\<^sub>1)) \<le> the (delay ?i (?f \<triangleright> ?n\<^sub>2))
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))

goal (1 subgoal):
 1. \<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))

goal (1 subgoal):
 1. \<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n < the (delay i (f \<triangleright> m))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_totalizer_recfn: "recfn 2 (r_totalizer d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (r_totalizer d)
[PROOF STEP]
unfolding r_totalizer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (Cn 2 (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 0, recf.Id 2 1])
[PROOF STEP]
by simp


[STATEMENT]
lemma r_totalizer:
  "eval (r_totalizer d) [i, x] =
    (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
let ?i = "Cn 2 r_delay [Id 2 0, Id 2 1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
have "eval ?i [i, x] = eval r_delay [i, x]" for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [i, x] = eval r_delay [i, x]
[PROOF STEP]
using r_delay_recfn
[PROOF STATE]
proof (prove)
using this:
recfn 2 r_delay

goal (1 subgoal):
 1. eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [i, x] = eval r_delay [i, x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [?i, ?x] = eval r_delay [?i, ?x]

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [?i, ?x] = eval r_delay [?i, ?x]
[PROOF STEP]
have i: "eval ?i [i, x] = delay i x" for i x
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [?i, ?x] = eval r_delay [?i, ?x]

goal (1 subgoal):
 1. eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [i, x] = delay i x
[PROOF STEP]
using r_delay
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [?i, ?x] = eval r_delay [?i, ?x]
eval r_delay [?i, ?x] \<down>= (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)

goal (1 subgoal):
 1. eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [i, x] = delay i x
[PROOF STEP]
by (simp add: delay_def)
[PROOF STATE]
proof (state)
this:
eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [?i, ?x] = delay ?i ?x

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
let ?t = "r_constn 1 d"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
have t: "eval ?t [i, x] \<down>= d" for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (r_constn 1 d) [i, x] \<down>= d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_constn 1 d) [?i, ?x] \<down>= d

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
let ?e1 = "Cn 2 r_take [?i, Id 2 1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
let ?e = "Cn 2 r_phi [Id 2 0, ?e1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
have "eval ?e1 [i, x] = eval r_take [the (delay i x), x]" for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [i, x] = eval r_take [the (delay i x), x]
[PROOF STEP]
using r_delay i delay_def
[PROOF STATE]
proof (prove)
using this:
eval r_delay [?i, ?x] \<down>= (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)
eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [?i, ?x] = delay ?i ?x
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)

goal (1 subgoal):
 1. eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [i, x] = eval r_take [the (delay i x), x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] = eval r_take [the (delay ?i ?x), ?x]

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] = eval r_take [the (delay ?i ?x), ?x]
[PROOF STEP]
have "eval ?e1 [i, x] \<down>= e_take (the (delay i x)) x" for i x
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] = eval r_take [the (delay ?i ?x), ?x]

goal (1 subgoal):
 1. eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [i, x] \<down>= e_take (the (delay i x)) x
[PROOF STEP]
using delay_le_length
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] = eval r_take [the (delay ?i ?x), ?x]
the (delay ?i ?x) \<le> e_length ?x

goal (1 subgoal):
 1. eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [i, x] \<down>= e_take (the (delay i x)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] \<down>= e_take (the (delay ?i ?x)) ?x

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] \<down>= e_take (the (delay ?i ?x)) ?x
[PROOF STEP]
have e: "eval ?e [i, x] = \<phi> i (e_take (the (delay i x)) x)"
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] \<down>= e_take (the (delay ?i ?x)) ?x

goal (1 subgoal):
 1. eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [i, x] = \<phi> i (e_take (the (delay i x)) x)
[PROOF STEP]
using phi_def
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]) [?i, ?x] \<down>= e_take (the (delay ?i ?x)) ?x
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]

goal (1 subgoal):
 1. eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [i, x] = \<phi> i (e_take (the (delay i x)) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [i, x] = \<phi> i (e_take (the (delay i x)) x)

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
let ?z = "r_lifz ?t ?e"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
have recfn_te: "recfn 2 ?t" "recfn 2 ?e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (r_constn 1 d) &&& recfn 2 (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
recfn 2 (r_constn 1 d)
recfn 2 (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
recfn 2 (r_constn 1 d)
recfn 2 (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])
[PROOF STEP]
have "eval (r_totalizer d) [i, x] = eval (r_lifz ?t ?e) [the (delay i x), i, x]"
      for i x
[PROOF STATE]
proof (prove)
using this:
recfn 2 (r_constn 1 d)
recfn 2 (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = eval (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [the (delay i x), i, x]
[PROOF STEP]
unfolding r_totalizer_def
[PROOF STATE]
proof (prove)
using this:
recfn 2 (r_constn 1 d)
recfn 2 (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])

goal (1 subgoal):
 1. eval (Cn 2 (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, x] = eval (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [the (delay i x), i, x]
[PROOF STEP]
using i r_totalizer_recfn delay_def
[PROOF STATE]
proof (prove)
using this:
recfn 2 (r_constn 1 d)
recfn 2 (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])
eval (Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1]) [?i, ?x] = delay ?i ?x
recfn 2 (r_totalizer ?d)
delay ?i ?x \<equiv> Some (if \<exists>j<e_length ?x. 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x]) then Suc (GREATEST j. j < e_length ?x \<and> 0 < the (eval r_result1 [e_length ?x, ?i, e_take (Suc j) ?x])) else 0)

goal (1 subgoal):
 1. eval (Cn 2 (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, x] = eval (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [the (delay i x), i, x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_totalizer d) [?i, ?x] = eval (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [the (delay ?i ?x), ?i, ?x]

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (r_totalizer d) [?i, ?x] = eval (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [the (delay ?i ?x), ?i, ?x]
[PROOF STEP]
have "eval (r_totalizer d) [i, x] =
      (if the (delay i x) = 0 then eval ?t [i, x] else eval ?e [i, x])"
      for i x
[PROOF STATE]
proof (prove)
using this:
eval (r_totalizer d) [?i, ?x] = eval (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [the (delay ?i ?x), ?i, ?x]

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then eval (r_constn 1 d) [i, x] else eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [i, x])
[PROOF STEP]
using recfn_te
[PROOF STATE]
proof (prove)
using this:
eval (r_totalizer d) [?i, ?x] = eval (r_lifz (r_constn 1 d) (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])) [the (delay ?i ?x), ?i, ?x]
recfn 2 (r_constn 1 d)
recfn 2 (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]])

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then eval (r_constn 1 d) [i, x] else eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [i, x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_totalizer d) [?i, ?x] = (if the (delay ?i ?x) = 0 then eval (r_constn 1 d) [?i, ?x] else eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [?i, ?x])

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (r_totalizer d) [?i, ?x] = (if the (delay ?i ?x) = 0 then eval (r_constn 1 d) [?i, ?x] else eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [?i, ?x])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval (r_totalizer d) [?i, ?x] = (if the (delay ?i ?x) = 0 then eval (r_constn 1 d) [?i, ?x] else eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [?i, ?x])

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
using t e
[PROOF STATE]
proof (prove)
using this:
eval (r_totalizer d) [?i, ?x] = (if the (delay ?i ?x) = 0 then eval (r_constn 1 d) [?i, ?x] else eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [?i, ?x])
eval (r_constn 1 d) [?i, ?x] \<down>= d
eval (Cn 2 r_phi [recf.Id 2 0, Cn 2 r_take [Cn 2 r_delay [recf.Id 2 0, recf.Id 2 1], recf.Id 2 1]]) [i, x] = \<phi> i (e_take (the (delay i x)) x)

goal (1 subgoal):
 1. eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \<phi> i (e_take (the (delay i x)) x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_totalizer_total: "total (r_totalizer d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Recursive.total (r_totalizer d)
[PROOF STEP]
proof (rule totalI2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. recfn 2 (r_totalizer d)
 2. \<And>x y. eval (r_totalizer d) [x, y] \<down>
[PROOF STEP]
show "recfn 2 (r_totalizer d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (r_totalizer d)
[PROOF STEP]
using r_totalizer_recfn
[PROOF STATE]
proof (prove)
using this:
recfn 2 (r_totalizer ?d)

goal (1 subgoal):
 1. recfn 2 (r_totalizer d)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 2 (r_totalizer d)

goal (1 subgoal):
 1. \<And>x y. eval (r_totalizer d) [x, y] \<down>
[PROOF STEP]
show "\<And>x y. eval (r_totalizer d) [x, y] \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. eval (r_totalizer d) [x, y] \<down>
[PROOF STEP]
using r_totalizer delay_gr0_converg
[PROOF STATE]
proof (prove)
using this:
eval (r_totalizer ?d) [?i, ?x] = (if the (delay ?i ?x) = 0 then Some ?d else \<phi> ?i (e_take (the (delay ?i ?x)) ?x))
0 < the (delay ?i ?x) \<Longrightarrow> \<phi> ?i (e_take (the (delay ?i ?x)) ?x) \<down>

goal (1 subgoal):
 1. \<And>x y. eval (r_totalizer d) [x, y] \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_totalizer d) [?x, ?y] \<down>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma totalizer_init:
  assumes "f \<in> \<R>"
  shows "totalizer d i (f \<triangleright> n) =
    (if the (delay i (f \<triangleright> n)) = 0 then Some d
     else \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> n)) - 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. totalizer d i (f \<triangleright> n) = (if the (delay i (f \<triangleright> n)) = 0 then Some d else \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> n)) - 1)))
[PROOF STEP]
using assms e_take_delay_init
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
\<lbrakk>?f \<in> \<R>; 0 < the (delay ?i (?f \<triangleright> ?n))\<rbrakk> \<Longrightarrow> e_take (the (delay ?i (?f \<triangleright> ?n))) (?f \<triangleright> ?n) = ?f \<triangleright> (the (delay ?i (?f \<triangleright> ?n)) - 1)

goal (1 subgoal):
 1. totalizer d i (f \<triangleright> n) = (if the (delay i (f \<triangleright> n)) = 0 then Some d else \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> n)) - 1)))
[PROOF STEP]
by (simp add: totalizer_def)


[STATEMENT]
lemma totalizer_in_R2: "totalizer d \<in> \<R>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. totalizer d \<in> \<R>\<^sup>2
[PROOF STEP]
using totalizer_def r_totalizer r_totalizer_total R2I r_totalizer_recfn
[PROOF STATE]
proof (prove)
using this:
totalizer ?d ?i ?x \<equiv> if the (delay ?i ?x) = 0 then Some ?d else \<phi> ?i (e_take (the (delay ?i ?x)) ?x)
eval (r_totalizer ?d) [?i, ?x] = (if the (delay ?i ?x) = 0 then Some ?d else \<phi> ?i (e_take (the (delay ?i ?x)) ?x))
Partial_Recursive.total (r_totalizer ?d)
\<lbrakk>recfn 2 ?r; Partial_Recursive.total ?r; \<And>x y. eval ?r [x, y] = ?f x y\<rbrakk> \<Longrightarrow> ?f \<in> \<R>\<^sup>2
recfn 2 (r_totalizer ?d)

goal (1 subgoal):
 1. totalizer d \<in> \<R>\<^sup>2
[PROOF STEP]
by metis


[STATEMENT]
lemma lemma_R_for_Lim:
  assumes "learn_lim \<psi> U (\<phi> i)"
  shows "learn_lim \<psi> U (totalizer d i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. learn_lim \<psi> U (totalizer d i)
[PROOF STEP]
proof (rule learn_limI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. environment \<psi> U (totalizer d i)
 2. \<And>f. f \<in> U \<Longrightarrow> \<exists>ia. \<psi> ia = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= ia)
[PROOF STEP]
show env: "environment \<psi> U (totalizer d i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. environment \<psi> U (totalizer d i)
[PROOF STEP]
using assms learn_limE(1) totalizer_in_R2
[PROOF STATE]
proof (prove)
using this:
learn_lim \<psi> U (\<phi> i)
learn_lim ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
totalizer ?d \<in> \<R>\<^sup>2

goal (1 subgoal):
 1. environment \<psi> U (totalizer d i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
environment \<psi> U (totalizer d i)

goal (1 subgoal):
 1. \<And>f. f \<in> U \<Longrightarrow> \<exists>ia. \<psi> ia = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= ia)
[PROOF STEP]
show "\<exists>j. \<psi> j = f \<and> (\<forall>\<^sup>\<infinity>n. totalizer d i (f \<triangleright> n) \<down>= j)" if "f \<in> U" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
have "f \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> \<R>
[PROOF STEP]
using assms env that
[PROOF STATE]
proof (prove)
using this:
learn_lim \<psi> U (\<phi> i)
environment \<psi> U (totalizer d i)
f \<in> U

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

goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
from assms learn_limE
[PROOF STATE]
proof (chain)
picking this:
learn_lim \<psi> U (\<phi> i)
learn_lim ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
\<lbrakk>learn_lim ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> \<exists>i. ?\<psi> i = ?f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. ?s (?f \<triangleright> n) \<down>= i)
[PROOF STEP]
obtain j n\<^sub>0 where
      j: "\<psi> j = f" and
      n0: "\<forall>n\<ge>n\<^sub>0. (\<phi> i) (f \<triangleright> n) \<down>= j"
[PROOF STATE]
proof (prove)
using this:
learn_lim \<psi> U (\<phi> i)
learn_lim ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
\<lbrakk>learn_lim ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> \<exists>i. ?\<psi> i = ?f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. ?s (?f \<triangleright> n) \<down>= i)

goal (1 subgoal):
 1. (\<And>j n\<^sub>0. \<lbrakk>\<psi> j = f; \<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>f \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
learn_lim \<psi> U (\<phi> i)
learn_lim ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
\<lbrakk>learn_lim ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> \<exists>i. ?\<psi> i = ?f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. ?s (?f \<triangleright> n) \<down>= i)
f \<in> U

goal (1 subgoal):
 1. (\<And>j n\<^sub>0. \<lbrakk>\<psi> j = f; \<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<psi> j = f
\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= j

goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
obtain m\<^sub>0 where m0: "\<forall>m\<ge>m\<^sub>0. the (delay i (f \<triangleright> m)) > n\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using delay_unbounded_monotone \<open>f \<in> \<R>\<close> \<open>f \<in> U\<close> assms learn_limE(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> \<R>; \<forall>n. \<phi> ?i (?f \<triangleright> n) \<down>\<rbrakk> \<Longrightarrow> \<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. ?n < the (delay ?i (?f \<triangleright> m))
f \<in> \<R>
f \<in> U
learn_lim \<psi> U (\<phi> i)
learn_lim ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s

goal (1 subgoal):
 1. (\<And>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))

goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
[PROOF STEP]
have "\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))
[PROOF STEP]
using totalizer_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
totalizer ?d ?i ?x \<equiv> if the (delay ?i ?x) = 0 then Some ?d else \<phi> ?i (e_take (the (delay ?i ?x)) ?x)

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))

goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))
[PROOF STEP]
have "\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> m)) - 1))"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> m)) - 1))
[PROOF STEP]
using e_take_delay_init m0 \<open>f \<in> \<R>\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))
\<lbrakk>?f \<in> \<R>; 0 < the (delay ?i (?f \<triangleright> ?n))\<rbrakk> \<Longrightarrow> e_take (the (delay ?i (?f \<triangleright> ?n))) (?f \<triangleright> ?n) = ?f \<triangleright> (the (delay ?i (?f \<triangleright> ?n)) - 1)
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
f \<in> \<R>

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> m)) - 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> m)) - 1))

goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
with m0 n0
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= j
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> m)) - 1))
[PROOF STEP]
have "\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) \<down>= j"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= j
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) = \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> m)) - 1))

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) \<down>= j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) \<down>= j

goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
with j
[PROOF STATE]
proof (chain)
picking this:
\<psi> j = f
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) \<down>= j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<psi> j = f
\<forall>m\<ge>m\<^sub>0. totalizer d i (f \<triangleright> m) \<down>= j

goal (1 subgoal):
 1. \<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j. \<psi> j = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (f \<triangleright> n) \<down>= j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f \<in> U \<Longrightarrow> \<exists>j. \<psi> j = ?f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. totalizer d i (?f \<triangleright> n) \<down>= j)

goal:
No subgoals!
[PROOF STEP]
qed