[STATEMENT]
lemma lemma_R_for_Lim_effective:
  "\<exists>g\<in>\<R>. \<forall>i.
     \<phi> (the (g i)) \<in> \<R> \<and>
     (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
have "totalizer 0 \<in> \<P>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. totalizer 0 \<in> \<P>\<^sup>2
[PROOF STEP]
using totalizer_in_R2
[PROOF STATE]
proof (prove)
using this:
totalizer ?d \<in> \<R>\<^sup>2

goal (1 subgoal):
 1. totalizer 0 \<in> \<P>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
totalizer 0 \<in> \<P>\<^sup>2

goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
totalizer 0 \<in> \<P>\<^sup>2
[PROOF STEP]
obtain g where g: "g \<in> \<R>" "\<forall>i. (totalizer 0) i = \<phi> (the (g i))"
[PROOF STATE]
proof (prove)
using this:
totalizer 0 \<in> \<P>\<^sup>2

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> \<R>; \<forall>i. totalizer 0 i = \<phi> (the (g i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using numbering_translation_for_phi
[PROOF STATE]
proof (prove)
using this:
totalizer 0 \<in> \<P>\<^sup>2
?\<psi> \<in> \<P>\<^sup>2 \<Longrightarrow> \<exists>c\<in>\<R>. \<forall>i. ?\<psi> i = \<phi> (the (c i))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> \<R>; \<forall>i. totalizer 0 i = \<phi> (the (g i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g \<in> \<R>
\<forall>i. totalizer 0 i = \<phi> (the (g i))

goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
with totalizer_in_R2
[PROOF STATE]
proof (chain)
picking this:
totalizer ?d \<in> \<R>\<^sup>2
g \<in> \<R>
\<forall>i. totalizer 0 i = \<phi> (the (g i))
[PROOF STEP]
have "\<forall>i. \<phi> (the (g i)) \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
totalizer ?d \<in> \<R>\<^sup>2
g \<in> \<R>
\<forall>i. totalizer 0 i = \<phi> (the (g i))

goal (1 subgoal):
 1. \<forall>i. \<phi> (the (g i)) \<in> \<R>
[PROOF STEP]
by (metis R2_proj_R1)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<phi> (the (g i)) \<in> \<R>

goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i. \<phi> (the (g i)) \<in> \<R>

goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
from g(2) lemma_R_for_Lim[where ?d=0]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. totalizer 0 i = \<phi> (the (g i))
learn_lim ?\<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_lim ?\<psi> ?U (totalizer 0 ?i)
[PROOF STEP]
have
    "\<forall>i U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. totalizer 0 i = \<phi> (the (g i))
learn_lim ?\<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_lim ?\<psi> ?U (totalizer 0 ?i)

goal (1 subgoal):
 1. \<forall>i U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))

goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<phi> (the (g i)) \<in> \<R>
\<forall>i U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<phi> (the (g i)) \<in> \<R>
\<forall>i U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))

goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
using g(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<phi> (the (g i)) \<in> \<R>
\<forall>i U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))
g \<in> \<R>

goal (1 subgoal):
 1. \<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lemma_R_for_BC:
  assumes "learn_bc \<psi> U (\<phi> i)"
  shows "learn_bc \<psi> U (totalizer d i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. learn_bc \<psi> U (totalizer d i)
