[STATEMENT]
lemma bangPres:
  fixes P :: pi
  and   Q :: pi

  assumes PBiSimQ: "P \<sim> Q"

  shows "!P \<sim> !Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
let ?X = "bangRel bisim"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
from PBiSimQ
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(!P, !Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (!P, !Q) \<in> bangRel bisim
[PROOF STEP]
by(rule BRBang)
[PROOF STATE]
proof (state)
this:
(!P, !Q) \<in> bangRel bisim

goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(!P, !Q) \<in> bangRel bisim

goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
proof(coinduct rule: bisimWeakCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> P \<leadsto>[bangRel bisim] Q
 2. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
case(cSim bP bQ)
[PROOF STATE]
proof (state)
this:
(bP, bQ) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> P \<leadsto>[bangRel bisim] Q
 2. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(bP, bQ) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> P \<leadsto>[bangRel bisim] Q
 2. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> P \<leadsto>[bangRel bisim] Q
 2. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
assume "(P, Q) \<in> ?X"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> P \<leadsto>[bangRel bisim] Q
 2. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
hence "P \<leadsto>[?X] Q"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> bangRel bisim

goal (1 subgoal):
 1. P \<leadsto>[bangRel bisim] Q
[PROOF STEP]
proof(induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> !P \<leadsto>[bangRel bisim] !Q
 2. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> !P \<leadsto>[bangRel bisim] !Q
 2. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume "P \<sim> Q"
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (3 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> !P \<leadsto>[bangRel bisim] !Q
 2. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
thus "!P \<leadsto>[?X] !Q"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. !P \<leadsto>[bangRel bisim] !Q
[PROOF STEP]
using bisimE(1) eqvt
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q
?P \<sim> ?Q \<Longrightarrow> ?P \<leadsto>[bisim] ?Q
eqvt bisim

goal (1 subgoal):
 1. !P \<leadsto>[bangRel bisim] !Q
[PROOF STEP]
by(rule Strong_Early_Sim_Pres.bangPres)
[PROOF STATE]
proof (state)
this:
!P \<leadsto>[bangRel bisim] !Q

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
fix P Q R T
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume RBiSimT: "R \<sim> T"
[PROOF STATE]
proof (state)
this:
R \<sim> T

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume PBangRelQ: "(P, Q) \<in> ?X"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume PSimQ: "P \<leadsto>[?X] Q"
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
from RBiSimT
[PROOF STATE]
proof (chain)
picking this:
R \<sim> T
[PROOF STEP]
have "R \<leadsto>[bisim] T"
[PROOF STATE]
proof (prove)
using this:
R \<sim> T

goal (1 subgoal):
 1. R \<leadsto>[bisim] T
[PROOF STEP]
by(blast dest: bisimE)
[PROOF STATE]
proof (state)
this:
R \<leadsto>[bisim] T

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
thus "R \<parallel> P \<leadsto>[?X] T \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[bisim] T

goal (1 subgoal):
 1. R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
[PROOF STEP]
using PSimQ RBiSimT PBangRelQ BRPar BRRes eqvt eqvtBangRel
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[bisim] T
P \<leadsto>[bangRel bisim] Q
R \<sim> T
(P, Q) \<in> bangRel bisim
\<lbrakk>(?R, ?T) \<in> ?Rel; (?P, ?Q) \<in> bangRel ?Rel\<rbrakk> \<Longrightarrow> (?R \<parallel> ?P, ?T \<parallel> ?Q) \<in> bangRel ?Rel
(?P, ?Q) \<in> bangRel ?Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> bangRel ?Rel
eqvt bisim
eqvt ?Rel \<Longrightarrow> eqvt (bangRel ?Rel)

goal (1 subgoal):
 1. R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
[PROOF STEP]
by(blast intro: Strong_Early_Sim_Pres.parCompose)
[PROOF STATE]
proof (state)
this:
R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
fix P Q a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume "P \<leadsto>[?X] Q"
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
from eqvtBangRel eqvt
[PROOF STATE]
proof (chain)
picking this:
eqvt ?Rel \<Longrightarrow> eqvt (bangRel ?Rel)
eqvt bisim
[PROOF STEP]
have "eqvt ?X"
[PROOF STATE]
proof (prove)
using this:
eqvt ?Rel \<Longrightarrow> eqvt (bangRel ?Rel)
eqvt bisim

goal (1 subgoal):
 1. eqvt (bangRel bisim)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eqvt (bangRel bisim)

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[bangRel bisim] Q
eqvt (bangRel bisim)
[PROOF STEP]
show "<\<nu>a>P \<leadsto>[?X] <\<nu>a>Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bangRel bisim] Q
eqvt (bangRel bisim)

goal (1 subgoal):
 1. <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
using BRRes
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bangRel bisim] Q
eqvt (bangRel bisim)
(?P, ?Q) \<in> bangRel ?Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> bangRel ?Rel

goal (1 subgoal):
 1. <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
by(blast intro: Strong_Early_Sim_Pres.resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> P \<leadsto>[bangRel bisim] Q
 2. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?Pa2, ?Qa2) \<in> bangRel bisim \<Longrightarrow> ?Pa2 \<leadsto>[bangRel bisim] ?Qa2

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> P \<leadsto>[bangRel bisim] Q
 2. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
with \<open>(bP, bQ) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(bP, bQ) \<in> bangRel bisim
(?Pa2, ?Qa2) \<in> bangRel bisim \<Longrightarrow> ?Pa2 \<leadsto>[bangRel bisim] ?Qa2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(bP, bQ) \<in> bangRel bisim
(?Pa2, ?Qa2) \<in> bangRel bisim \<Longrightarrow> ?Pa2 \<leadsto>[bangRel bisim] ?Qa2

goal (1 subgoal):
 1. bP \<leadsto>[bangRel bisim] bQ
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bP \<leadsto>[bangRel bisim] bQ

goal (1 subgoal):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
case(cSym bP bQ)
[PROOF STATE]
proof (state)
this:
(bP, bQ) \<in> bangRel bisim

goal (1 subgoal):
 1. \<And>P Q. (P, Q) \<in> bangRel bisim \<Longrightarrow> (Q, P) \<in> bangRel bisim
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(bP, bQ) \<in> bangRel bisim

goal (1 subgoal):
 1. (bQ, bP) \<in> bangRel bisim
[PROOF STEP]
by(metis bangRelSymetric bisimE)
[PROOF STATE]
proof (state)
this:
(bQ, bP) \<in> bangRel bisim

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
!P \<sim> !Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rmge2:
  assumes "xs = list_decode e"
  shows "rmge2 e =
   (if \<forall>i<length xs. xs ! i < 2 then Some 0
    else Some (xs ! (GREATEST i. i < length xs \<and> xs ! i \<ge> 2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
have "(i < e_length e \<and> e_nth e i \<ge> 2) = (i < length xs \<and> xs ! i \<ge> 2)" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < e_length e \<and> 2 \<le> e_nth e i) = (i < length xs \<and> 2 \<le> xs ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = Partial_Recursive.list_decode e

goal (1 subgoal):
 1. (i < e_length e \<and> 2 \<le> e_nth e i) = (i < length xs \<and> 2 \<le> xs ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(?i < e_length e \<and> 2 \<le> e_nth e ?i) = (?i < length xs \<and> 2 \<le> xs ! ?i)

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?i < e_length e \<and> 2 \<le> e_nth e ?i) = (?i < length xs \<and> 2 \<le> xs ! ?i)
[PROOF STEP]
have "(GREATEST i. i < e_length e \<and> e_nth e i \<ge> 2) =
      (GREATEST i. i < length xs \<and> xs ! i \<ge> 2)"
[PROOF STATE]
proof (prove)
using this:
(?i < e_length e \<and> 2 \<le> e_nth e ?i) = (?i < length xs \<and> 2 \<le> xs ! ?i)

goal (1 subgoal):
 1. (GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i) = (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i) = (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i) = (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
have "(\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = Partial_Recursive.list_decode e

goal (1 subgoal):
 1. (\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
have "(GREATEST i. i < length xs \<and> xs ! i \<ge> 2) < length xs" (is "Greatest ?P < _")
      if "\<not> (\<forall>i<length xs. xs ! i < 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < length xs \<and> 2 \<le> xs ! i) < length xs
[PROOF STEP]
using that GreatestI_ex_nat[of ?P] le_less_linear order.asym
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i<length xs. xs ! i < 2)
\<lbrakk>\<exists>k<length xs. 2 \<le> xs ! k; \<And>y. y < length xs \<and> 2 \<le> xs ! y \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> (GREATEST i. i < length xs \<and> 2 \<le> xs ! i) < length xs \<and> 2 \<le> xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)
?x \<le> ?y \<or> ?y < ?x
\<lbrakk>?a < ?b; ?b < ?a\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (GREATEST i. i < length xs \<and> 2 \<le> xs ! i) < length xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i<length xs. xs ! i < 2) \<Longrightarrow> (GREATEST i. i < length xs \<and> 2 \<le> xs ! i) < length xs

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i) = (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)
(\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)
\<not> (\<forall>i<length xs. xs ! i < 2) \<Longrightarrow> (GREATEST i. i < length xs \<and> 2 \<le> xs ! i) < length xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i) = (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)
(\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)
\<not> (\<forall>i<length xs. xs ! i < 2) \<Longrightarrow> (GREATEST i. i < length xs \<and> 2 \<le> xs ! i) < length xs

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
using rmge2_def assms
[PROOF STATE]
proof (prove)
using this:
(GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i) = (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)
(\<forall>i<length xs. xs ! i < 2) = (\<forall>i<e_length e. e_nth e i < 2)
\<not> (\<forall>i<length xs. xs ! i < 2) \<Longrightarrow> (GREATEST i. i < length xs \<and> 2 \<le> xs ! i) < length xs
rmge2 ?e \<equiv> if \<forall>i<e_length ?e. e_nth ?e i < 2 then Some 0 else Some (e_nth ?e (GREATEST i. i < e_length ?e \<and> 2 \<le> e_nth ?e i))
xs = Partial_Recursive.list_decode e

goal (1 subgoal):
 1. rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rmge2 e = (if \<forall>i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs \<and> 2 \<le> xs ! i)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rmge2_in_R1: "rmge2 \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
define g where
    "g = Cn 3 r_ifle [r_constn 2 2, Cn 3 r_nth [Id 3 2, Id 3 0], Cn 3 r_nth [Id 3 2, Id 3 0], Id 3 1]"
[PROOF STATE]
proof (state)
this:
g = Cn 3 r_ifle [r_constn 2 2, Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], recf.Id 3 1]

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g = Cn 3 r_ifle [r_constn 2 2, Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], recf.Id 3 1]
[PROOF STEP]
have "recfn 3 g"
[PROOF STATE]
proof (prove)
using this:
g = Cn 3 r_ifle [r_constn 2 2, Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], recf.Id 3 1]

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

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
recfn 3 g
[PROOF STEP]
have g: "eval g [j, r, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else r)" for j r e
[PROOF STATE]
proof (prove)
using this:
recfn 3 g

