[STATEMENT]
lemma r_inconsist: "eval r_inconsist [i, e] = inconsist i e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
define f where "f = Cn 2 r_length [Id 2 1]"
[PROOF STATE]
proof (state)
this:
f = Cn 2 r_length [recf.Id 2 1]

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
define len where "len = Cn 4 r_length [Id 4 3]"
[PROOF STATE]
proof (state)
this:
len = Cn 4 r_length [recf.Id 4 3]

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
define nth where "nth = Cn 4 r_nth [Id 4 3, Id 4 0]"
[PROOF STATE]
proof (state)
this:
nth = Cn 4 r_nth [recf.Id 4 3, recf.Id 4 0]

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
define ph where "ph = Cn 4 r_phi [Id 4 2, Id 4 0]"
[PROOF STATE]
proof (state)
this:
ph = Cn 4 r_phi [recf.Id 4 2, recf.Id 4 0]

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
define g where
    "g = Cn 4 r_ifless [Id 4 1, len, Id 4 1, Cn 4 r_ifeq [ph, nth, Id 4 1, Id 4 0]]"
[PROOF STATE]
proof (state)
this:
g = Cn 4 r_ifless [recf.Id 4 1, len, recf.Id 4 1, Cn 4 r_ifeq [ph, nth, recf.Id 4 1, recf.Id 4 0]]

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have "recfn 2 f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 f
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (Cn 2 r_length [recf.Id 2 1])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 2 f

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have f: "eval f [i, e] \<down>= e_length e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval f [i, e] \<down>= e_length e
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 r_length [recf.Id 2 1]) [i, e] \<down>= e_length e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval f [i, e] \<down>= e_length e

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have "recfn 4 len"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 len
[PROOF STEP]
unfolding len_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 (Cn 4 r_length [recf.Id 4 3])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 4 len

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have len: "eval len [j, v, i, e] \<down>= e_length e" for j v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval len [j, v, i, e] \<down>= e_length e
[PROOF STEP]
unfolding len_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_length [recf.Id 4 3]) [j, v, i, e] \<down>= e_length e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval len [?j, ?v, i, e] \<down>= e_length e

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have "recfn 4 nth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 nth
[PROOF STEP]
unfolding nth_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 (Cn 4 r_nth [recf.Id 4 3, recf.Id 4 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 4 nth

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have nth: "eval nth [j, v, i, e] \<down>= e_nth e j" for j v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval nth [j, v, i, e] \<down>= e_nth e j
[PROOF STEP]
unfolding nth_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_nth [recf.Id 4 3, recf.Id 4 0]) [j, v, i, e] \<down>= e_nth e j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval nth [?j, ?v, i, e] \<down>= e_nth e ?j

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have "recfn 4 ph"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 ph
[PROOF STEP]
unfolding ph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 (Cn 4 r_phi [recf.Id 4 2, recf.Id 4 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 4 ph

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have ph: "eval ph [j, v, i, e] = \<phi> i j" for j v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval ph [j, v, i, e] = \<phi> i j
[PROOF STEP]
unfolding ph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_phi [recf.Id 4 2, recf.Id 4 0]) [j, v, i, e] = \<phi> i j
[PROOF STEP]
using phi_def
[PROOF STATE]
proof (prove)
using this:
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]

goal (1 subgoal):
 1. eval (Cn 4 r_phi [recf.Id 4 2, recf.Id 4 0]) [j, v, i, e] = \<phi> i j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval ph [?j, ?v, i, e] = \<phi> i ?j

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have "recfn 4 g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 g
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 4 (Cn 4 r_ifless [recf.Id 4 1, len, recf.Id 4 1, Cn 4 r_ifeq [ph, nth, recf.Id 4 1, recf.Id 4 0]])
[PROOF STEP]
using \<open>recfn 4 nth\<close> \<open>recfn 4 ph\<close> \<open>recfn 4 len\<close>
[PROOF STATE]
proof (prove)
using this:
recfn 4 nth
recfn 4 ph
recfn 4 len

goal (1 subgoal):
 1. recfn 4 (Cn 4 r_ifless [recf.Id 4 1, len, recf.Id 4 1, Cn 4 r_ifeq [ph, nth, recf.Id 4 1, recf.Id 4 0]])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 4 g

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have g_diverg: "eval g [j, v, i, e] \<up>" if "eval ph [j, v, i, e] \<up>" for j v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval g [j, v, i, e] \<up>
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_ifless [recf.Id 4 1, len, recf.Id 4 1, Cn 4 r_ifeq [ph, nth, recf.Id 4 1, recf.Id 4 0]]) [j, v, i, e] \<up>
[PROOF STEP]
using that \<open>recfn 4 nth\<close> \<open>recfn 4 ph\<close> \<open>recfn 4 len\<close>
[PROOF STATE]
proof (prove)
using this:
eval ph [j, v, i, e] \<up>
recfn 4 nth
recfn 4 ph
recfn 4 len