[PROOF STEP]
proof (rule learn_bcI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. environment \<psi> U (totalizer d i)
 2. \<And>f. f \<in> U \<Longrightarrow> \<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[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_bcE(1) totalizer_in_R2
[PROOF STATE]
proof (prove)
using this:
learn_bc \<psi> U (\<phi> i)
learn_bc ?\<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>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[PROOF STEP]
show "\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f" if "f \<in> U" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[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_bc \<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>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[PROOF STEP]
obtain n\<^sub>0 where n0: "\<forall>n\<ge>n\<^sub>0. \<psi> (the ((\<phi> i) (f \<triangleright> n))) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (\<phi> i (f \<triangleright> n))) = f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms learn_bcE \<open>f \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
learn_bc \<psi> U (\<phi> i)
learn_bc ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
\<lbrakk>learn_bc ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. ?\<psi> (the (?s (?f \<triangleright> n))) = ?f
f \<in> U

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

goal (1 subgoal):
 1. \<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[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_bcE(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_bc \<psi> U (\<phi> i)
learn_bc ?\<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>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[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>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[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>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> n))) = f
[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. \<psi> (the (\<phi> i (f \<triangleright> n))) = f
\<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. \<psi> (the (totalizer d i (f \<triangleright> m))) = f"
[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. \<psi> (the (\<phi> i (f \<triangleright> n))) = f
\<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. \<psi> (the (totalizer d i (f \<triangleright> m))) = f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>m\<^sub>0. \<psi> (the (totalizer d i (f \<triangleright> m))) = f

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. \<And>f. f \<in> U \<Longrightarrow> \<exists>ia n\<^sub>0. \<psi> ia = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc ia)
[PROOF STEP]
show "\<exists>j n\<^sub>0. \<psi> j = f \<and>
           (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and>
           (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)"
      if "f \<in> U" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc 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_fin \<psi> U (\<phi> i)
environment \<psi> U (totalizer 0 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 n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
from assms learn_finE[of \<psi> U "\<phi> i"]
[PROOF STATE]
proof (chain)
picking this:
learn_fin \<psi> U (\<phi> i)
learn_fin \<psi> U (\<phi> i) \<Longrightarrow> environment \<psi> U (\<phi> i)
\<lbrakk>learn_fin \<psi> U (\<phi> i); ?f \<in> U\<rbrakk> \<Longrightarrow> \<exists>ia n\<^sub>0. \<psi> ia = ?f \<and> (\<forall>n<n\<^sub>0. \<phi> i (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (?f \<triangleright> n) \<down>= Suc ia)
[PROOF STEP]
obtain j where
      j: "\<psi> j = f" and
      ex_n0: "\<exists>n\<^sub>0. (\<forall>n<n\<^sub>0. (\<phi> i) (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. (\<phi> i) (f \<triangleright> n) \<down>= Suc j)"
[PROOF STATE]
proof (prove)
using this:
learn_fin \<psi> U (\<phi> i)
learn_fin \<psi> U (\<phi> i) \<Longrightarrow> environment \<psi> U (\<phi> i)
\<lbrakk>learn_fin \<psi> U (\<phi> i); ?f \<in> U\<rbrakk> \<Longrightarrow> \<exists>ia n\<^sub>0. \<psi> ia = ?f \<and> (\<forall>n<n\<^sub>0. \<phi> i (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (?f \<triangleright> n) \<down>= Suc ia)

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

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

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
let ?Q = "\<lambda>n\<^sub>0. (\<forall>n<n\<^sub>0. (\<phi> i) (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. (\<phi> i) (f \<triangleright> n) \<down>= Suc j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
define n\<^sub>0 where "n\<^sub>0 = Least ?Q"
[PROOF STATE]
proof (state)
this:
n\<^sub>0 = (LEAST n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j))

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
with ex_n0
[PROOF STATE]
proof (chain)
picking this:
\<exists>n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j)
n\<^sub>0 = (LEAST n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j))
[PROOF STEP]
have n0: "?Q n\<^sub>0" "\<forall>n<n\<^sub>0. \<not> ?Q n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j)
n\<^sub>0 = (LEAST n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j))

goal (1 subgoal):
 1. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j) &&& \<forall>n<n\<^sub>0. \<not> ((\<forall>na<n. \<phi> i (f \<triangleright> na) \<down>= 0) \<and> (\<forall>na\<ge>n. \<phi> i (f \<triangleright> na) \<down>= Suc j))
[PROOF STEP]
using LeastI_ex[of ?Q] not_less_Least[of _ ?Q]
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j)
n\<^sub>0 = (LEAST n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j))
\<exists>x. (\<forall>n<x. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>x. \<phi> i (f \<triangleright> n) \<down>= Suc j) \<Longrightarrow> (\<forall>n<LEAST n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j). \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>LEAST n\<^sub>0. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j). \<phi> i (f \<triangleright> n) \<down>= Suc j)
?k < (LEAST x. (\<forall>n<x. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>x. \<phi> i (f \<triangleright> n) \<down>= Suc j)) \<Longrightarrow> \<not> ((\<forall>n<?k. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>?k. \<phi> i (f \<triangleright> n) \<down>= Suc j))

