[STATEMENT]
lemma inconsist_for_total:
  assumes "total1 (\<phi> i)"
  shows "inconsist i e \<down>=
    (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x
     then LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x
     else e_length e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsist i e \<down>= (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
unfolding inconsist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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)) \<down>= (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
using assms total1_def
[PROOF STATE]
proof (prove)
using this:
total1 (\<phi> i)
total1 ?f \<equiv> \<forall>x. ?f x \<down>

goal (1 subgoal):
 1. (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)) \<down>= (if \<exists>x<e_length e. \<phi> i x \<down>\<noteq> e_nth e x then LEAST x. x < e_length e \<and> \<phi> i x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
by (auto; blast)


[STATEMENT]
lemma inconsist_for_V01:
  assumes "f \<in> V\<^sub>0\<^sub>1" and "k = amalgamate (the (f 0)) (the (f 1))"
  shows "inconsist k e \<down>=
    (if \<exists>x<e_length e. \<phi> k x \<down>\<noteq> e_nth e x
     then LEAST x. x < e_length e \<and> \<phi> k x \<down>\<noteq> e_nth e x
     else e_length e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsist k e \<down>= (if \<exists>x<e_length e. \<phi> k x \<down>\<noteq> e_nth e x then LEAST x. x < e_length e \<and> \<phi> k x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inconsist k e \<down>= (if \<exists>x<e_length e. \<phi> k x \<down>\<noteq> e_nth e x then LEAST x. x < e_length e \<and> \<phi> k x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
have "\<phi> k \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> k \<in> \<R>
[PROOF STEP]
using amalgamation_V01_R1[OF assms(1)] assms(2) amalgamate
[PROOF STATE]
proof (prove)
using this:
amalgamation (the (f 0)) (the (f 1)) \<in> \<R>
k = amalgamate (the (f 0)) (the (f 1))
\<phi> (amalgamate ?i ?j) = amalgamation ?i ?j

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

goal (1 subgoal):
 1. inconsist k e \<down>= (if \<exists>x<e_length e. \<phi> k x \<down>\<noteq> e_nth e x then LEAST x. x < e_length e \<and> \<phi> k x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> k \<in> \<R>
[PROOF STEP]
have "total1 (\<phi> k)"
[PROOF STATE]
proof (prove)
using this:
\<phi> k \<in> \<R>

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

goal (1 subgoal):
 1. inconsist k e \<down>= (if \<exists>x<e_length e. \<phi> k x \<down>\<noteq> e_nth e x then LEAST x. x < e_length e \<and> \<phi> k x \<down>\<noteq> e_nth e x else e_length e)
[PROOF STEP]
with inconsist_for_total[of k]
[PROOF STATE]
proof (chain)
picking this:
total1 (\<phi> k) \<Longrightarrow> inconsist k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> k x \<down>\<noteq> e_nth ?e x else e_length ?e)
total1 (\<phi> k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
total1 (\<phi> k) \<Longrightarrow> inconsist k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> k x \<down>\<noteq> e_nth ?e x else e_length ?e)
total1 (\<phi> k)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_auxhyp_prim: "prim_recfn 1 r_auxhyp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prim_recfn 1 r_auxhyp
[PROOF STEP]
unfolding r_auxhyp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prim_recfn 1 (Cn 1 (r_smn 1 1) [r_const (encode r_prenum), recf.Id 1 0])
[PROOF STEP]
by simp


[STATEMENT]
lemma r_auxhyp: "\<phi> (the (eval r_auxhyp [e])) = prenum e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) = prenum e
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
let ?p = "encode r_prenum"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
let ?p = "encode r_prenum"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
have "eval r_auxhyp [e] = eval (r_smn 1 1) [?p, e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_auxhyp [e] = eval (r_smn 1 1) [encode r_prenum, e]
[PROOF STEP]
unfolding r_auxhyp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 1 (r_smn 1 1) [r_const (encode r_prenum), recf.Id 1 0]) [e] = eval (r_smn 1 1) [encode r_prenum, e]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_auxhyp [e] = eval (r_smn 1 1) [encode r_prenum, e]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_auxhyp [e] = eval (r_smn 1 1) [encode r_prenum, e]
[PROOF STEP]
have "eval r_auxhyp [e] \<down>= smn 1 ?p [e]"
[PROOF STATE]
proof (prove)
using this:
eval r_auxhyp [e] = eval (r_smn 1 1) [encode r_prenum, e]

goal (1 subgoal):
 1. eval r_auxhyp [e] \<down>= smn 1 (encode r_prenum) [e]
[PROOF STEP]
by (simp add: r_smn)
[PROOF STATE]
proof (state)
this:
eval r_auxhyp [e] \<down>= smn 1 (encode r_prenum) [e]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval r_auxhyp [e] \<down>= smn 1 (encode r_prenum) [e]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
have "... \<down>= encode (Cn 1 (r_universal (1 + length [e]))
      (r_constn (1 - 1) ?p #
       map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (smn 1 (encode r_prenum) [e]) \<down>= encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))
[PROOF STEP]
using smn[of 1 ?p "[e]"]
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> smn 1 (encode r_prenum) [e] = encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))