goal (1 subgoal):
 1. eval (Cn 4 r_ifless [recf.Id 4 1, len, recf.Id 4 1, Cn 4 r_ifeq [ph, nth, recf.Id 4 1, recf.Id 4 0]]) [j, v, i, e] \<up>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval ph [?j, ?v, i, e] \<up> \<Longrightarrow> eval g [?j, ?v, i, e] \<up>

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have g_converg: "eval g [j, v, i, e] \<down>=
      (if v < e_length e then v else if \<phi> i j \<down>= e_nth e j then v else j)"
      if "eval ph [j, v, i, e] \<down>" for j v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval g [j, v, i, e] \<down>= (if v < e_length e then v else if \<phi> i j \<down>= e_nth e j then v else j)
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_ifless [recf.Id 4 1, len, recf.Id 4 1, Cn 4 r_ifeq [ph, nth, recf.Id 4 1, recf.Id 4 0]]) [j, v, i, e] \<down>= (if v < e_length e then v else if \<phi> i j \<down>= e_nth e j then v else j)
[PROOF STEP]
using that \<open>recfn 4 nth\<close> \<open>recfn 4 ph\<close> \<open>recfn 4 len\<close> len nth ph
[PROOF STATE]
proof (prove)
using this:
eval ph [j, v, i, e] \<down>
recfn 4 nth
recfn 4 ph
recfn 4 len
eval len [?j, ?v, i, e] \<down>= e_length e
eval nth [?j, ?v, i, e] \<down>= e_nth e ?j
eval ph [?j, ?v, i, e] = \<phi> i ?j

goal (1 subgoal):
 1. eval (Cn 4 r_ifless [recf.Id 4 1, len, recf.Id 4 1, Cn 4 r_ifeq [ph, nth, recf.Id 4 1, recf.Id 4 0]]) [j, v, i, e] \<down>= (if v < e_length e then v else if \<phi> i j \<down>= e_nth e j then v else j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval ph [?j, ?v, i, e] \<down> \<Longrightarrow> eval g [?j, ?v, i, e] \<down>= (if ?v < e_length e then ?v else if \<phi> i ?j \<down>= e_nth e ?j then ?v else ?j)

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
define h where "h \<equiv> Pr 2 f g"
[PROOF STATE]
proof (state)
this:
h \<equiv> Pr 2 f g

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h \<equiv> Pr 2 f g
[PROOF STEP]
have "recfn 3 h"
[PROOF STATE]
proof (prove)
using this:
h \<equiv> Pr 2 f g

goal (1 subgoal):
 1. recfn 3 h
[PROOF STEP]
by (simp add: \<open>recfn 2 f\<close> \<open>recfn 4 g\<close>)
[PROOF STATE]
proof (state)
this:
recfn 3 h

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
let ?invariant = "\<lambda>j i e.
    (if \<exists>x<j. \<phi> i x \<up> then None
     else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
          then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
          else Some (e_length e))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have "eval h [j, i, e] = ?invariant j i e" if "j \<le> e_length e" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
j \<le> e_length e

goal (1 subgoal):
 1. eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
proof (induction j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> e_length e \<Longrightarrow> eval h [0, i, e] = (if \<exists>x<0. \<phi> i x \<up> then None else if \<exists>x<0. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < 0 \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. \<And>j. \<lbrakk>j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)); Suc j \<le> e_length e\<rbrakk> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 \<le> e_length e

goal (2 subgoals):
 1. 0 \<le> e_length e \<Longrightarrow> eval h [0, i, e] = (if \<exists>x<0. \<phi> i x \<up> then None else if \<exists>x<0. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < 0 \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. \<And>j. \<lbrakk>j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)); Suc j \<le> e_length e\<rbrakk> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> e_length e
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> e_length e