goal (1 subgoal):
 1. (\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j) &&& \<forall>n<n\<^sub>0. \<not> ((\<forall>na<n. \<phi> i (f \<triangleright> na) \<down>= 0) \<and> (\<forall>na\<ge>n. \<phi> i (f \<triangleright> na) \<down>= Suc j))
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
(\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j)
\<forall>n<n\<^sub>0. \<not> ((\<forall>na<n. \<phi> i (f \<triangleright> na) \<down>= 0) \<and> (\<forall>na\<ge>n. \<phi> i (f \<triangleright> na) \<down>= Suc j))

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
define m\<^sub>0 where "m\<^sub>0 = (LEAST m\<^sub>0. \<forall>m\<ge>m\<^sub>0. the (delay i (f \<triangleright> m)) > n\<^sub>0)"
      (is "m\<^sub>0 = Least ?P")
[PROOF STATE]
proof (state)
this:
m\<^sub>0 = (LEAST m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)))

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m\<^sub>0 = (LEAST m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)))

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
have "\<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. the (delay i (f \<triangleright> m)) > n\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
[PROOF STEP]
using delay_unbounded_monotone \<open>f\<in>\<R>\<close> \<open>f \<in> U\<close> assms learn_finE(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_fin \<psi> U (\<phi> i)
learn_fin ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s

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

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m\<^sub>0 = (LEAST m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)))
\<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
[PROOF STEP]
have m0: "?P m\<^sub>0" "\<forall>m<m\<^sub>0. \<not> ?P m"
[PROOF STATE]
proof (prove)
using this:
m\<^sub>0 = (LEAST m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)))
\<exists>m\<^sub>0. \<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. n\<^sub>0 < the (delay i (f \<triangleright> m)) &&& \<forall>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))
[PROOF STEP]
using LeastI_ex[of ?P] not_less_Least[of _ ?P]
[PROOF STATE]
proof (prove)
using this:
m\<^sub>0 = (LEAST m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)))
\<exists>m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
\<exists>x. \<forall>m\<ge>x. n\<^sub>0 < the (delay i (f \<triangleright> m)) \<Longrightarrow> \<forall>m\<ge>LEAST m\<^sub>0. \<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m)). n\<^sub>0 < the (delay i (f \<triangleright> m))
?k < (LEAST x. \<forall>m\<ge>x. n\<^sub>0 < the (delay i (f \<triangleright> m))) \<Longrightarrow> \<not> (\<forall>m\<ge>?k. n\<^sub>0 < the (delay i (f \<triangleright> m)))

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

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc 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))
\<forall>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))
[PROOF STEP]
have "\<forall>m\<ge>m\<^sub>0. totalizer 0 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))
\<forall>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. totalizer 0 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))
\<forall>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))
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 0 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 0 i (f \<triangleright> m) = \<phi> i (e_take (the (delay i (f \<triangleright> m))) (f \<triangleright> m))

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>m\<^sub>0. totalizer 0 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 0 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 0 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 0 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 0 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))
\<forall>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))
f \<in> \<R>

goal (1 subgoal):
 1. \<forall>m\<ge>m\<^sub>0. totalizer 0 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 0 i (f \<triangleright> m) = \<phi> i (f \<triangleright> (the (delay i (f \<triangleright> m)) - 1))

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc 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>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))
(\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j)
\<forall>n<n\<^sub>0. \<not> ((\<forall>na<n. \<phi> i (f \<triangleright> na) \<down>= 0) \<and> (\<forall>na\<ge>n. \<phi> i (f \<triangleright> na) \<down>= Suc j))
\<forall>m\<ge>m\<^sub>0. totalizer 0 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 0 i (f \<triangleright> m) \<down>= Suc j"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
\<forall>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))
(\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j)
\<forall>n<n\<^sub>0. \<not> ((\<forall>na<n. \<phi> i (f \<triangleright> na) \<down>= 0) \<and> (\<forall>na\<ge>n. \<phi> i (f \<triangleright> na) \<down>= Suc j))
\<forall>m\<ge>m\<^sub>0. totalizer 0 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 0 i (f \<triangleright> m) \<down>= Suc j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>m\<^sub>0. totalizer 0 i (f \<triangleright> m) \<down>= Suc j

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