goal (1 subgoal):
 1. Some (smn 1 (encode r_prenum) [e]) \<down>= encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (smn 1 (encode r_prenum) [e]) \<down>= encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Some (smn 1 (encode r_prenum) [e]) \<down>= encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
have "... \<down>= encode (Cn 1 (r_universal (1 + 1))
      (r_constn 0 ?p # map (r_constn 0) [e] @ [Id 1 0]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))) \<down>= encode (Cn 1 (r_universal (1 + 1)) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))) \<down>= encode (Cn 1 (r_universal (1 + 1)) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Some (encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) (encode r_prenum) # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))) \<down>= encode (Cn 1 (r_universal (1 + 1)) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
have "... \<down>= encode (Cn 1 (r_universal 2)
      (r_constn 0 ?p # map (r_constn 0) [e] @ [Id 1 0]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (encode (Cn 1 (r_universal (1 + 1)) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))) \<down>= encode (Cn 1 (r_universal 2) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))
[PROOF STEP]
by (metis one_add_one)
[PROOF STATE]
proof (state)
this:
Some (encode (Cn 1 (r_universal (1 + 1)) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))) \<down>= encode (Cn 1 (r_universal 2) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Some (encode (Cn 1 (r_universal (1 + 1)) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))) \<down>= encode (Cn 1 (r_universal 2) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
have "... \<down>= encode (Cn 1 (r_universal 2) [r_constn 0 ?p, r_constn 0 e, Id 1 0])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (encode (Cn 1 (r_universal 2) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))) \<down>= encode (Cn 1 (r_universal 2) [r_constn 0 (encode r_prenum), r_constn 0 e, recf.Id 1 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (encode (Cn 1 (r_universal 2) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))) \<down>= encode (Cn 1 (r_universal 2) [r_constn 0 (encode r_prenum), r_constn 0 e, recf.Id 1 0])

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Some (encode (Cn 1 (r_universal 2) (r_constn 0 (encode r_prenum) # map (r_constn 0) [e] @ [recf.Id 1 0]))) \<down>= encode (Cn 1 (r_universal 2) [r_constn 0 (encode r_prenum), r_constn 0 e, recf.Id 1 0])

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
have "... \<down>= encode (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (encode (Cn 1 (r_universal 2) [r_constn 0 (encode r_prenum), r_constn 0 e, recf.Id 1 0])) \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])
[PROOF STEP]
using r_constn_def
[PROOF STATE]
proof (prove)
using this:
r_constn ?n ?c \<equiv> if ?n = 0 then r_const ?c else r_dummy ?n (r_const ?c)

goal (1 subgoal):
 1. Some (encode (Cn 1 (r_universal 2) [r_constn 0 (encode r_prenum), r_constn 0 e, recf.Id 1 0])) \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (encode (Cn 1 (r_universal 2) [r_constn 0 (encode r_prenum), r_constn 0 e, recf.Id 1 0])) \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval r_auxhyp [e] \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])
[PROOF STEP]
have "eval r_auxhyp [e] \<down>=
    encode (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0])"
[PROOF STATE]
proof (prove)
using this:
eval r_auxhyp [e] \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])

goal (1 subgoal):
 1. eval r_auxhyp [e] \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eval r_auxhyp [e] \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval r_auxhyp [e] \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
have "\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [the (eval r_auxhyp [e]), x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = eval r_phi [the (eval r_auxhyp [e]), x]
[PROOF STEP]
by (simp add: phi_def)
[PROOF STATE]
proof (state)
this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [the (eval r_auxhyp [e]), x]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval r_auxhyp [e] \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])
\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [the (eval r_auxhyp [e]), x]
[PROOF STEP]
have "\<phi> (the (eval r_auxhyp [e])) x =
      eval r_phi [encode (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0]), x]"
      (is "_ = eval r_phi [encode ?f, x]")