goal (1 subgoal):
 1. eval h [0, i, e] = (if \<exists>x<0. \<phi> i x \<up> then None else if \<exists>x<0. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < 0 \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> e_length e

goal (1 subgoal):
 1. eval (Pr 2 f g) [0, i, e] = (if \<exists>x<0. \<phi> i x \<up> then None else if \<exists>x<0. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < 0 \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
using \<open>recfn 2 f\<close> f \<open>recfn 4 g\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> e_length e
recfn 2 f
eval f [i, e] \<down>= e_length e
recfn 4 g

goal (1 subgoal):
 1. eval (Pr 2 f g) [0, i, e] = (if \<exists>x<0. \<phi> i x \<up> then None else if \<exists>x<0. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < 0 \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval h [0, i, e] = (if \<exists>x<0. \<phi> i x \<up> then None else if \<exists>x<0. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < 0 \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)); Suc j \<le> e_length e\<rbrakk> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)); Suc j \<le> e_length e\<rbrakk> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
Suc j \<le> e_length e

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)); Suc j \<le> e_length e\<rbrakk> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
Suc j \<le> e_length e
[PROOF STEP]
have j_less: "j < e_length e"
[PROOF STATE]
proof (prove)
using this:
j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
Suc j \<le> e_length e

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)); Suc j \<le> e_length e\<rbrakk> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < e_length e
[PROOF STEP]
have j_le: "j \<le> e_length e"
[PROOF STATE]
proof (prove)
using this:
j < e_length e

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)); Suc j \<le> e_length e\<rbrakk> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
proof (cases "eval h [j, i, e] \<up>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval h [j, i, e] \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
eval h [j, i, e] \<up>

goal (2 subgoals):
 1. eval h [j, i, e] \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval h [j, i, e] \<up>
[PROOF STEP]
have "\<exists>x<j. \<phi> i x \<up>"
[PROOF STATE]
proof (prove)
using this:
eval h [j, i, e] \<up>

goal (1 subgoal):
 1. \<exists>x<j. \<phi> i x \<up>
[PROOF STEP]
using j_le Suc.IH
[PROOF STATE]
proof (prove)
using this:
eval h [j, i, e] \<up>
j \<le> e_length e
j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal (1 subgoal):
 1. \<exists>x<j. \<phi> i x \<up>
[PROOF STEP]
by (metis option.simps(3))
[PROOF STATE]
proof (state)
this:
\<exists>x<j. \<phi> i x \<up>

goal (2 subgoals):
 1. eval h [j, i, e] \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<j. \<phi> i x \<up>
[PROOF STEP]
have "\<exists>x<Suc j. \<phi> i x \<up>"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<j. \<phi> i x \<up>

goal (1 subgoal):
 1. \<exists>x<Suc j. \<phi> i x \<up>
[PROOF STEP]
using less_SucI
[PROOF STATE]
proof (prove)
using this:
\<exists>x<j. \<phi> i x \<up>
?m < ?n \<Longrightarrow> ?m < Suc ?n

goal (1 subgoal):
 1. \<exists>x<Suc j. \<phi> i x \<up>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x<Suc j. \<phi> i x \<up>

goal (2 subgoals):
 1. eval h [j, i, e] \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x<Suc j. \<phi> i x \<up>

goal (2 subgoals):
 1. eval h [j, i, e] \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
have h: "eval h [Suc j, i, e] \<up>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval h [Suc j, i, e] \<up>
[PROOF STEP]
using True h_def \<open>recfn 3 h\<close>
[PROOF STATE]
proof (prove)
using this:
eval h [j, i, e] \<up>
h \<equiv> Pr 2 f g
recfn 3 h

goal (1 subgoal):
 1. eval h [Suc j, i, e] \<up>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval h [Suc j, i, e] \<up>

goal (2 subgoals):
 1. eval h [j, i, e] \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<Suc j. \<phi> i x \<up>
eval h [Suc j, i, e] \<up>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x<Suc j. \<phi> i x \<up>
eval h [Suc j, i, e] \<up>

goal (1 subgoal):
 1. eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal (1 subgoal):
 1. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
eval h [j, i, e] \<down>

goal (1 subgoal):
 1. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
with Suc.IH j_le
[PROOF STATE]
proof (chain)
picking this:
j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
j \<le> e_length e
eval h [j, i, e] \<down>
[PROOF STEP]
have h_j: "eval h [j, i, e] =
        (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
         then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
         else Some (e_length e))"
[PROOF STATE]
proof (prove)
using this:
j \<le> e_length e \<Longrightarrow> eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<up> then None else if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
j \<le> e_length e
eval h [j, i, e] \<down>

goal (1 subgoal):
 1. eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal (1 subgoal):
 1. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
have the_h_j: "the (eval h [j, i, e]) =
        (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
         then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x
         else e_length e)"
         (is "_ = ?v")
[PROOF STATE]
proof (prove)
using this:
eval h [j, i, e] = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal (1 subgoal):
 1. the (eval h [j, i, e]) = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (eval h [j, i, e]) = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (1 subgoal):
 1. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
have h_Suc: "eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]
[PROOF STEP]
using False h_def \<open>recfn 4 g\<close> \<open>recfn 2 f\<close>
[PROOF STATE]
proof (prove)
using this:
eval h [j, i, e] \<down>
h \<equiv> Pr 2 f g
recfn 4 g
recfn 2 f

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

goal (1 subgoal):
 1. eval h [j, i, e] \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
proof (cases "\<phi> i j \<up>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> i j \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<phi> i j \<up>

goal (2 subgoals):
 1. \<phi> i j \<up> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
 2. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
with ph g_diverg h_Suc
[PROOF STATE]
proof (chain)
picking this:
eval ph [?j, ?v, i, e] = \<phi> i ?j
eval ph [?j, ?v, i, e] \<up> \<Longrightarrow> eval g [?j, ?v, i, e] \<up>
eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]
\<phi> i j \<up>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval ph [?j, ?v, i, e] = \<phi> i ?j
eval ph [?j, ?v, i, e] \<up> \<Longrightarrow> eval g [?j, ?v, i, e] \<up>
eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]
\<phi> i j \<up>

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

goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<phi> i j \<down>

goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
with h_Suc
[PROOF STATE]
proof (chain)
picking this:
eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]
\<phi> i j \<down>
[PROOF STEP]
have "eval h [Suc j, i, e] \<down>=
          (if ?v < e_length e then ?v
           else if \<phi> i j \<down>= e_nth e j then ?v else j)"
          (is "_ \<down>= ?lhs")
[PROOF STATE]
proof (prove)
using this:
eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]
\<phi> i j \<down>

goal (1 subgoal):
 1. eval h [Suc j, i, e] \<down>= (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j)
[PROOF STEP]
using g_converg ph the_h_j
[PROOF STATE]
proof (prove)
using this:
eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]
\<phi> i j \<down>
eval ph [?j, ?v, i, e] \<down> \<Longrightarrow> eval g [?j, ?v, i, e] \<down>= (if ?v < e_length e then ?v else if \<phi> i ?j \<down>= e_nth e ?j then ?v else ?j)
eval ph [?j, ?v, i, e] = \<phi> i ?j
the (eval h [j, i, e]) = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (1 subgoal):
 1. eval h [Suc j, i, e] \<down>= (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval h [Suc j, i, e] \<down>= (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j)

goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval h [Suc j, i, e] \<down>= (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j)

goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
have "?invariant (Suc j) i e \<down>=
          (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x
           then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x
           else e_length e)"
          (is "_ \<down>= ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<phi> i j \<down>
[PROOF STEP]
have "\<phi> i j \<down>"
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<down>

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

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

goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
have "\<not> (\<exists>x<j. \<phi> i x \<up>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<exists>x<j. \<phi> i x \<up>)
[PROOF STEP]
by (metis (no_types, lifting) Suc.IH h_j j_le option.simps(3))
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>x<j. \<phi> i x \<up>)

goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> i j \<down>
\<not> (\<exists>x<j. \<phi> i x \<up>)
[PROOF STEP]
have "\<not> (\<exists>x<Suc j. \<phi> i x \<up>)"
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<down>
\<not> (\<exists>x<j. \<phi> i x \<up>)

goal (1 subgoal):
 1. \<not> (\<exists>x<Suc j. \<phi> i x \<up>)
[PROOF STEP]
using less_Suc_eq
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<down>
\<not> (\<exists>x<j. \<phi> i x \<up>)
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)