goal (1 subgoal):
 1. \<exists>j n\<^sub>0. \<psi> j = f \<and> (\<forall>n<n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. totalizer 0 i (f \<triangleright> n) \<down>= Suc j)
[PROOF STEP]
have "totalizer 0 i (f \<triangleright> m) \<down>= 0" if "m < m\<^sub>0" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
proof (cases "the (delay i (f \<triangleright> m)) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. the (delay i (f \<triangleright> m)) = 0 \<Longrightarrow> totalizer 0 i (f \<triangleright> m) \<down>= 0
 2. the (delay i (f \<triangleright> m)) \<noteq> 0 \<Longrightarrow> totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> m)) = 0

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

goal (1 subgoal):
 1. totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
by (simp add: totalizer_def)
[PROOF STATE]
proof (state)
this:
totalizer 0 i (f \<triangleright> m) \<down>= 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> m)) \<noteq> 0 \<Longrightarrow> totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> m)) \<noteq> 0 \<Longrightarrow> totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> m)) \<noteq> 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> m)) \<noteq> 0 \<Longrightarrow> totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (delay i (f \<triangleright> m)) \<noteq> 0
[PROOF STEP]
have "the (delay i (f \<triangleright> m)) \<le> n\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> m)) \<noteq> 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> m)) \<le> n\<^sub>0
[PROOF STEP]
using m0 that \<open>f \<in> \<R>\<close> delay_monotone
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> m)) \<noteq> 0
\<forall>m\<ge>m\<^sub>0. n\<^sub>0 < the (delay i (f \<triangleright> m))
\<forall>m<m\<^sub>0. \<not> (\<forall>ma\<ge>m. n\<^sub>0 < the (delay i (f \<triangleright> ma)))
m < 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))

goal (1 subgoal):
 1. the (delay i (f \<triangleright> m)) \<le> n\<^sub>0
[PROOF STEP]
by (meson leI order.strict_trans2)
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> m)) \<le> n\<^sub>0

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

goal (1 subgoal):
 1. totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
using \<open>f \<in> \<R>\<close> n0(1) totalizer_init
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> m)) \<le> n\<^sub>0
f \<in> \<R>
(\<forall>n<n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (f \<triangleright> n) \<down>= Suc j)
?f \<in> \<R> \<Longrightarrow> 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)))

goal (1 subgoal):
 1. totalizer 0 i (f \<triangleright> m) \<down>= 0
[PROOF STEP]
by (simp add: Suc_le_lessD)
[PROOF STATE]
proof (state)
this:
totalizer 0 i (f \<triangleright> m) \<down>= 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?m < m\<^sub>0 \<Longrightarrow> totalizer 0 i (f \<triangleright> ?m) \<down>= 0

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lemma_R_for_TOTAL:
  fixes \<psi> :: partial2
  shows "\<exists>d. \<forall>U. \<forall>i. learn_total \<psi> U (\<phi> i) \<longrightarrow>  learn_total \<psi> U (totalizer d i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