[PROOF STATE]
proof (prove)
using this:
eval r_auxhyp [e] \<down>= encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0])
\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [the (eval r_auxhyp [e]), x]

goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = eval r_phi [encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]), x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]), x]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]), x]
[PROOF STEP]
have "\<phi> (the (eval r_auxhyp [e])) x =
      eval (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0]) [x]"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]), x]

goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = eval (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]) [x]
[PROOF STEP]
using r_phi_def r_universal[of ?f 1 "[x]"]
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_phi [encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]), x]
r_phi \<equiv> r_universal 1
\<lbrakk>recfn 1 (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]); length [x] = 1\<rbrakk> \<Longrightarrow> eval (r_universal 1) [encode (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]), x] = eval (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]) [x]

goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = eval (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]) [x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (eval r_auxhyp [e])) x = eval (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]) [x]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (eval r_auxhyp [e])) x = eval (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]) [x]
[PROOF STEP]
have "\<phi> (the (eval r_auxhyp [e])) x = eval (r_universal 2) [?p, e, x]"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (eval r_auxhyp [e])) x = eval (Cn 1 (r_universal 2) [r_const (encode r_prenum), r_const e, recf.Id 1 0]) [x]

goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = eval (r_universal 2) [encode r_prenum, e, x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (eval r_auxhyp [e])) x = eval (r_universal 2) [encode r_prenum, e, x]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (eval r_auxhyp [e])) x = eval (r_universal 2) [encode r_prenum, e, x]
[PROOF STEP]
have "\<phi> (the (eval r_auxhyp [e])) x = eval r_prenum [e, x]"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (eval r_auxhyp [e])) x = eval (r_universal 2) [encode r_prenum, e, x]

goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = eval r_prenum [e, x]
[PROOF STEP]
using r_universal
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (eval r_auxhyp [e])) x = eval (r_universal 2) [encode r_prenum, e, x]
\<lbrakk>recfn ?n ?f; length ?xs = ?n\<rbrakk> \<Longrightarrow> eval (r_universal ?n) (encode ?f # ?xs) = eval ?f ?xs

goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = eval r_prenum [e, x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_prenum [e, x]

goal (1 subgoal):
 1. \<And>x. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_prenum [e, x]
[PROOF STEP]
show "\<phi> (the (eval r_auxhyp [e])) x = prenum e x"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (eval r_auxhyp [e])) x = eval r_prenum [e, x]

goal (1 subgoal):
 1. \<phi> (the (eval r_auxhyp [e])) x = prenum e x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (eval r_auxhyp [e])) x = prenum e x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma auxhyp_prenum: "\<phi> (the (auxhyp e)) = prenum e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (the (auxhyp e)) = prenum e
[PROOF STEP]
using auxhyp_def r_auxhyp
[PROOF STATE]
proof (prove)
using this:
auxhyp ?e \<equiv> eval r_auxhyp [?e]
\<phi> (the (eval r_auxhyp [?e])) = prenum ?e

goal (1 subgoal):
 1. \<phi> (the (auxhyp e)) = prenum e
[PROOF STEP]
by metis


[STATEMENT]
lemma auxhyp_in_R1: "auxhyp \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. auxhyp \<in> \<R>
[PROOF STEP]
using auxhyp_def Mn_free_imp_total R1I r_auxhyp_prim
[PROOF STATE]
proof (prove)
using this:
auxhyp ?e \<equiv> eval r_auxhyp [?e]
\<lbrakk>wellf ?f; Mn_free ?f\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f
\<lbrakk>recfn 1 ?r; Partial_Recursive.total ?r; \<And>x. eval ?r [x] = ?f x\<rbrakk> \<Longrightarrow> ?f \<in> \<R>
prim_recfn 1 r_auxhyp

goal (1 subgoal):
 1. auxhyp \<in> \<R>
[PROOF STEP]
by metis


[STATEMENT]
lemma r_sv01_recfn: "recfn 1 r_sv01"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 r_sv01
[PROOF STEP]
unfolding r_sv01_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (let at0 = Cn 1 r_nth [recf.Id 1 0, Z]; at1 = Cn 1 r_nth [recf.Id 1 0, r_const 1]; m = Cn 1 r_amalgamate [at0, at1]; c = Cn 1 r_inconsist [m, recf.Id 1 0]; p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]; g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]] in Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0])
[PROOF STEP]
using r_auxhyp_prim r_inconsist_recfn r_amalgamate_recfn
[PROOF STATE]
proof (prove)
using this:
prim_recfn 1 r_auxhyp
recfn 2 r_inconsist
recfn 2 r_amalgamate

