[STATEMENT]
lemma rmge2_init:
  "rmge2 (f \<triangleright> n) =
   (if \<forall>i<Suc n. the (f i) < 2 then Some 0
    else Some (the (f (GREATEST i. i < Suc n \<and> the (f i) \<ge> 2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
let ?xs = "prefix f n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "f \<triangleright> n = list_encode ?xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
[PROOF STEP]
by (simp add: init_def)
[PROOF STATE]
proof (state)
this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length ?xs. ?xs ! i < 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "(GREATEST i. i < Suc n \<and> the (f i) \<ge> 2) =
      (GREATEST i. i < length ?xs \<and> ?xs ! i \<ge> 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
[PROOF STEP]
using length_prefix[of f n] prefix_nth[of _ n f]
[PROOF STATE]
proof (prove)
using this:
length (prefix f n) = Suc n
?k < Suc n \<Longrightarrow> prefix f n ! ?k = the (f ?k)

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

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "(GREATEST i. i < Suc n \<and> the (f i) \<ge> 2) < Suc n"
      if "\<not> (\<forall>i<Suc n. the (f i) < 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n
[PROOF STEP]
using that GreatestI_ex_nat[of "\<lambda>i. i<Suc n \<and> the (f i) \<ge> 2" n]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i<Suc n. the (f i) < 2)
\<lbrakk>\<exists>k<Suc n. 2 \<le> the (f k); \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<rbrakk> \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n \<and> 2 \<le> the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))

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

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
\<not> (\<forall>i<Suc n. the (f i) < 2) \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
\<not> (\<forall>i<Suc n. the (f i) < 2) \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
using rmge2
[PROOF STATE]
proof (prove)
using this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
\<not> (\<forall>i<Suc n. the (f i) < 2) \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n
?xs = Partial_Recursive.list_decode ?e \<Longrightarrow> 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 (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (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) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))

goal:
No subgoals!
[PROOF STEP]
qed