goal (1 subgoal):
 1. eval g [j, r, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else r)
[PROOF STEP]
using g_def
[PROOF STATE]
proof (prove)
using this:
recfn 3 g
g = Cn 3 r_ifle [r_constn 2 2, Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], Cn 3 r_nth [recf.Id 3 2, recf.Id 3 0], recf.Id 3 1]

goal (1 subgoal):
 1. eval g [j, r, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval g [?j, ?r, ?e] \<down>= (if 2 \<le> e_nth ?e ?j then e_nth ?e ?j else ?r)

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
let ?h = "Pr 1 Z g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
have "recfn 2 ?h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (Pr 1 Z g)
[PROOF STEP]
by (simp add: \<open>recfn 3 g\<close>)
[PROOF STATE]
proof (state)
this:
recfn 2 (Pr 1 Z g)

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
have h: "eval ?h [j, e] =
   (if \<forall>i<j. e_nth e i < 2 then Some 0
    else Some (e_nth e (GREATEST i. i < j \<and> e_nth e i \<ge> 2)))" for j e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
proof (induction j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval (Pr 1 Z g) [0, e] = (if \<forall>i<0. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < 0 \<and> 2 \<le> e_nth e i)))
 2. \<And>j. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. eval (Pr 1 Z g) [0, e] = (if \<forall>i<0. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < 0 \<and> 2 \<le> e_nth e i)))
 2. \<And>j. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 Z g) [0, e] = (if \<forall>i<0. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < 0 \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
using \<open>recfn 2 ?h\<close>
[PROOF STATE]
proof (prove)
using this:
recfn 2 (Pr 1 Z g)

goal (1 subgoal):
 1. eval (Pr 1 Z g) [0, e] = (if \<forall>i<0. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < 0 \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [0, e] = (if \<forall>i<0. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < 0 \<and> 2 \<le> e_nth e i)))

goal (1 subgoal):
 1. \<And>j. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)))

goal (1 subgoal):
 1. \<And>j. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
have "eval ?h [Suc j, e] = eval g [j, the (eval ?h [j, e]), e]"
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)))

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = eval g [j, the (eval (Pr 1 Z g) [j, e]), e]
[PROOF STEP]
using \<open>recfn 2 ?h\<close>
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)))
recfn 2 (Pr 1 Z g)

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = eval g [j, the (eval (Pr 1 Z g) [j, e]), e]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] = eval g [j, the (eval (Pr 1 Z g) [j, e]), e]

goal (1 subgoal):
 1. \<And>j. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 Z g) [Suc j, e] = eval g [j, the (eval (Pr 1 Z g) [j, e]), e]
[PROOF STEP]
have *: "eval ?h [Suc j, e] \<down>=
      (if 2 \<le> e_nth e j then e_nth e j
       else if \<forall>i<j. e_nth e i < 2 then 0
            else (e_nth e (GREATEST i. i < j \<and> e_nth e i \<ge> 2)))"
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] = eval g [j, the (eval (Pr 1 Z g) [j, e]), e]

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))
[PROOF STEP]
using g Suc
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] = eval g [j, the (eval (Pr 1 Z g) [j, e]), e]
eval g [?j, ?r, ?e] \<down>= (if 2 \<le> e_nth ?e ?j then e_nth ?e ?j else ?r)
eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)))

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))

goal (1 subgoal):
 1. \<And>j. eval (Pr 1 Z g) [j, e] = (if \<forall>i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
proof (cases "\<forall>i<Suc j. e_nth e i < 2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>i<Suc j. e_nth e i < 2 \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
 2. \<not> (\<forall>i<Suc j. e_nth e i < 2) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>i<Suc j. e_nth e i < 2

goal (2 subgoals):
 1. \<forall>i<Suc j. e_nth e i < 2 \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
 2. \<not> (\<forall>i<Suc j. e_nth e i < 2) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<Suc j. e_nth e i < 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i<Suc j. e_nth e i < 2

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<forall>i<Suc j. e_nth e i < 2
eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))

goal (1 subgoal):
 1. \<not> (\<forall>i<Suc j. e_nth e i < 2) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>i<Suc j. e_nth e i < 2) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
case ex: False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i<Suc j. e_nth e i < 2)

goal (1 subgoal):
 1. \<not> (\<forall>i<Suc j. e_nth e i < 2) \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