goal (1 subgoal):
 1. recfn 1 (let at0 = Cn 1 r_nth [recf.Id 1 0, Z]; at1 = Cn 1 r_nth [recf.Id 1 0, r_const 1]; m = Cn 1 r_amalgamate [at0, at1]; c = Cn 1 r_inconsist [m, recf.Id 1 0]; p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]; g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]] in Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0])
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma sv01_in_P1: "s\<^bsub>01\<^esub> \<in> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<^bsub>01\<^esub> \<in> \

[PROOF STEP]
using sv01_def r_sv01_recfn P1I
[PROOF STATE]
proof (prove)
using this:
s\<^bsub>01\<^esub> ?e \<equiv> eval r_sv01 [?e]
recfn 1 r_sv01
\<lbrakk>recfn 1 ?r; (\<lambda>x. eval ?r [x]) = ?f\<rbrakk> \<Longrightarrow> ?f \<in> \

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> \<in> \

[PROOF STEP]
by presburger


[STATEMENT]
lemma sv01:
  assumes "f \<in> V\<^sub>0\<^sub>1"
  shows "s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)"
    and "n \<noteq> 0 \<Longrightarrow>
      inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n \<Longrightarrow>
      s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f"
    and "n \<noteq> 0 \<Longrightarrow>
      the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n \<Longrightarrow>
      pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 \<Longrightarrow>
      s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1"
    and "n \<noteq> 0 \<Longrightarrow>
      the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n \<Longrightarrow>
      pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0 \<Longrightarrow>
      s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0) &&& (\<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f)) &&& (\<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1) &&& (\<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have f_total: "\<And>x. f x \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f x \<down>
[PROOF STEP]
using assms V01_def R1_imp_total1
[PROOF STATE]
proof (prove)
using this:
f \<in> V\<^sub>0\<^sub>1
V\<^sub>0\<^sub>1 = {f \<in> \<R>. \<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f}
?f \<in> \<R> \<Longrightarrow> total1 ?f

goal (1 subgoal):
 1. \<And>x. f x \<down>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ?x \<down>

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
define at0 where "at0 = Cn 1 r_nth [Id 1 0, Z]"
[PROOF STATE]
proof (state)
this:
at0 = Cn 1 r_nth [recf.Id 1 0, Z]

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
define at1 where "at1 = Cn 1 r_nth [Id 1 0, r_const 1]"
[PROOF STATE]
proof (state)
this:
at1 = Cn 1 r_nth [recf.Id 1 0, r_const 1]

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
define m where  "m = Cn 1 r_amalgamate [at0, at1]"
[PROOF STATE]
proof (state)
this:
m = Cn 1 r_amalgamate [at0, at1]

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
define c where "c = Cn 1 r_inconsist [m, Id 1 0]"
[PROOF STATE]
proof (state)
this:
c = Cn 1 r_inconsist [m, recf.Id 1 0]

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
define p where "p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]"
[PROOF STATE]
proof (state)
this:
p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
define g where "g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]]"
[PROOF STATE]
proof (state)
this:
g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]]

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "recfn 1 g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 g
[PROOF STEP]
unfolding g_def p_def c_def m_def at1_def at0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (Cn 1 r_ifeq [Cn 1 r_inconsist [Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]], recf.Id 1 0], r_length, Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]], Cn 1 r_ifz [Cn 1 r_pdec1 [Cn 1 r_parallel [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1], Cn 1 r_inconsist [Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]], recf.Id 1 0]]], Cn 1 r_nth [recf.Id 1 0, r_const 1], Cn 1 r_nth [recf.Id 1 0, Z]]])
[PROOF STEP]
using r_auxhyp_prim r_inconsist_recfn r_amalgamate_recfn
[PROOF STATE]
proof (prove)
using this:
prim_recfn 1 r_auxhyp
recfn 2 r_inconsist
recfn 2 r_amalgamate

goal (1 subgoal):
 1. recfn 1 (Cn 1 r_ifeq [Cn 1 r_inconsist [Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]], recf.Id 1 0], r_length, Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]], Cn 1 r_ifz [Cn 1 r_pdec1 [Cn 1 r_parallel [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1], Cn 1 r_inconsist [Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]], recf.Id 1 0]]], Cn 1 r_nth [recf.Id 1 0, r_const 1], Cn 1 r_nth [recf.Id 1 0, Z]]])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 g

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> 0] \<down>= 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> 0] \<down>= 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> 0] \<down>= 0

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> 0] \<down>= 0
[PROOF STEP]
have "eval r_sv01 [f \<triangleright> 0] = eval r_auxhyp [f \<triangleright> 0]"
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> 0] \<down>= 0