proof (cases "\<exists>d. \<psi> d \<in> \<R>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
 2. \<nexists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>d. \<psi> d \<in> \<R>

goal (2 subgoals):
 1. \<exists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
 2. \<nexists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>d. \<psi> d \<in> \<R>
[PROOF STEP]
obtain d where "\<psi> d \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
\<exists>d. \<psi> d \<in> \<R>

goal (1 subgoal):
 1. (\<And>d. \<psi> d \<in> \<R> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<psi> d \<in> \<R>

goal (2 subgoals):
 1. \<exists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
 2. \<nexists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
have "learn_total \<psi> U (totalizer d i)" if "learn_total \<psi> U (\<phi> i)" for U i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. learn_total \<psi> U (totalizer d i)
[PROOF STEP]
proof (rule learn_totalI)
[PROOF STATE]
proof (state)
goal (3 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)
 3. \<And>f n. f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[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 that learn_totalE(1) totalizer_in_R2
[PROOF STATE]
proof (prove)
using this:
learn_total \<psi> U (\<phi> i)
learn_total ?\<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 (2 subgoals):
 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)
 2. \<And>f n. f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
show "\<And>f. f \<in> U \<Longrightarrow> \<exists>j. \<psi> j = f \<and> (\<forall>\<^sup>\<infinity>n. totalizer d i (f \<triangleright> n) \<down>= j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. 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)
[PROOF STEP]
using that learn_total_def lemma_R_for_Lim[where ?d=d] learn_limE(2)
[PROOF STATE]
proof (prove)
using this:
learn_total \<psi> U (\<phi> i)
learn_total ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n. ?\<psi> (the (?s (f \<triangleright> n))) \<in> \<R>)
learn_lim ?\<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_lim ?\<psi> ?U (totalizer d ?i)
\<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>f. 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)
[PROOF STEP]
by metis
[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 (1 subgoal):
 1. \<And>f n. f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
show "\<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>" if "f \<in> U" for f n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
proof (cases "the (delay i (f \<triangleright> n)) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. the (delay i (f \<triangleright> n)) = 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
 2. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n)) = 0

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

goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
using totalizer_def \<open>\<psi> d \<in> \<R>\<close>
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n)) = 0
totalizer ?d ?i ?x \<equiv> if the (delay ?i ?x) = 0 then Some ?d else \<phi> ?i (e_take (the (delay ?i ?x)) ?x)
\<psi> d \<in> \<R>

goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n)) \<noteq> 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
have "f \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> \<R>
[PROOF STEP]
using that env
[PROOF STATE]
proof (prove)
using this:
f \<in> U
environment \<psi> U (totalizer d i)

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

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> \<R>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>

goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
using False that \<open>learn_total \<psi> U (\<phi> i)\<close> totalizer_init learn_totalE(3)
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>
the (delay i (f \<triangleright> n)) \<noteq> 0
f \<in> U
learn_total \<psi> U (\<phi> i)
?f \<in> \<R> \<Longrightarrow> 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)))
\<lbrakk>learn_total ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> ?\<psi> (the (?s (?f \<triangleright> ?n))) \<in> \<R>

goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> (the (totalizer d i (f \<triangleright> n))) \<in> \<R>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (?f \<triangleright> ?n))) \<in> \<R>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
learn_total \<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_total \<psi> ?U (totalizer d ?i)

goal (2 subgoals):
 1. \<exists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
 2. \<nexists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
learn_total \<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_total \<psi> ?U (totalizer d ?i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
learn_total \<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_total \<psi> ?U (totalizer d ?i)

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

goal (1 subgoal):
 1. \<nexists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>d. \<psi> d \<in> \<R>

goal (1 subgoal):
 1. \<nexists>d. \<psi> d \<in> \<R> \<Longrightarrow> \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>d. \<psi> d \<in> \<R>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>d. \<psi> d \<in> \<R>

goal (1 subgoal):
 1. \<exists>d. \<forall>U i. learn_total \<psi> U (\<phi> i) \<longrightarrow> learn_total \<psi> U (totalizer d i)
[PROOF STEP]
using learn_total_def lemma_R_for_Lim
[PROOF STATE]
proof (prove)
using this:
\<nexists>d. \<psi> d \<in> \<R>
learn_total ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n. ?\<psi> (the (?s (f \<triangleright> n))) \<in> \<R>)
learn_lim ?\<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_lim ?\<psi> ?U (totalizer ?d ?i)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lemma_R_for_CP:
  fixes \<psi> :: partial2 and U :: "partial1 set"
  assumes "learn_cp \<psi> U (\<phi> i)"
  shows "\<exists>d. learn_cp \<psi> U (totalizer d i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