goal (1 subgoal):
 1. \<not> (\<exists>x<Suc j. \<phi> i x \<up>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>x<Suc j. \<phi> i x \<up>)

goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>x<Suc j. \<phi> i x \<up>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<Suc j. \<phi> i x \<up>)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
have "?lhs = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
proof (cases "?v < e_length e")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e

goal (2 subgoals):
 1. (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
[PROOF STEP]
have
            ex_j: "\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x" and
            v_eq: "?v = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)"
[PROOF STATE]
proof (prove)
using this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e

goal (1 subgoal):
 1. \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x &&& (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
by presburger+
[PROOF STATE]
proof (state)
this:
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)

goal (2 subgoals):
 1. (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
have "?lhs = ?v"
[PROOF STATE]
proof (prove)
using this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (2 subgoals):
 1. (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
from ex_j
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
have "\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x

goal (1 subgoal):
 1. \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
using less_SucI
[PROOF STATE]
proof (prove)
using this:
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
?m < ?n \<Longrightarrow> ?m < Suc ?n

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

goal (2 subgoals):
 1. (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x
[PROOF STEP]
have "?rhs = (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x

goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)

goal (2 subgoals):
 1. (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
with True v_eq ex_j
[PROOF STATE]
proof (chain)
picking this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
using least_bounded_Suc[of j "\<lambda>x. \<phi> i x \<down>\<noteq> e_nth e x"]
[PROOF STATE]
proof (prove)
using this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x \<Longrightarrow> (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) = (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

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

goal (1 subgoal):
 1. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
[PROOF STEP]
have not_ex: "\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)"
[PROOF STATE]
proof (prove)
using this:
\<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e

goal (1 subgoal):
 1. \<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
using Least_le[of "\<lambda>x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x"] j_le
[PROOF STATE]
proof (prove)
using this:
\<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
?k < j \<and> \<phi> i ?k \<down>\<noteq> e_nth e ?k \<Longrightarrow> (LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x) \<le> ?k
j \<le> e_length e

goal (1 subgoal):
 1. \<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
by (smt leD le_less_linear le_trans)
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
have "?v = e_length e"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e

goal (1 subgoal):
 1. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e
[PROOF STEP]
have lhs: "?lhs = (if \<phi> i j \<down>= e_nth e j then e_length e else j)"
[PROOF STATE]
proof (prove)
using this:
\<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e
(if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<phi> i j \<down>= e_nth e j then e_length e else j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<phi> i j \<down>= e_nth e j then e_length e else j)

goal (1 subgoal):
 1. \<not> (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
proof (cases "\<phi> i j \<down>= e_nth e j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> i j \<down>= e_nth e j \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<phi> i j \<down>= e_nth e j

goal (2 subgoals):
 1. \<phi> i j \<down>= e_nth e j \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> i j \<down>= e_nth e j
[PROOF STEP]
have "\<not> (\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x)"
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<down>= e_nth e j

goal (1 subgoal):
 1. \<not> (\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
using less_SucE not_ex
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<down>= e_nth e j
\<lbrakk>?m < Suc ?n; ?m < ?n \<Longrightarrow> ?P; ?m = ?n \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. \<not> (\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x)

goal (2 subgoals):
 1. \<phi> i j \<down>= e_nth e j \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x)
[PROOF STEP]
have "?rhs = e_length e"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x)

goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e

goal (2 subgoals):
 1. \<phi> i j \<down>= e_nth e j \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e

goal (2 subgoals):
 1. \<phi> i j \<down>= e_nth e j \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
\<phi> i j \<down>= e_nth e j
[PROOF STEP]
have "?lhs = e_length e"
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<down>= e_nth e j

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = e_length e
[PROOF STEP]
using lhs
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<down>= e_nth e j
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<phi> i j \<down>= e_nth e j then e_length e else j)

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = e_length e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = e_length e

goal (2 subgoals):
 1. \<phi> i j \<down>= e_nth e j \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
 2. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = e_length e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = e_length e
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = e_length e

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<phi> i j \<noteq> Some (e_nth e j)

goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> i j \<noteq> Some (e_nth e j)
[PROOF STEP]
have "\<phi> i j \<down>\<noteq> e_nth e j"
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<noteq> Some (e_nth e j)

goal (1 subgoal):
 1. \<phi> i j \<down>\<noteq> e_nth e j
[PROOF STEP]
using \<open>\<phi> i j \<down>\<close>
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<noteq> Some (e_nth e j)
\<phi> i j \<down>

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

goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
with not_ex
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)
\<phi> i j \<down>\<noteq> e_nth e j
[PROOF STEP]
have "(LEAST x. x<Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) = j"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)
\<phi> i j \<down>\<noteq> e_nth e j

goal (1 subgoal):
 1. (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) = j
[PROOF STEP]
using LeastI[of "\<lambda>x. x<Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x" j] less_Suc_eq
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x)
\<phi> i j \<down>\<noteq> e_nth e j
j < Suc j \<and> \<phi> i j \<down>\<noteq> e_nth e j \<Longrightarrow> (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) < Suc j \<and> \<phi> i (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) \<down>\<noteq> e_nth e (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x)
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)

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

goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) = j
[PROOF STEP]
have "?rhs = j"
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) = j

goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = j
[PROOF STEP]
using \<open>\<phi> i j \<down>\<noteq> e_nth e j\<close>
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) = j
\<phi> i j \<down>\<noteq> e_nth e j

goal (1 subgoal):
 1. (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = j
[PROOF STEP]
by (meson lessI)
[PROOF STATE]
proof (state)
this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = j

goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = j

goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
from False lhs
[PROOF STATE]
proof (chain)
picking this:
\<phi> i j \<noteq> Some (e_nth e j)
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<phi> i j \<down>= e_nth e j then e_length e else j)
[PROOF STEP]
have "?lhs = j"
[PROOF STATE]
proof (prove)
using this:
\<phi> i j \<noteq> Some (e_nth e j)
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<phi> i j \<down>= e_nth e j then e_length e else j)

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = j

goal (1 subgoal):
 1. \<phi> i j \<noteq> Some (e_nth e j) \<Longrightarrow> (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = j
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) = j
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = j

goal (1 subgoal):
 1. (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (1 subgoal):
 1. \<phi> i j \<down> \<Longrightarrow> eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval h [Suc j, i, e] \<down>= (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j)
(if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval h [Suc j, i, e] \<down>= (if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j)
(if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e)) \<down>= (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
(if (if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e) < e_length e then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else if \<phi> i j \<down>= e_nth e j then if \<exists>x<j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e else j) = (if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)

goal (1 subgoal):
 1. eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval h [Suc j, i, e] = (if \<exists>x<Suc j. \<phi> i x \<up> then None else if \<exists>x<Suc j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < Suc j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?j \<le> e_length e \<Longrightarrow> eval h [?j, i, e] = (if \<exists>x<?j. \<phi> i x \<up> then None else if \<exists>x<?j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < ?j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j \<le> e_length e \<Longrightarrow> eval h [?j, i, e] = (if \<exists>x<?j. \<phi> i x \<up> then None else if \<exists>x<?j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < ?j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
have "eval h [e_length e, i, e] = ?invariant (e_length e) i e"
[PROOF STATE]
proof (prove)
using this:
?j \<le> e_length e \<Longrightarrow> eval h [?j, i, e] = (if \<exists>x<?j. \<phi> i x \<up> then None else if \<exists>x<?j. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < ?j \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

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

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval h [e_length e, i, e] = (if \<exists>x<e_length e. \<phi> i x \<up> then None else if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
[PROOF STEP]
have "eval h [e_length e, i, e] = inconsist i e"
[PROOF STATE]
proof (prove)
using this:
eval h [e_length e, i, e] = (if \<exists>x<e_length e. \<phi> i x \<up> then None else if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))

goal (1 subgoal):
 1. eval h [e_length e, i, e] = inconsist i e
[PROOF STEP]
using inconsist_def
[PROOF STATE]
proof (prove)
using this:
eval h [e_length e, i, e] = (if \<exists>x<e_length e. \<phi> i x \<up> then None else if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then Some (LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x) else Some (e_length e))
inconsist ?i ?e \<equiv> if \<exists>x<e_length ?e. \<phi> ?i x \<up> then None else if \<exists>x<e_length ?e. \<phi> ?i x \<down>\<noteq> e_nth ?e x then Some (LEAST x. x < e_length ?e \<and> \<phi> ?i x \<down>\<noteq> e_nth ?e x) else Some (e_length ?e)

goal (1 subgoal):
 1. eval h [e_length e, i, e] = inconsist i e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval h [e_length e, i, e] = inconsist i e

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval h [e_length e, i, e] = inconsist i e

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
have "eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [Id 2 1], Id 2 0, Id 2 1]) [i, e] =
      eval h [e_length e, i, e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, e] = eval h [e_length e, i, e]
[PROOF STEP]
using \<open>recfn 4 g\<close> \<open>recfn 2 f\<close> h_def
[PROOF STATE]
proof (prove)
using this:
recfn 4 g
recfn 2 f
h \<equiv> Pr 2 f g

goal (1 subgoal):
 1. eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, e] = eval h [e_length e, i, e]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, e] = eval h [e_length e, i, e]

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval h [e_length e, i, e] = inconsist i e
eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, e] = eval h [e_length e, i, e]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval h [e_length e, i, e] = inconsist i e
eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, e] = eval h [e_length e, i, e]

goal (1 subgoal):
 1. eval r_inconsist [i, e] = inconsist i e
[PROOF STEP]
unfolding r_inconsist_def
[PROOF STATE]
proof (prove)
using this:
eval h [e_length e, i, e] = inconsist i e
eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, e] = eval h [e_length e, i, e]

goal (1 subgoal):
 1. eval (let f = Cn 2 r_length [recf.Id 2 1]; g = Cn 4 r_ifless [recf.Id 4 1, Cn 4 r_length [recf.Id 4 3], recf.Id 4 1, Cn 4 r_ifeq [Cn 4 r_phi [recf.Id 4 2, recf.Id 4 0], Cn 4 r_nth [recf.Id 4 3, recf.Id 4 0], recf.Id 4 1, recf.Id 4 0]] in Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1]) [i, e] = inconsist i e
[PROOF STEP]
by (simp add: f_def g_def len_def nth_def ph_def)
[PROOF STATE]
proof (state)
this:
eval r_inconsist [i, e] = inconsist i e

goal:
No subgoals!
[PROOF STEP]
qed