goal (1 subgoal):
 1. eval r_sv01 [f \<triangleright> 0] = eval r_auxhyp [f \<triangleright> 0]
[PROOF STEP]
unfolding r_sv01_def
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> 0] \<down>= 0

goal (1 subgoal):
 1. eval (let at0 = Cn 1 r_nth [recf.Id 1 0, Z]; at1 = Cn 1 r_nth [recf.Id 1 0, r_const 1]; m = Cn 1 r_amalgamate [at0, at1]; c = Cn 1 r_inconsist [m, recf.Id 1 0]; p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]; g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]] in Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]) [f \<triangleright> 0] = eval r_auxhyp [f \<triangleright> 0]
[PROOF STEP]
using \<open>recfn 1 g\<close> c_def g_def m_def p_def r_auxhyp_prim
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> 0] \<down>= 0
recfn 1 g
c = Cn 1 r_inconsist [m, recf.Id 1 0]
g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]]
m = Cn 1 r_amalgamate [at0, at1]
p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]
prim_recfn 1 r_auxhyp

goal (1 subgoal):
 1. eval (let at0 = Cn 1 r_nth [recf.Id 1 0, Z]; at1 = Cn 1 r_nth [recf.Id 1 0, r_const 1]; m = Cn 1 r_amalgamate [at0, at1]; c = Cn 1 r_inconsist [m, recf.Id 1 0]; p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]; g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]] in Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]) [f \<triangleright> 0] = eval r_auxhyp [f \<triangleright> 0]
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
eval r_sv01 [f \<triangleright> 0] = eval r_auxhyp [f \<triangleright> 0]

goal (4 subgoals):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
 2. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 4. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_sv01 [f \<triangleright> 0] = eval r_auxhyp [f \<triangleright> 0]
[PROOF STEP]
show "s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)"
[PROOF STATE]
proof (prove)
using this:
eval r_sv01 [f \<triangleright> 0] = eval r_auxhyp [f \<triangleright> 0]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)
[PROOF STEP]
by (simp add: auxhyp_def sv01_def)
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> 0) = auxhyp (f \<triangleright> 0)

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have sv01: "s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]" if "n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
have *: "eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0"
      (is "?r_eq \<down>\<noteq> 0")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
have "recfn 2 (r_lifz r_auxhyp g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (r_lifz r_auxhyp g)
[PROOF STEP]
using \<open>recfn 1 g\<close> r_auxhyp_prim
[PROOF STATE]
proof (prove)
using this:
recfn 1 g
prim_recfn 1 r_auxhyp

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

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
recfn 2 (r_lifz r_auxhyp g)

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
have "eval r_sv01 [f \<triangleright> n] =
        eval (Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], Id 1 0]) [f \<triangleright> n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_sv01 [f \<triangleright> n] = eval (Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]) [f \<triangleright> n]
[PROOF STEP]
using r_sv01_def
[PROOF STATE]
proof (prove)
using this:
r_sv01 \<equiv> let at0 = Cn 1 r_nth [recf.Id 1 0, Z]; at1 = Cn 1 r_nth [recf.Id 1 0, r_const 1]; m = Cn 1 r_amalgamate [at0, at1]; c = Cn 1 r_inconsist [m, recf.Id 1 0]; p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]; g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]] in Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]

goal (1 subgoal):
 1. eval r_sv01 [f \<triangleright> n] = eval (Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]) [f \<triangleright> n]
[PROOF STEP]
by (metis at0_def at1_def c_def g_def m_def p_def)
[PROOF STATE]
proof (state)
this:
eval r_sv01 [f \<triangleright> n] = eval (Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]) [f \<triangleright> n]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0
recfn 2 (r_lifz r_auxhyp g)
eval r_sv01 [f \<triangleright> n] = eval (Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]) [f \<triangleright> n]
[PROOF STEP]
have "eval r_sv01 [f \<triangleright> n] = eval (r_lifz r_auxhyp g) [the ?r_eq, f \<triangleright> n]"
[PROOF STATE]
proof (prove)
using this:
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0
recfn 2 (r_lifz r_auxhyp g)
eval r_sv01 [f \<triangleright> n] = eval (Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], recf.Id 1 0]) [f \<triangleright> n]