proof (cases "2 \<le> e_nth e j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
 2. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
2 \<le> e_nth e j

goal (2 subgoals):
 1. 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
 2. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> e_nth e j
[PROOF STEP]
have "eval ?h [Suc j, e] \<down>= e_nth e j"
[PROOF STATE]
proof (prove)
using this:
2 \<le> e_nth e j

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e j
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
2 \<le> e_nth e j
eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e j

goal (2 subgoals):
 1. 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
 2. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e j

goal (2 subgoals):
 1. 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
 2. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
have "(GREATEST i. i < Suc j \<and> e_nth e i \<ge> 2) = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = j
[PROOF STEP]
using ex True Greatest_equality[of "\<lambda>i.  i < Suc j \<and> e_nth e i \<ge> 2"]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i<Suc j. e_nth e i < 2)
2 \<le> e_nth e j
\<lbrakk>?x < Suc j \<and> 2 \<le> e_nth e ?x; \<And>y. y < Suc j \<and> 2 \<le> e_nth e y \<Longrightarrow> y \<le> ?x\<rbrakk> \<Longrightarrow> (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = ?x

goal (1 subgoal):
 1. (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = j

goal (2 subgoals):
 1. 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
 2. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e j
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e j
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = j

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
using ex
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e j
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = j
\<not> (\<forall>i<Suc j. e_nth e i < 2)

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))

goal (1 subgoal):
 1. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 2 \<le> e_nth e j

goal (1 subgoal):
 1. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 2 \<le> e_nth e j
[PROOF STEP]
have "\<exists>i<j. e_nth e i \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<not> 2 \<le> e_nth e j

goal (1 subgoal):
 1. \<exists>i<j. 2 \<le> e_nth e i
[PROOF STEP]
using ex leI less_Suc_eq
[PROOF STATE]
proof (prove)
using this:
\<not> 2 \<le> e_nth e j
\<not> (\<forall>i<Suc j. e_nth e i < 2)
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)

goal (1 subgoal):
 1. \<exists>i<j. 2 \<le> e_nth e i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i<j. 2 \<le> e_nth e i

goal (1 subgoal):
 1. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))
\<exists>i<j. 2 \<le> e_nth e i
[PROOF STEP]
have "eval ?h [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> e_nth e i \<ge> 2)"
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))
\<exists>i<j. 2 \<le> e_nth e i

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] \<down>= (if 2 \<le> e_nth e j then e_nth e j else if \<forall>i<j. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i))
\<exists>i<j. 2 \<le> e_nth e i
\<not> 2 \<le> e_nth e j

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
[PROOF STEP]
by (smt leD)
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)

goal (1 subgoal):
 1. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)

goal (1 subgoal):
 1. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
have "(GREATEST i. i < Suc j \<and> e_nth e i \<ge> 2) =
            (GREATEST i. i < j \<and> e_nth e i \<ge> 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
[PROOF STEP]
using False ex
[PROOF STATE]
proof (prove)
using this:
\<not> 2 \<le> e_nth e j
\<not> (\<forall>i<Suc j. e_nth e i < 2)

goal (1 subgoal):
 1. (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
[PROOF STEP]
by (metis less_SucI less_Suc_eq less_antisym numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = (GREATEST i. i < j \<and> 2 \<le> e_nth e i)

goal (1 subgoal):
 1. \<not> 2 \<le> e_nth e j \<Longrightarrow> eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = (GREATEST i. i < j \<and> 2 \<le> e_nth e i)

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
using ex
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [Suc j, e] \<down>= e_nth e (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
(GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i) = (GREATEST i. i < j \<and> 2 \<le> e_nth e i)
\<not> (\<forall>i<Suc j. e_nth e i < 2)

goal (1 subgoal):
 1. eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [Suc j, e] = (if \<forall>i<Suc j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < Suc j \<and> 2 \<le> e_nth e i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval (Pr 1 Z g) [?j, ?e] = (if \<forall>i<?j. e_nth ?e i < 2 then Some 0 else Some (e_nth ?e (GREATEST i. i < ?j \<and> 2 \<le> e_nth ?e i)))

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
let ?hh = "Cn 1 ?h [Cn 1 r_length [Id 1 0], Id 1 0]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
have "recfn 1 ?hh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])
[PROOF STEP]
using \<open>recfn 2 ?h\<close>
[PROOF STATE]
proof (prove)
using this:
recfn 2 (Pr 1 Z g)

goal (1 subgoal):
 1. recfn 1 (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
with h
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 Z g) [?j, ?e] = (if \<forall>i<?j. e_nth ?e i < 2 then Some 0 else Some (e_nth ?e (GREATEST i. i < ?j \<and> 2 \<le> e_nth ?e i)))
recfn 1 (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])
[PROOF STEP]
have hh: "eval ?hh [e] \<down>=
    (if \<forall>i<e_length e. e_nth e i < 2 then 0
     else e_nth e (GREATEST i. i < e_length e \<and> e_nth e i \<ge> 2))" for e
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 Z g) [?j, ?e] = (if \<forall>i<?j. e_nth ?e i < 2 then Some 0 else Some (e_nth ?e (GREATEST i. i < ?j \<and> 2 \<le> e_nth ?e i)))
recfn 1 (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])

goal (1 subgoal):
 1. eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [e] \<down>= (if \<forall>i<e_length e. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] \<down>= (if \<forall>i<e_length ?e. e_nth ?e i < 2 then 0 else e_nth ?e (GREATEST i. i < e_length ?e \<and> 2 \<le> e_nth ?e i))

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] \<down>= (if \<forall>i<e_length ?e. e_nth ?e i < 2 then 0 else e_nth ?e (GREATEST i. i < e_length ?e \<and> 2 \<le> e_nth ?e i))
[PROOF STEP]
have "eval ?hh [e] = rmge2 e" for e
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] \<down>= (if \<forall>i<e_length ?e. e_nth ?e i < 2 then 0 else e_nth ?e (GREATEST i. i < e_length ?e \<and> 2 \<le> e_nth ?e i))

goal (1 subgoal):
 1. eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [e] = rmge2 e
[PROOF STEP]
unfolding rmge2_def
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] \<down>= (if \<forall>i<e_length ?e. e_nth ?e i < 2 then 0 else e_nth ?e (GREATEST i. i < e_length ?e \<and> 2 \<le> e_nth ?e i))

goal (1 subgoal):
 1. eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [e] = (if \<forall>i<e_length e. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < e_length e \<and> 2 \<le> e_nth e i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] = rmge2 ?e

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] = rmge2 ?e

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
have "total ?hh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Recursive.total (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])
[PROOF STEP]
using hh totalI1 \<open>recfn 1 ?hh\<close>
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] \<down>= (if \<forall>i<e_length ?e. e_nth ?e i < 2 then 0 else e_nth ?e (GREATEST i. i < e_length ?e \<and> 2 \<le> e_nth ?e i))
\<lbrakk>recfn 1 ?f; \<And>x. eval ?f [x] \<down>\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f
recfn 1 (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])

goal (1 subgoal):
 1. Partial_Recursive.total (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Partial_Recursive.total (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] = rmge2 ?e
Partial_Recursive.total (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] = rmge2 ?e
Partial_Recursive.total (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])

goal (1 subgoal):
 1. rmge2 \<in> \<R>
[PROOF STEP]
using \<open>recfn 1 ?hh\<close>
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0]) [?e] = rmge2 ?e
Partial_Recursive.total (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])
recfn 1 (Cn 1 (Pr 1 Z g) [Cn 1 r_length [recf.Id 1 0], recf.Id 1 0])

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma U_LIMCONS_in_Lim: "U\<^bsub>LIM-CONS\<^esub> \<in> LIM"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> LIM
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> LIM
[PROOF STEP]
have "U\<^bsub>LIM-CONS\<^esub> \<subseteq> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<subseteq> \<R>
[PROOF STEP]
unfolding U_LIMCONS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {vs @ [j] \<odot> p |vs j p. 2 \<le> j \<and> p \<in> \<R>\<^sub>0\<^sub>1 \<and> \<phi> j = vs @ [j] \<odot> p} \<subseteq> \<R>
[PROOF STEP]
using prepend_in_R1 RPred1_subseteq_R1
[PROOF STATE]
proof (prove)
using this:
?f \<in> \<R> \<Longrightarrow> ?vs \<odot> ?f \<in> \<R>
\<R>\<^sub>0\<^sub>1 \<subseteq> \<R>