proof (cases "U = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. U = {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
 2. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
U = {}

goal (2 subgoals):
 1. U = {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
 2. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
U = {}

goal (1 subgoal):
 1. \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
using assms learn_cp_def lemma_R_for_Lim
[PROOF STATE]
proof (prove)
using this:
U = {}
learn_cp \<psi> U (\<phi> i)
learn_cp ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n. ?\<psi> (the (?s (f \<triangleright> n))) \<in> ?U)
learn_lim ?\<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_lim ?\<psi> ?U (totalizer ?d ?i)

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

goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
U \<noteq> {}

goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U \<noteq> {}
[PROOF STEP]
obtain f where "f \<in> U"
[PROOF STATE]
proof (prove)
using this:
U \<noteq> {}

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

goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
from \<open>f \<in> U\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> U
[PROOF STEP]
obtain d where "\<psi> d = f"
[PROOF STATE]
proof (prove)
using this:
f \<in> U

goal (1 subgoal):
 1. (\<And>d. \<psi> d = f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using learn_cpE(2)[OF assms]
[PROOF STATE]
proof (prove)
using this:
f \<in> U
?f \<in> U \<Longrightarrow> \<exists>ia n\<^sub>0. \<psi> ia = ?f \<and> (\<forall>n\<ge>n\<^sub>0. \<phi> i (?f \<triangleright> n) \<down>= ia)

goal (1 subgoal):
 1. (\<And>d. \<psi> d = f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<psi> d = f

goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
with \<open>f \<in> U\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> U
\<psi> d = f
[PROOF STEP]
have "\<psi> d \<in> U"
[PROOF STATE]
proof (prove)
using this:
f \<in> U
\<psi> d = f

goal (1 subgoal):
 1. \<psi> d \<in> U
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> d \<in> U

goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
have "learn_cp \<psi> U (totalizer d i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
proof (rule learn_cpI)
[PROOF STATE]
proof (state)
goal (3 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)
 3. \<And>f n. f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[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_cpE(1) totalizer_in_R2
[PROOF STATE]
proof (prove)
using this:
learn_cp \<psi> U (\<phi> i)
learn_cp ?\<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 (2 subgoals):
 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)
 2. \<And>f n. f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
show "\<And>f. f \<in> U \<Longrightarrow> \<exists>j. \<psi> j = f \<and> (\<forall>\<^sup>\<infinity>n. totalizer d i (f \<triangleright> n) \<down>= j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. 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)
[PROOF STEP]
using assms learn_cp_def lemma_R_for_Lim[where ?d=d] learn_limE(2)
[PROOF STATE]
proof (prove)
using this:
learn_cp \<psi> U (\<phi> i)
learn_cp ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n. ?\<psi> (the (?s (f \<triangleright> n))) \<in> ?U)
learn_lim ?\<psi> ?U (\<phi> ?i) \<Longrightarrow> learn_lim ?\<psi> ?U (totalizer d ?i)
\<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>f. 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)
[PROOF STEP]
by metis
[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 (1 subgoal):
 1. \<And>f n. f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
show "\<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U" if "f \<in> U" for f n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
proof (cases "the (delay i (f \<triangleright> n)) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. the (delay i (f \<triangleright> n)) = 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
 2. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n)) = 0

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

goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
using totalizer_def \<open>\<psi> d \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n)) = 0
totalizer ?d ?i ?x \<equiv> if the (delay ?i ?x) = 0 then Some ?d else \<phi> ?i (e_take (the (delay ?i ?x)) ?x)
\<psi> d \<in> U

goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
the (delay i (f \<triangleright> n)) \<noteq> 0

goal (1 subgoal):
 1. the (delay i (f \<triangleright> n)) \<noteq> 0 \<Longrightarrow> \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (delay i (f \<triangleright> n)) \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n)) \<noteq> 0

goal (1 subgoal):
 1. \<psi> (the (totalizer d i (f \<triangleright> n))) \<in> U
[PROOF STEP]
using that env assms totalizer_init learn_cpE(3)
[PROOF STATE]
proof (prove)
using this:
the (delay i (f \<triangleright> n)) \<noteq> 0
f \<in> U
environment \<psi> U (totalizer d i)
learn_cp \<psi> U (\<phi> i)
?f \<in> \<R> \<Longrightarrow> 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)))
\<lbrakk>learn_cp ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> ?\<psi> (the (?s (?f \<triangleright> ?n))) \<in> ?U

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f \<in> U \<Longrightarrow> \<psi> (the (totalizer d i (?f \<triangleright> ?n))) \<in> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
learn_cp \<psi> U (totalizer d i)

goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>d. learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
learn_cp \<psi> U (totalizer d i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
learn_cp \<psi> U (totalizer d i)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prefixes_length: "length (prefixes z i j x) = Suc x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (local.prefixes z i j x) = Suc x
[PROOF STEP]
by (induction x) simp_all


[STATEMENT]
lemma init_adverse_eq_prefixes: "(adverse z i j) \<triangleright> n = list_encode (prefixes z i j n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j \<triangleright> n = Partial_Recursive.list_encode (local.prefixes z i j n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.adverse z i j \<triangleright> n = Partial_Recursive.list_encode (local.prefixes z i j n)
[PROOF STEP]
have "prefix (adverse z i j) n = prefixes z i j n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (local.adverse z i j) n = local.prefixes z i j n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prefix (local.adverse z i j) 0 = local.prefixes z i j 0
 2. \<And>n. prefix (local.adverse z i j) n = local.prefixes z i j n \<Longrightarrow> prefix (local.adverse z i j) (Suc n) = local.prefixes z i j (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. prefix (local.adverse z i j) 0 = local.prefixes z i j 0
 2. \<And>n. prefix (local.adverse z i j) n = local.prefixes z i j n \<Longrightarrow> prefix (local.adverse z i j) (Suc n) = local.prefixes z i j (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (local.adverse z i j) 0 = local.prefixes z i j 0
[PROOF STEP]
using adverse_def prefixes_length prefixI'
[PROOF STATE]
proof (prove)
using this:
local.adverse ?z ?i ?j ?x \<equiv> Some (last (local.prefixes ?z ?i ?j ?x))
length (local.prefixes ?z ?i ?j ?x) = Suc ?x
\<lbrakk>length ?vs = Suc ?n; \<And>x. x < Suc ?n \<Longrightarrow> ?f x \<down>= ?vs ! x\<rbrakk> \<Longrightarrow> prefix ?f ?n = ?vs

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

goal (1 subgoal):
 1. \<And>n. prefix (local.adverse z i j) n = local.prefixes z i j n \<Longrightarrow> prefix (local.adverse z i j) (Suc n) = local.prefixes z i j (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. prefix (local.adverse z i j) n = local.prefixes z i j n \<Longrightarrow> prefix (local.adverse z i j) (Suc n) = local.prefixes z i j (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
prefix (local.adverse z i j) n = local.prefixes z i j n

goal (1 subgoal):
 1. \<And>n. prefix (local.adverse z i j) n = local.prefixes z i j n \<Longrightarrow> prefix (local.adverse z i j) (Suc n) = local.prefixes z i j (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prefix (local.adverse z i j) n = local.prefixes z i j n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
prefix (local.adverse z i j) n = local.prefixes z i j n

goal (1 subgoal):
 1. prefix (local.adverse z i j) (Suc n) = local.prefixes z i j (Suc n)
[PROOF STEP]
using adverse_def
[PROOF STATE]
proof (prove)
using this:
prefix (local.adverse z i j) n = local.prefixes z i j n
local.adverse ?z ?i ?j ?x \<equiv> Some (last (local.prefixes ?z ?i ?j ?x))

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

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

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> n = Partial_Recursive.list_encode (local.prefixes z i j n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prefix (local.adverse z i j) n = local.prefixes z i j n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prefix (local.adverse z i j) n = local.prefixes z i j n

goal (1 subgoal):
 1. local.adverse z i j \<triangleright> n = Partial_Recursive.list_encode (local.prefixes z i j n)
[PROOF STEP]
by (simp add: init_def)
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<triangleright> n = Partial_Recursive.list_encode (local.prefixes z i j n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adverse_at_01:
  "adverse z i j 0 \<down>= i"
  "adverse z i j 1 \<down>= j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j 0 \<down>= i &&& local.adverse z i j 1 \<down>= j
[PROOF STEP]
by (auto simp add: adverse_def)