goal (1 subgoal):
 1. eval r_sv01 [f \<triangleright> n] = eval (r_lifz r_auxhyp g) [the (eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n]), f \<triangleright> n]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_sv01 [f \<triangleright> n] = eval (r_lifz r_auxhyp g) [the (eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n]), f \<triangleright> n]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_sv01 [f \<triangleright> n] = eval (r_lifz r_auxhyp g) [the (eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n]), f \<triangleright> n]
[PROOF STEP]
have "eval r_sv01 [f \<triangleright> n] = eval g [f \<triangleright> n]"
[PROOF STATE]
proof (prove)
using this:
eval r_sv01 [f \<triangleright> n] = eval (r_lifz r_auxhyp g) [the (eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n]), f \<triangleright> n]

goal (1 subgoal):
 1. eval r_sv01 [f \<triangleright> n] = eval g [f \<triangleright> n]
[PROOF STEP]
using "*" \<open>recfn 1 g\<close> r_auxhyp_prim
[PROOF STATE]
proof (prove)
using this:
eval r_sv01 [f \<triangleright> n] = eval (r_lifz r_auxhyp g) [the (eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n]), f \<triangleright> n]
eval (Cn 1 r_eq [r_length, r_const 1]) [f \<triangleright> n] \<down>\<noteq> 0
recfn 1 g
prim_recfn 1 r_auxhyp

goal (1 subgoal):
 1. eval r_sv01 [f \<triangleright> n] = eval g [f \<triangleright> n]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval r_sv01 [f \<triangleright> n] = eval g [f \<triangleright> n]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_sv01 [f \<triangleright> n] = eval g [f \<triangleright> n]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval r_sv01 [f \<triangleright> n] = eval g [f \<triangleright> n]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]
[PROOF STEP]
by (simp add: sv01_def that)
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "recfn 1 at0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 at0
[PROOF STEP]
unfolding at0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (Cn 1 r_nth [recf.Id 1 0, Z])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 at0

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have at0: "eval at0 [f \<triangleright> n] \<down>= the (f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval at0 [f \<triangleright> n] \<down>= the (f 0)
[PROOF STEP]
unfolding at0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 1 r_nth [recf.Id 1 0, Z]) [f \<triangleright> n] \<down>= the (f 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval at0 [f \<triangleright> n] \<down>= the (f 0)

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "recfn 1 at1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 at1
[PROOF STEP]
unfolding at1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (Cn 1 r_nth [recf.Id 1 0, r_const 1])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 at1

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have at1: "n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)
[PROOF STEP]
unfolding at1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_nth [recf.Id 1 0, r_const 1]) [f \<triangleright> n] \<down>= the (f 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "recfn 1 m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 m
[PROOF STEP]
unfolding m_def at0_def at1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]])
[PROOF STEP]
using r_amalgamate_recfn
[PROOF STATE]
proof (prove)
using this:
recfn 2 r_amalgamate

goal (1 subgoal):
 1. recfn 1 (Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 m

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have m: "n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f"
      (is "_ \<Longrightarrow> _ \<down>= ?m")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f
[PROOF STEP]
unfolding m_def at0_def at1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]]) [f \<triangleright> n] \<down>= amalg01 f
[PROOF STEP]
using at0 at1 amalgamate r_amalgamate r_amalgamate_recfn
[PROOF STATE]
proof (prove)
using this:
eval at0 [f \<triangleright> n] \<down>= the (f 0)
n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)
\<phi> (amalgamate ?i ?j) = amalgamation ?i ?j
eval r_amalgamate [?i, ?j] \<down>= amalgamate ?i ?j
recfn 2 r_amalgamate

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_amalgamate [Cn 1 r_nth [recf.Id 1 0, Z], Cn 1 r_nth [recf.Id 1 0, r_const 1]]) [f \<triangleright> n] \<down>= amalg01 f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f
[PROOF STEP]
have c: "n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)"
      (is "_ \<Longrightarrow> _ = ?c")
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_inconsist [m, recf.Id 1 0]) [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)
[PROOF STEP]
using r_inconsist_recfn \<open>recfn 1 m\<close> r_inconsist
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f
recfn 2 r_inconsist
recfn 1 m
eval r_inconsist [?i, ?e] = inconsist ?i ?e

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_inconsist [m, recf.Id 1 0]) [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)
[PROOF STEP]
have c_converg: "n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>
[PROOF STEP]
using inconsist_for_V01[OF assms]
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)
?k = amalg01 f \<Longrightarrow> inconsist ?k ?e \<down>= (if \<exists>x<e_length ?e. \<phi> ?k x \<down>\<noteq> e_nth ?e x then LEAST x. x < e_length ?e \<and> \<phi> ?k x \<down>\<noteq> e_nth ?e x else e_length ?e)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "recfn 1 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 c
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (Cn 1 r_inconsist [m, recf.Id 1 0])
[PROOF STEP]
using \<open>recfn 1 m\<close> r_inconsist_recfn
[PROOF STATE]
proof (prove)
using this:
recfn 1 m
recfn 2 r_inconsist