goal (1 subgoal):
 1. {vs @ [j] \<odot> p |vs j p. 2 \<le> j \<and> p \<in> \<R>\<^sub>0\<^sub>1 \<and> \<phi> j = vs @ [j] \<odot> p} \<subseteq> \<R>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
U\<^bsub>LIM-CONS\<^esub> \<subseteq> \<R>

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> LIM
[PROOF STEP]
have "learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2
[PROOF STEP]
proof (rule learn_limI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. environment \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2
 2. \<And>f. f \<in> U\<^bsub>LIM-CONS\<^esub> \<Longrightarrow> \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
show "environment \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. environment \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2
[PROOF STEP]
using \<open>U_LIMCONS \<subseteq> \<R>\<close> phi_in_P2 rmge2_def rmge2_in_R1
[PROOF STATE]
proof (prove)
using this:
U\<^bsub>LIM-CONS\<^esub> \<subseteq> \<R>
\<phi> \<in> \<P>\<^sup>2
rmge2 ?e \<equiv> if \<forall>i<e_length ?e. e_nth ?e i < 2 then Some 0 else Some (e_nth ?e (GREATEST i. i < e_length ?e \<and> 2 \<le> e_nth ?e i))
rmge2 \<in> \<R>

goal (1 subgoal):
 1. environment \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
environment \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2

goal (1 subgoal):
 1. \<And>f. f \<in> U\<^bsub>LIM-CONS\<^esub> \<Longrightarrow> \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
show "\<exists>i. \<phi> i = f \<and> (\<forall>\<^sup>\<infinity>n. rmge2 (f \<triangleright> n) \<down>= i)" if "f \<in> U\<^bsub>LIM-CONS\<^esub>" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
f \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
obtain vs j p where
        j: "j \<ge> 2"
        and p: "p \<in> \<R>\<^sub>0\<^sub>1"
        and s: "\<phi> j = vs @ [j] \<odot> p"
        and f: "f = vs @ [j] \<odot> p"
[PROOF STATE]
proof (prove)
using this:
f \<in> U\<^bsub>LIM-CONS\<^esub>

goal (1 subgoal):
 1. (\<And>j p vs. \<lbrakk>2 \<le> j; p \<in> \<R>\<^sub>0\<^sub>1; \<phi> j = vs @ [j] \<odot> p; f = vs @ [j] \<odot> p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding U_LIMCONS_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {vs @ [j] \<odot> p |vs j p. 2 \<le> j \<and> p \<in> \<R>\<^sub>0\<^sub>1 \<and> \<phi> j = vs @ [j] \<odot> p}

goal (1 subgoal):
 1. (\<And>j p vs. \<lbrakk>2 \<le> j; p \<in> \<R>\<^sub>0\<^sub>1; \<phi> j = vs @ [j] \<odot> p; f = vs @ [j] \<odot> p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 \<le> j
p \<in> \<R>\<^sub>0\<^sub>1
\<phi> j = vs @ [j] \<odot> p
f = vs @ [j] \<odot> p

goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> j
p \<in> \<R>\<^sub>0\<^sub>1
\<phi> j = vs @ [j] \<odot> p
f = vs @ [j] \<odot> p
[PROOF STEP]
have "\<phi> j = f"
[PROOF STATE]
proof (prove)
using this:
2 \<le> j
p \<in> \<R>\<^sub>0\<^sub>1
\<phi> j = vs @ [j] \<odot> p
f = vs @ [j] \<odot> p

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

goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
f \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
have "total1 f"
[PROOF STATE]
proof (prove)
using this:
f \<in> U\<^bsub>LIM-CONS\<^esub>

goal (1 subgoal):
 1. total1 f
[PROOF STEP]
using \<open>U\<^bsub>LIM-CONS\<^esub> \<subseteq> \<R>\<close> R1_imp_total1 total1_def
[PROOF STATE]
proof (prove)
using this:
f \<in> U\<^bsub>LIM-CONS\<^esub>
U\<^bsub>LIM-CONS\<^esub> \<subseteq> \<R>
?f \<in> \<R> \<Longrightarrow> total1 ?f
total1 ?f \<equiv> \<forall>x. ?f x \<down>

goal (1 subgoal):
 1. total1 f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
total1 f

goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
define n\<^sub>0 where "n\<^sub>0 = length vs"
[PROOF STATE]
proof (state)
this:
n\<^sub>0 = length vs

goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
have f_gr_n0: "f n \<down>= 0 \<or> f n \<down>= 1" if "n > n\<^sub>0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<down>= 0 \<or> f n \<down>= 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n \<down>= 0 \<or> f n \<down>= 1
[PROOF STEP]
have "f n = p (n - n\<^sub>0 - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n = p (n - n\<^sub>0 - 1)
[PROOF STEP]
using that n\<^sub>0_def f
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 < n
n\<^sub>0 = length vs
f = vs @ [j] \<odot> p

goal (1 subgoal):
 1. f n = p (n - n\<^sub>0 - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f n = p (n - n\<^sub>0 - 1)

goal (1 subgoal):
 1. f n \<down>= 0 \<or> f n \<down>= 1
[PROOF STEP]
with RPred1_def p
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>0\<^sub>1 \<equiv> {f \<in> \<R>. \<forall>x. f x \<down>= 0 \<or> f x \<down>= 1}
p \<in> \<R>\<^sub>0\<^sub>1
f n = p (n - n\<^sub>0 - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>0\<^sub>1 \<equiv> {f \<in> \<R>. \<forall>x. f x \<down>= 0 \<or> f x \<down>= 1}
p \<in> \<R>\<^sub>0\<^sub>1
f n = p (n - n\<^sub>0 - 1)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n\<^sub>0 < ?n \<Longrightarrow> f ?n \<down>= 0 \<or> f ?n \<down>= 1

goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
have "rmge2 (f \<triangleright> n) \<down>= j" if "n \<ge> n\<^sub>0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) \<down>= j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) \<down>= j
[PROOF STEP]
have n0_greatest: "(GREATEST i. i < Suc n \<and> the (f i) \<ge> 2) = n\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = n\<^sub>0
[PROOF STEP]
proof (rule Greatest_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n\<^sub>0 < Suc n \<and> 2 \<le> the (f n\<^sub>0)
 2. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
show "n\<^sub>0 < Suc n \<and> the (f n\<^sub>0) \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n\<^sub>0 < Suc n \<and> 2 \<le> the (f n\<^sub>0)
[PROOF STEP]
using n\<^sub>0_def f that j
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 = length vs
f = vs @ [j] \<odot> p
n\<^sub>0 \<le> n
2 \<le> j

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

goal (1 subgoal):
 1. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
show "\<And>y. y < Suc n \<and> the (f y) \<ge> 2 \<Longrightarrow> y \<le> n\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
assume "y < Suc n \<and> 2 \<le> the (f y)"
[PROOF STATE]
proof (state)
this:
y < Suc n \<and> 2 \<le> the (f y)

goal (1 subgoal):
 1. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y < Suc n \<and> 2 \<le> the (f y)

goal (1 subgoal):
 1. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
have "p \<in> \<R> \<and> (\<forall>n. p n \<down>= 0 \<or> p n \<down>= 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<R> \<and> (\<forall>n. p n \<down>= 0 \<or> p n \<down>= 1)
[PROOF STEP]
using RPred1_def p
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>0\<^sub>1 \<equiv> {f \<in> \<R>. \<forall>x. f x \<down>= 0 \<or> f x \<down>= 1}
p \<in> \<R>\<^sub>0\<^sub>1

goal (1 subgoal):
 1. p \<in> \<R> \<and> (\<forall>n. p n \<down>= 0 \<or> p n \<down>= 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> \<R> \<and> (\<forall>n. p n \<down>= 0 \<or> p n \<down>= 1)

goal (1 subgoal):
 1. \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<^sub>0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y < Suc n \<and> 2 \<le> the (f y)
p \<in> \<R> \<and> (\<forall>n. p n \<down>= 0 \<or> p n \<down>= 1)
[PROOF STEP]
show "y \<le> n\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
y < Suc n \<and> 2 \<le> the (f y)
p \<in> \<R> \<and> (\<forall>n. p n \<down>= 0 \<or> p n \<down>= 1)

goal (1 subgoal):
 1. y \<le> n\<^sub>0
[PROOF STEP]
using f_gr_n0
[PROOF STATE]
proof (prove)
using this:
y < Suc n \<and> 2 \<le> the (f y)
p \<in> \<R> \<and> (\<forall>n. p n \<down>= 0 \<or> p n \<down>= 1)
n\<^sub>0 < ?n \<Longrightarrow> f ?n \<down>= 0 \<or> f ?n \<down>= 1

goal (1 subgoal):
 1. y \<le> n\<^sub>0
[PROOF STEP]
by (metis Suc_1 Suc_n_not_le_n Zero_neq_Suc le_less_linear le_zero_eq option.sel)
[PROOF STATE]
proof (state)
this:
y \<le> n\<^sub>0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?y < Suc n \<and> 2 \<le> the (f ?y) \<Longrightarrow> ?y \<le> n\<^sub>0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = n\<^sub>0

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) \<down>= j
[PROOF STEP]
have "f n\<^sub>0 \<down>= j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n\<^sub>0 \<down>= j
[PROOF STEP]
using n\<^sub>0_def f
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 = length vs
f = vs @ [j] \<odot> p

goal (1 subgoal):
 1. f n\<^sub>0 \<down>= j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f n\<^sub>0 \<down>= j

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) \<down>= j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f n\<^sub>0 \<down>= j
[PROOF STEP]
have "\<not> (\<forall>i<Suc n. the (f i) < 2)"
[PROOF STATE]
proof (prove)
using this:
f n\<^sub>0 \<down>= j

goal (1 subgoal):
 1. \<not> (\<forall>i<Suc n. the (f i) < 2)
[PROOF STEP]
using j that less_Suc_eq_le
[PROOF STATE]
proof (prove)
using this:
f n\<^sub>0 \<down>= j
2 \<le> j
n\<^sub>0 \<le> n
(?m < Suc ?n) = (?m \<le> ?n)

goal (1 subgoal):
 1. \<not> (\<forall>i<Suc n. the (f i) < 2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i<Suc n. the (f i) < 2)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) \<down>= j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>i<Suc n. the (f i) < 2)
[PROOF STEP]
have "rmge2 (f \<triangleright> n) = f (GREATEST i. i < Suc n \<and> the (f i) \<ge> 2)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i<Suc n. the (f i) < 2)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i))
[PROOF STEP]
using rmge2_init_total \<open>total1 f\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i<Suc n. the (f i) < 2)
total1 ?f \<Longrightarrow> rmge2 (?f \<triangleright> ?n) = (if \<forall>i<Suc ?n. the (?f i) < 2 then Some 0 else ?f (GREATEST i. i < Suc ?n \<and> 2 \<le> the (?f i)))
total1 f

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rmge2 (f \<triangleright> n) = f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i))

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) \<down>= j
[PROOF STEP]
with n0_greatest \<open>f n\<^sub>0 \<down>= j\<close>
[PROOF STATE]
proof (chain)
picking this:
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = n\<^sub>0
f n\<^sub>0 \<down>= j
rmge2 (f \<triangleright> n) = f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = n\<^sub>0
f n\<^sub>0 \<down>= j
rmge2 (f \<triangleright> n) = f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i))

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) \<down>= j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rmge2 (f \<triangleright> n) \<down>= j

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