goal (1 subgoal):
 1. recfn 1 (Cn 1 r_inconsist [m, recf.Id 1 0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 c

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have par: "n \<noteq> 0 \<Longrightarrow>
      eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] = parallel (the (f 0)) (the (f 1)) (the ?c)"
      (is "_ \<Longrightarrow> _ = ?par")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] = parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
using at0 at1 c c_converg m r_parallel' \<open>recfn 1 at0\<close> \<open>recfn 1 at1\<close> \<open>recfn 1 c\<close>
[PROOF STATE]
proof (prove)
using this:
eval at0 [f \<triangleright> n] \<down>= the (f 0)
n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>
n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f
eval r_parallel [?i, ?j, ?x] = parallel ?i ?j ?x
recfn 1 at0
recfn 1 at1
recfn 1 c

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] = parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] = parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
with parallel_converg_V01[OF assms]
[PROOF STATE]
proof (chain)
picking this:
parallel (the (f 0)) (the (f 1)) ?x \<down>
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] = parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))
[PROOF STEP]
have
      par_converg: "n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>"
[PROOF STATE]
proof (prove)
using this:
parallel (the (f 0)) (the (f 1)) ?x \<down>
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] = parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>
[PROOF STEP]
have p_converg: "n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]) [f \<triangleright> n] \<down>
[PROOF STEP]
using at0 at1 c_converg \<open>recfn 1 at0\<close> \<open>recfn 1 at1\<close> \<open>recfn 1 c\<close>
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>
eval at0 [f \<triangleright> n] \<down>= the (f 0)
n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>
recfn 1 at0
recfn 1 at1
recfn 1 c

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]) [f \<triangleright> n] \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have p: "n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>= pdec1 (the ?par)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>= pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]) [f \<triangleright> n] \<down>= pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
using at0 at1 c_converg \<open>recfn 1 at0\<close> \<open>recfn 1 at1\<close> \<open>recfn 1 c\<close> par par_converg
[PROOF STATE]
proof (prove)
using this:
eval at0 [f \<triangleright> n] \<down>= the (f 0)
n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>
recfn 1 at0
recfn 1 at1
recfn 1 c
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] = parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_parallel [at0, at1, c]) [f \<triangleright> n] \<down>

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]) [f \<triangleright> n] \<down>= pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>= pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "recfn 1 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 p
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 (Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]])
[PROOF STEP]
using \<open>recfn 1 at0\<close> \<open>recfn 1 at1\<close> \<open>recfn 1 m\<close> \<open>recfn 1 c\<close>
[PROOF STATE]
proof (prove)
using this:
recfn 1 at0
recfn 1 at1
recfn 1 m
recfn 1 c

goal (1 subgoal):
 1. recfn 1 (Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 p

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
let ?r = "Cn 1 r_ifz [p, at1, at0]"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have r: "n \<noteq> 0 \<Longrightarrow> eval ?r [f \<triangleright> n] = (if pdec1 (the ?par) = 0 then f 1 else f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n] = (if pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 then f 1 else f 0)
[PROOF STEP]
using at0 at1 c_converg \<open>recfn 1 at0\<close> \<open>recfn 1 at1\<close> \<open>recfn 1 c\<close>
      \<open>recfn 1 m\<close> \<open>recfn 1 p\<close> p f_total
[PROOF STATE]
proof (prove)
using this:
eval at0 [f \<triangleright> n] \<down>= the (f 0)
n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>
recfn 1 at0
recfn 1 at1
recfn 1 c
recfn 1 m
recfn 1 p
n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>= pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n)))))
f ?x \<down>

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n] = (if pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 then f 1 else f 0)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n] = (if pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 then f 1 else f 0)

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have g: "n \<noteq> 0 \<Longrightarrow>
      eval g [f \<triangleright> n] \<down>=
        (if the ?c = e_length (f \<triangleright> n)
         then ?m else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]]) [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))
[PROOF STEP]
using \<open>recfn 1 p\<close> \<open>recfn 1 at0\<close> \<open>recfn 1 at1\<close> \<open>recfn 1 c\<close> \<open>recfn 1 m\<close>
      p_converg at1 at0 c c_converg m