goal (1 subgoal):
 1. \<exists>i. \<phi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (f \<triangleright> n) \<down>= i)
[PROOF STEP]
with \<open>\<phi> j = f\<close>
[PROOF STATE]
proof (chain)
picking this:
\<phi> j = f
n\<^sub>0 \<le> ?n \<Longrightarrow> rmge2 (f \<triangleright> ?n) \<down>= j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> j = f
n\<^sub>0 \<le> ?n \<Longrightarrow> rmge2 (f \<triangleright> ?n) \<down>= j

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f \<in> U\<^bsub>LIM-CONS\<^esub> \<Longrightarrow> \<exists>i. \<phi> i = ?f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. rmge2 (?f \<triangleright> n) \<down>= i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> LIM
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> LIM
[PROOF STEP]
using Lim_def
[PROOF STATE]
proof (prove)
using this:
learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> rmge2
LIM \<equiv> {U. \<exists>\<psi> s. learn_lim \<psi> U s}

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> LIM
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U\<^bsub>LIM-CONS\<^esub> \<in> LIM

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma goedel_at:
  fixes m :: nat and k :: nat
  assumes "f \<in> \<R>"
  shows "\<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)
[PROOF STEP]
define psi :: "partial1 \<Rightarrow> nat \<Rightarrow> partial2" where
    "psi = (\<lambda>f k i x. (if x = k then Some i else f x))"
[PROOF STATE]
proof (state)
this:
psi = (\<lambda>f k i x. if x = k then Some i else f x)

goal (1 subgoal):
 1. \<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)
[PROOF STEP]
have "psi f k \<in> \<R>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psi f k \<in> \<R>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psi f k \<in> \<R>\<^sup>2
[PROOF STEP]
obtain r where r: "recfn 1 r" "total r" "eval r [x] = f x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>recfn 1 r; Partial_Recursive.total r; \<And>x. eval r [x] = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>recfn 1 r; Partial_Recursive.total r; \<And>x. eval r [x] = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 r
Partial_Recursive.total r
eval r [?x] = f ?x

goal (1 subgoal):
 1. psi f k \<in> \<R>\<^sup>2
[PROOF STEP]
define r_psi where
      "r_psi = Cn 2 r_ifeq [Id 2 1, r_dummy 1 (r_const k), Id 2 0, Cn 2 r [Id 2 1]]"
[PROOF STATE]
proof (state)
this:
r_psi = Cn 2 r_ifeq [recf.Id 2 1, r_dummy 1 (r_const k), recf.Id 2 0, Cn 2 r [recf.Id 2 1]]

goal (1 subgoal):
 1. psi f k \<in> \<R>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psi f k \<in> \<R>\<^sup>2
[PROOF STEP]
proof (rule R2I[of r_psi])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. recfn 2 r_psi
 2. Partial_Recursive.total r_psi
 3. \<And>x y. eval r_psi [x, y] = psi f k x y
[PROOF STEP]
from r_psi_def
[PROOF STATE]
proof (chain)
picking this:
r_psi = Cn 2 r_ifeq [recf.Id 2 1, r_dummy 1 (r_const k), recf.Id 2 0, Cn 2 r [recf.Id 2 1]]
[PROOF STEP]
show "recfn 2 r_psi"
[PROOF STATE]
proof (prove)
using this:
r_psi = Cn 2 r_ifeq [recf.Id 2 1, r_dummy 1 (r_const k), recf.Id 2 0, Cn 2 r [recf.Id 2 1]]

goal (1 subgoal):
 1. recfn 2 r_psi
[PROOF STEP]
using r(1)
[PROOF STATE]
proof (prove)
using this:
r_psi = Cn 2 r_ifeq [recf.Id 2 1, r_dummy 1 (r_const k), recf.Id 2 0, Cn 2 r [recf.Id 2 1]]
recfn 1 r

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

goal (2 subgoals):
 1. Partial_Recursive.total r_psi
 2. \<And>x y. eval r_psi [x, y] = psi f k x y
[PROOF STEP]
have "eval r_psi [i, x] = (if x = k then Some i else f x)" for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_psi [i, x] = (if x = k then Some i else f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_psi [i, x] = (if x = k then Some i else f x)
[PROOF STEP]
have "eval (Cn 2 r [Id 2 1]) [i, x] = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 r [recf.Id 2 1]) [i, x] = f x
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
recfn 1 r
Partial_Recursive.total r
eval r [?x] = f ?x

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

goal (1 subgoal):
 1. eval r_psi [i, x] = (if x = k then Some i else f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 2 r [recf.Id 2 1]) [i, x] = f x
[PROOF STEP]
have "eval r_psi [i, x] = eval r_ifeq [x, k, i, the (f x)]"
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r [recf.Id 2 1]) [i, x] = f x