[PROOF STATE]
proof (prove)
using this:
recfn 1 p
recfn 1 at0
recfn 1 at1
recfn 1 c
recfn 1 m
n \<noteq> 0 \<Longrightarrow> eval p [f \<triangleright> n] \<down>
n \<noteq> 0 \<Longrightarrow> eval at1 [f \<triangleright> n] \<down>= the (f 1)
eval at0 [f \<triangleright> n] \<down>= the (f 0)
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] = inconsist (amalg01 f) (f \<triangleright> n)
n \<noteq> 0 \<Longrightarrow> eval c [f \<triangleright> n] \<down>
n \<noteq> 0 \<Longrightarrow> eval m [f \<triangleright> n] \<down>= amalg01 f

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]]) [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
assume "n \<noteq> 0" and "?c \<down>= Suc n"
[PROOF STATE]
proof (state)
this:
n \<noteq> 0
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<noteq> 0
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
have "e_length (f \<triangleright> n) = Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_length (f \<triangleright> n) = Suc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e_length (f \<triangleright> n) = Suc n

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n
e_length (f \<triangleright> n) = Suc n
[PROOF STEP]
have "eval g [f \<triangleright> n] \<down>= ?m"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n
e_length (f \<triangleright> n) = Suc n

goal (1 subgoal):
 1. eval g [f \<triangleright> n] \<down>= amalg01 f
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0
inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n
e_length (f \<triangleright> n) = Suc n
n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))

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

goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; inconsist (amalg01 f) (f \<triangleright> n) \<down>= Suc n\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 3. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval g [f \<triangleright> n] \<down>= amalg01 f
[PROOF STEP]
show "s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f"
[PROOF STATE]
proof (prove)
using this:
eval g [f \<triangleright> n] \<down>= amalg01 f

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
[PROOF STEP]
using sv01[OF \<open>n \<noteq> 0\<close>]
[PROOF STATE]
proof (prove)
using this:
eval g [f \<triangleright> n] \<down>= amalg01 f
s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) \<down>= amalg01 f

goal (2 subgoals):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
assume "n \<noteq> 0" and "the ?c < Suc n" and "pdec1 (the ?par) = 0"
[PROOF STATE]
proof (state)
this:
n \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0

goal (2 subgoals):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
with g r f_total
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n] = (if pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 then f 1 else f 0)
f ?x \<down>
n \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0
[PROOF STEP]
have "eval g [f \<triangleright> n] = f 1"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n] = (if pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 then f 1 else f 0)
f ?x \<down>
n \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0

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

goal (2 subgoals):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
 2. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval g [f \<triangleright> n] = f 1
[PROOF STEP]
show "s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1"
[PROOF STATE]
proof (prove)
using this:
eval g [f \<triangleright> n] = f 1

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
[PROOF STEP]
using sv01[OF \<open>n \<noteq> 0\<close>]
[PROOF STATE]
proof (prove)
using this:
eval g [f \<triangleright> n] = f 1
s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 1

goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
assume "n \<noteq> 0" and "the ?c < Suc n" and "pdec1 (the ?par) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
n \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
with g r f_total
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n] = (if pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 then f 1 else f 0)
f ?x \<down>
n \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0
[PROOF STEP]
have "eval g [f \<triangleright> n] = f 0"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> eval g [f \<triangleright> n] \<down>= (if the (inconsist (amalg01 f) (f \<triangleright> n)) = e_length (f \<triangleright> n) then amalg01 f else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n]))
n \<noteq> 0 \<Longrightarrow> eval (Cn 1 r_ifz [p, at1, at0]) [f \<triangleright> n] = (if pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) = 0 then f 1 else f 0)
f ?x \<down>
n \<noteq> 0
the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n
pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0

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

goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval g [f \<triangleright> n] = f 0
[PROOF STEP]
show "s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0"
[PROOF STATE]
proof (prove)
using this:
eval g [f \<triangleright> n] = f 0

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
using sv01[OF \<open>n \<noteq> 0\<close>]
[PROOF STATE]
proof (prove)
using this:
eval g [f \<triangleright> n] = f 0
s\<^bsub>01\<^esub> (f \<triangleright> n) = eval g [f \<triangleright> n]

goal (1 subgoal):
 1. s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<noteq> 0; the (inconsist (amalg01 f) (f \<triangleright> n)) < Suc n; pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \<triangleright> n))))) \<noteq> 0\<rbrakk> \<Longrightarrow> s\<^bsub>01\<^esub> (f \<triangleright> n) = f 0

goal:
No subgoals!
[PROOF STEP]
qed