goal (1 subgoal):
 1. eval r_psi [i, x] = eval r_ifeq [x, k, i, the (f x)]
[PROOF STEP]
unfolding r_psi_def
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r [recf.Id 2 1]) [i, x] = f x

goal (1 subgoal):
 1. eval (Cn 2 r_ifeq [recf.Id 2 1, r_dummy 1 (r_const k), recf.Id 2 0, Cn 2 r [recf.Id 2 1]]) [i, x] = eval r_ifeq [x, k, i, the (f x)]
[PROOF STEP]
using \<open>recfn 2 r_psi\<close> r R1_imp_total1[OF assms]
[PROOF STATE]
proof (prove)
using this:
eval (Cn 2 r [recf.Id 2 1]) [i, x] = f x
recfn 2 r_psi
recfn 1 r
Partial_Recursive.total r
eval r [?x] = f ?x
total1 f

goal (1 subgoal):
 1. eval (Cn 2 r_ifeq [recf.Id 2 1, r_dummy 1 (r_const k), recf.Id 2 0, Cn 2 r [recf.Id 2 1]]) [i, x] = eval r_ifeq [x, k, i, the (f x)]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_psi [i, x] = eval r_ifeq [x, k, i, the (f x)]

goal (1 subgoal):
 1. eval r_psi [i, x] = (if x = k then Some i else f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_psi [i, x] = eval r_ifeq [x, k, i, the (f x)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval r_psi [i, x] = eval r_ifeq [x, k, i, the (f x)]

goal (1 subgoal):
 1. eval r_psi [i, x] = (if x = k then Some i else f x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eval r_psi [i, x] = eval r_ifeq [x, k, i, the (f x)]
f \<in> \<R>

goal (1 subgoal):
 1. eval r_psi [i, x] = (if x = k then Some i else f x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_psi [i, x] = (if x = k then Some i else f x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval r_psi [?i, ?x] = (if ?x = k then Some ?i else f ?x)

goal (2 subgoals):
 1. Partial_Recursive.total r_psi
 2. \<And>x y. eval r_psi [x, y] = psi f k x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_psi [?i, ?x] = (if ?x = k then Some ?i else f ?x)
[PROOF STEP]
show "\<And>x y. eval r_psi [x, y] = psi f k x y"
[PROOF STATE]
proof (prove)
using this:
eval r_psi [?i, ?x] = (if ?x = k then Some ?i else f ?x)

goal (1 subgoal):
 1. \<And>x y. eval r_psi [x, y] = psi f k x y
[PROOF STEP]
unfolding psi_def
[PROOF STATE]
proof (prove)
using this:
eval r_psi [?i, ?x] = (if ?x = k then Some ?i else f ?x)

goal (1 subgoal):
 1. \<And>x y. eval r_psi [x, y] = (if y = k then Some x else f y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_psi [?x, ?y] = psi f k ?x ?y

goal (1 subgoal):
 1. Partial_Recursive.total r_psi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_psi [?x, ?y] = psi f k ?x ?y
[PROOF STEP]
show "total r_psi"
[PROOF STATE]
proof (prove)
using this:
eval r_psi [?x, ?y] = psi f k ?x ?y

goal (1 subgoal):
 1. Partial_Recursive.total r_psi
[PROOF STEP]
using totalI2[of r_psi] \<open>recfn 2 r_psi\<close> assms psi_def
[PROOF STATE]
proof (prove)
using this:
eval r_psi [?x, ?y] = psi f k ?x ?y
\<lbrakk>recfn 2 r_psi; \<And>x y. eval r_psi [x, y] \<down>\<rbrakk> \<Longrightarrow> Partial_Recursive.total r_psi
recfn 2 r_psi
f \<in> \<R>
psi = (\<lambda>f k i x. if x = k then Some i else f x)

goal (1 subgoal):
 1. Partial_Recursive.total r_psi
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Partial_Recursive.total r_psi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
psi f k \<in> \<R>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
psi f k \<in> \<R>\<^sup>2

goal (1 subgoal):
 1. \<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
psi f k \<in> \<R>\<^sup>2
[PROOF STEP]
obtain n where "n \<ge> m" "\<phi> n = psi f k n"
[PROOF STATE]
proof (prove)
using this:
psi f k \<in> \<R>\<^sup>2

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>m \<le> n; \<phi> n = psi f k n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms kleene_fixed_point[of "psi f k" m]
[PROOF STATE]
proof (prove)
using this:
psi f k \<in> \<R>\<^sup>2
f \<in> \<R>
\<lbrakk>psi f k \<in> \<P>\<^sup>2; \<And>i. \<lbrakk>m \<le> i; \<phi> i = psi f k i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>m \<le> n; \<phi> n = psi f k n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<le> n
\<phi> n = psi f k n

goal (1 subgoal):
 1. \<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> n
\<phi> n = psi f k n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<le> n
\<phi> n = psi f k n

goal (1 subgoal):
 1. \<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)
[PROOF STEP]
unfolding psi_def
[PROOF STATE]
proof (prove)
using this:
m \<le> n
\<phi> n = (\<lambda>x. if x = k then Some n else f x)

goal (1 subgoal):
 1. \<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n\<ge>m. \<phi> n = (\<lambda>x. if x = k then Some n else f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma U_LIMCONS_prefix_complete:
  assumes "length vs > 0"
  shows "\<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
let ?p = "\<lambda>_. Some 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
let ?f = "vs @ [0] \<odot> ?p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
have "?f \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs @ [0] \<odot> 0\<^sup>\<infinity> \<in> \<R>
[PROOF STEP]
using prepend_in_R1 RPred1_subseteq_R1 const0_in_RPred1
[PROOF STATE]
proof (prove)
using this:
?f \<in> \<R> \<Longrightarrow> ?vs \<odot> ?f \<in> \<R>
\<R>\<^sub>0\<^sub>1 \<subseteq> \<R>
0\<^sup>\<infinity> \<in> \<R>\<^sub>0\<^sub>1

goal (1 subgoal):
 1. vs @ [0] \<odot> 0\<^sup>\<infinity> \<in> \<R>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vs @ [0] \<odot> 0\<^sup>\<infinity> \<in> \<R>

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
with goedel_at[of ?f 2 "length vs"]
[PROOF STATE]
proof (chain)
picking this:
vs @ [0] \<odot> 0\<^sup>\<infinity> \<in> \<R> \<Longrightarrow> \<exists>n\<ge>2. \<phi> n = (\<lambda>x. if x = length vs then Some n else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)
vs @ [0] \<odot> 0\<^sup>\<infinity> \<in> \<R>
[PROOF STEP]
obtain j where
    j: "j \<ge> 2" "\<phi> j = (\<lambda>x. if x = length vs then Some j else ?f x)" (is "_ = ?g")
[PROOF STATE]
proof (prove)
using this:
vs @ [0] \<odot> 0\<^sup>\<infinity> \<in> \<R> \<Longrightarrow> \<exists>n\<ge>2. \<phi> n = (\<lambda>x. if x = length vs then Some n else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)
vs @ [0] \<odot> 0\<^sup>\<infinity> \<in> \<R>

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>2 \<le> j; \<phi> j = (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 \<le> j
\<phi> j = (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
2 \<le> j
\<phi> j = (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
have g: "?g x = (vs @ [j] \<odot> ?p) x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) = (vs @ [j] \<odot> 0\<^sup>\<infinity>) x
[PROOF STEP]
by (simp add: nth_append)
[PROOF STATE]
proof (state)
this:
(if ?x1 = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) ?x1) = (vs @ [j] \<odot> 0\<^sup>\<infinity>) ?x1

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
2 \<le> j
\<phi> j = (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)
(if ?x1 = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) ?x1) = (vs @ [j] \<odot> 0\<^sup>\<infinity>) ?x1
[PROOF STEP]
have "?g \<in> U\<^bsub>LIM-CONS\<^esub>"
[PROOF STATE]
proof (prove)
using this:
2 \<le> j
\<phi> j = (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)
(if ?x1 = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) ?x1) = (vs @ [j] \<odot> 0\<^sup>\<infinity>) ?x1

goal (1 subgoal):
 1. (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
unfolding U_LIMCONS_def
[PROOF STATE]
proof (prove)
using this:
2 \<le> j
\<phi> j = (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)
(if ?x1 = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) ?x1) = (vs @ [j] \<odot> 0\<^sup>\<infinity>) ?x1

goal (1 subgoal):
 1. (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) \<in> {vs @ [j] \<odot> p |vs j p. 2 \<le> j \<and> p \<in> \<R>\<^sub>0\<^sub>1 \<and> \<phi> j = vs @ [j] \<odot> p}
[PROOF STEP]
using const0_in_RPred1
[PROOF STATE]
proof (prove)
using this:
2 \<le> j
\<phi> j = (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x)
(if ?x1 = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) ?x1) = (vs @ [j] \<odot> 0\<^sup>\<infinity>) ?x1
0\<^sup>\<infinity> \<in> \<R>\<^sub>0\<^sub>1

goal (1 subgoal):
 1. (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) \<in> {vs @ [j] \<odot> p |vs j p. 2 \<le> j \<and> p \<in> \<R>\<^sub>0\<^sub>1 \<and> \<phi> j = vs @ [j] \<odot> p}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) \<in> U\<^bsub>LIM-CONS\<^esub>

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) \<in> U\<^bsub>LIM-CONS\<^esub>

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
have "prefix ?g (length vs - 1) = vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) (length vs - 1) = vs
[PROOF STEP]
using g assms prefixI prepend_associative
[PROOF STATE]
proof (prove)
using this:
(if ?x1 = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) ?x1) = (vs @ [j] \<odot> 0\<^sup>\<infinity>) ?x1
0 < length vs
\<lbrakk>0 < length ?vs; \<And>x. x < length ?vs \<Longrightarrow> ?f x \<down>= ?vs ! x\<rbrakk> \<Longrightarrow> prefix ?f (length ?vs - 1) = ?vs
?us @ ?vs \<odot> ?f = ?us \<odot> ?vs \<odot> ?f

goal (1 subgoal):
 1. prefix (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) (length vs - 1) = vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prefix (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) (length vs - 1) = vs

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) \<in> U\<^bsub>LIM-CONS\<^esub>
prefix (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) (length vs - 1) = vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) \<in> U\<^bsub>LIM-CONS\<^esub>
prefix (\<lambda>x. if x = length vs then Some j else (vs @ [0] \<odot> 0\<^sup>\<infinity>) x) (length vs - 1) = vs

goal (1 subgoal):
 1. \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length vs - 1) = vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma U_prefix_complete_imp_total_strategy:
  assumes "\<And>vs. length vs > 0 \<Longrightarrow> \<exists>f\<in>U. prefix f (length vs - 1) = vs"
    and "learn_cons \<psi> U s"
  shows "\<exists>t. total1 t \<and> learn_cons \<psi> U t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
define t where "t = (\<lambda>e. if e = 0 then Some 0 else s e)"
[PROOF STATE]
proof (state)
this:
t = (\<lambda>e. if e = 0 then Some 0 else s e)

goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
have "s e \<down>" if "e > 0" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
0 < e
[PROOF STEP]
have "list_decode e \<noteq> []" (is "?vs \<noteq> _")
[PROOF STATE]
proof (prove)
using this:
0 < e

goal (1 subgoal):
 1. Partial_Recursive.list_decode e \<noteq> []
[PROOF STEP]
using list_encode_0 list_encode_decode
[PROOF STATE]
proof (prove)
using this:
0 < e
(Partial_Recursive.list_encode ?xs = 0) = (?xs = [])
Partial_Recursive.list_encode (Partial_Recursive.list_decode ?n) = ?n

goal (1 subgoal):
 1. Partial_Recursive.list_decode e \<noteq> []
[PROOF STEP]
by (metis less_imp_neq)
[PROOF STATE]
proof (state)
this:
Partial_Recursive.list_decode e \<noteq> []

goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Partial_Recursive.list_decode e \<noteq> []
[PROOF STEP]
have "length ?vs > 0"
[PROOF STATE]
proof (prove)
using this:
Partial_Recursive.list_decode e \<noteq> []

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

goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
0 < length ?vs \<Longrightarrow> \<exists>f\<in>U. prefix f (length ?vs - 1) = ?vs
0 < e_length e
[PROOF STEP]
obtain f where f: "f \<in> U" "prefix f (length ?vs - 1) = ?vs"
[PROOF STATE]
proof (prove)
using this:
0 < length ?vs \<Longrightarrow> \<exists>f\<in>U. prefix f (length ?vs - 1) = ?vs
0 < e_length e

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> U; prefix f (e_length e - 1) = Partial_Recursive.list_decode e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> U
prefix f (e_length e - 1) = Partial_Recursive.list_decode e

goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
with learn_cons_def learn_limE
[PROOF STATE]
proof (chain)
picking this:
learn_cons ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n k. k \<le> n \<longrightarrow> ?\<psi> (the (?s (f \<triangleright> n))) k = f k)
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
prefix f (e_length e - 1) = Partial_Recursive.list_decode e
[PROOF STEP]
have "s (f \<triangleright> (length ?vs - 1)) \<down>"
[PROOF STATE]
proof (prove)
using this:
learn_cons ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n k. k \<le> n \<longrightarrow> ?\<psi> (the (?s (f \<triangleright> n))) k = f k)
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
prefix f (e_length e - 1) = Partial_Recursive.list_decode e

goal (1 subgoal):
 1. s (f \<triangleright> (e_length e - 1)) \<down>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
learn_cons ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n k. k \<le> n \<longrightarrow> ?\<psi> (the (?s (f \<triangleright> n))) k = f k)
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
prefix f (e_length e - 1) = Partial_Recursive.list_decode e
learn_cons \<psi> U s

goal (1 subgoal):
 1. s (f \<triangleright> (e_length e - 1)) \<down>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s (f \<triangleright> (e_length e - 1)) \<down>

goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (f \<triangleright> (e_length e - 1)) \<down>
[PROOF STEP]
show "s e \<down>"
[PROOF STATE]
proof (prove)
using this:
s (f \<triangleright> (e_length e - 1)) \<down>

goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
using f(2) init_def
[PROOF STATE]
proof (prove)
using this:
s (f \<triangleright> (e_length e - 1)) \<down>
prefix f (e_length e - 1) = Partial_Recursive.list_decode e
?f \<triangleright> ?n \<equiv> Partial_Recursive.list_encode (prefix ?f ?n)

goal (1 subgoal):
 1. s e \<down>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s e \<down>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?e \<Longrightarrow> s ?e \<down>

goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?e \<Longrightarrow> s ?e \<down>
[PROOF STEP]
have "total1 t"
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> s ?e \<down>

goal (1 subgoal):
 1. total1 t
[PROOF STEP]
using t_def
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> s ?e \<down>
t = (\<lambda>e. if e = 0 then Some 0 else s e)

goal (1 subgoal):
 1. total1 t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
total1 t

goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
have "t \<in> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
learn_cons \<psi> U s
[PROOF STEP]
have "s \<in> \
"
[PROOF STATE]
proof (prove)
using this:
learn_cons \<psi> U s

goal (1 subgoal):
 1. s \<in> \

[PROOF STEP]
using learn_consE
[PROOF STATE]
proof (prove)
using this:
learn_cons \<psi> U s
learn_cons ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
\<lbrakk>learn_cons ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> \<exists>i n\<^sub>0. ?\<psi> i = ?f \<and> (\<forall>n\<ge>n\<^sub>0. ?s (?f \<triangleright> n) \<down>= i)
\<lbrakk>learn_cons ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> \<forall>k\<le>?n. ?\<psi> (the (?s (?f \<triangleright> ?n))) k = ?f k

goal (1 subgoal):
 1. s \<in> \

[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in> \

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> \

[PROOF STEP]
obtain rs where rs: "recfn 1 rs" "eval rs [x] = s x" for x
[PROOF STATE]
proof (prove)
using this:
s \<in> \

goal (1 subgoal):
 1. (\<And>rs. \<lbrakk>recfn 1 rs; \<And>x. eval rs [x] = s x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 rs
eval rs [?x] = s ?x

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
define rt where "rt = Cn 1 (r_lifz Z rs) [Id 1 0, Id 1 0]"
[PROOF STATE]
proof (state)
this:
rt = Cn 1 (r_lifz Z rs) [recf.Id 1 0, recf.Id 1 0]

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rt = Cn 1 (r_lifz Z rs) [recf.Id 1 0, recf.Id 1 0]
[PROOF STEP]
have "recfn 1 rt"
[PROOF STATE]
proof (prove)
using this:
rt = Cn 1 (r_lifz Z rs) [recf.Id 1 0, recf.Id 1 0]

goal (1 subgoal):
 1. recfn 1 rt
[PROOF STEP]
using rs
[PROOF STATE]
proof (prove)
using this:
rt = Cn 1 (r_lifz Z rs) [recf.Id 1 0, recf.Id 1 0]
recfn 1 rs
eval rs [?x] = s ?x

goal (1 subgoal):
 1. recfn 1 rt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 rt

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
recfn 1 rt

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
have "eval rt [x] = t x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval rt [x] = t x
[PROOF STEP]
using rs rt_def t_def
[PROOF STATE]
proof (prove)
using this:
recfn 1 rs
eval rs [?x] = s ?x
rt = Cn 1 (r_lifz Z rs) [recf.Id 1 0, recf.Id 1 0]
t = (\<lambda>e. if e = 0 then Some 0 else s e)

goal (1 subgoal):
 1. eval rt [x] = t x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval rt [?x] = t ?x

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
recfn 1 rt
eval rt [?x] = t ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
recfn 1 rt
eval rt [?x] = t ?x

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> \

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<in> \

goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
have "s (f \<triangleright> n) = t (f \<triangleright> n)" if "f \<in> U" for f n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s (f \<triangleright> n) = t (f \<triangleright> n)
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s (f \<triangleright> n) = (if f \<triangleright> n = 0 then Some 0 else s (f \<triangleright> n))
[PROOF STEP]
by (simp add: init_neq_zero)
[PROOF STATE]
proof (state)
this:
?f \<in> U \<Longrightarrow> s (?f \<triangleright> ?n) = t (?f \<triangleright> ?n)

goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?f \<in> U \<Longrightarrow> s (?f \<triangleright> ?n) = t (?f \<triangleright> ?n)
[PROOF STEP]
have "learn_cons \<psi> U t"
[PROOF STATE]
proof (prove)
using this:
?f \<in> U \<Longrightarrow> s (?f \<triangleright> ?n) = t (?f \<triangleright> ?n)

goal (1 subgoal):
 1. learn_cons \<psi> U t
[PROOF STEP]
using \<open>t \<in> \
\<close> assms(2) learn_consE[of \<psi> U s] learn_consI[of \<psi> U t]
[PROOF STATE]
proof (prove)
using this:
?f \<in> U \<Longrightarrow> s (?f \<triangleright> ?n) = t (?f \<triangleright> ?n)
t \<in> \

learn_cons \<psi> U s
learn_cons \<psi> U s \<Longrightarrow> environment \<psi> U s
\<lbrakk>learn_cons \<psi> U s; ?f \<in> U\<rbrakk> \<Longrightarrow> \<exists>i n\<^sub>0. \<psi> i = ?f \<and> (\<forall>n\<ge>n\<^sub>0. s (?f \<triangleright> n) \<down>= i)
\<lbrakk>learn_cons \<psi> U s; ?f \<in> U\<rbrakk> \<Longrightarrow> \<forall>k\<le>?n. \<psi> (the (s (?f \<triangleright> ?n))) k = ?f k
\<lbrakk>environment \<psi> U t; \<And>f. f \<in> U \<Longrightarrow> \<exists>i. \<psi> i = f \<and> (\<exists>n\<^sub>0. \<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= i); \<And>f n. f \<in> U \<Longrightarrow> \<forall>k\<le>n. \<psi> (the (t (f \<triangleright> n))) k = f k\<rbrakk> \<Longrightarrow> learn_cons \<psi> U t

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

goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
with \<open>total1 t\<close>
[PROOF STATE]
proof (chain)
picking this:
total1 t
learn_cons \<psi> U t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
total1 t
learn_cons \<psi> U t

goal (1 subgoal):
 1. \<exists>t. total1 t \<and> learn_cons \<psi> U t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t. total1 t \<and> learn_cons \<psi> U t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_s_recfn [simp]: "recfn 1 r_s"
  and r_s_total [simp]: "\<And>x. eval r_s [x] \<down>"
  and eval_r_s: "s = (\<lambda>x. eval r_s [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 r_s &&& (\<And>x. eval r_s [x] \<down>) &&& s = (\<lambda>x. eval r_s [x])
[PROOF STEP]
using r_s_def R1_SOME[OF s_in_R1, of r_s]
[PROOF STATE]
proof (prove)
using this:
r_s \<equiv> SOME r_s. recfn 1 r_s \<and> Partial_Recursive.total r_s \<and> s = (\<lambda>x. eval r_s [x])
r_s = (SOME r'. recfn 1 r' \<and> Partial_Recursive.total r' \<and> s = (\<lambda>x. eval r' [x])) \<Longrightarrow> recfn 1 r_s
r_s = (SOME r'. recfn 1 r' \<and> Partial_Recursive.total r' \<and> s = (\<lambda>x. eval r' [x])) \<Longrightarrow> eval r_s [?x] \<down>
r_s = (SOME r'. recfn 1 r' \<and> Partial_Recursive.total r' \<and> s = (\<lambda>x. eval r' [x])) \<Longrightarrow> s ?x = eval r_s [?x]
r_s = (SOME r'. recfn 1 r' \<and> Partial_Recursive.total r' \<and> s = (\<lambda>x. eval r' [x])) \<Longrightarrow> s = (\<lambda>x. eval r_s [x])

goal (1 subgoal):
 1. recfn 1 r_s &&& (\<And>x. eval r_s [x] \<down>) &&& s = (\<lambda>x. eval r_s [x])
[PROOF STEP]
by simp_all


[STATEMENT]
lemma r_prefixes_aux_recfn: "recfn 3 r_prefixes_aux"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 3 r_prefixes_aux
[PROOF STEP]
unfolding r_prefixes_aux_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 3 (Cn 3 r_ifeq [Cn 3 r_s [Cn 3 r_snoc [recf.Id 3 1, r_constn 2 0]], Cn 3 r_s [recf.Id 3 1], Cn 3 r_snoc [recf.Id 3 1, r_constn 2 1], Cn 3 r_snoc [recf.Id 3 1, r_constn 2 0]])
[PROOF STEP]
by simp


[STATEMENT]
lemma r_prefixes_aux:
  "eval r_prefixes_aux [j, v, i] \<down>=
    e_snoc v (if eval r_s [e_snoc v 0] = eval r_s [v] then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_prefixes_aux [j, v, i] \<down>= e_snoc v (if eval r_s [e_snoc v 0] = eval r_s [v] then 1 else 0)
[PROOF STEP]
unfolding r_prefixes_aux_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 3 r_ifeq [Cn 3 r_s [Cn 3 r_snoc [recf.Id 3 1, r_constn 2 0]], Cn 3 r_s [recf.Id 3 1], Cn 3 r_snoc [recf.Id 3 1, r_constn 2 1], Cn 3 r_snoc [recf.Id 3 1, r_constn 2 0]]) [j, v, i] \<down>= e_snoc v (if eval r_s [e_snoc v 0] = eval r_s [v] then 1 else 0)
[PROOF STEP]
by auto