[STATEMENT]
lemma adverse_in_R3: "\<exists>r. recfn 3 r \<and> total r \<and> (\<lambda>i j x. eval r [i, j, x]) = adverse z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
obtain rs where rs: "recfn 1 rs" "total rs" "(\<lambda>x. eval rs [x]) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>rs. \<lbrakk>recfn 1 rs; Partial_Recursive.total rs; (\<lambda>x. eval rs [x]) = s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R1E
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> \<R>; \<And>r. \<lbrakk>recfn 1 r; Partial_Recursive.total r; ?f = (\<lambda>x. eval r [x])\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
have s_total: "\<And>x. s x \<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. s x \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s ?x \<down>

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define f where "f = Cn 2 r_singleton_encode [Id 2 0]"
[PROOF STATE]
proof (state)
this:
f = Cn 2 r_singleton_encode [recf.Id 2 0]

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f = Cn 2 r_singleton_encode [recf.Id 2 0]
[PROOF STEP]
have "recfn 2 f"
[PROOF STATE]
proof (prove)
using this:
f = Cn 2 r_singleton_encode [recf.Id 2 0]

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

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
have f: "\<And>i j. eval f [i, j] \<down>= list_encode [i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. eval f [i, j] \<down>= singleton_encode i
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. eval (Cn 2 r_singleton_encode [recf.Id 2 0]) [i, j] \<down>= singleton_encode i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval f [?i, ?j] \<down>= singleton_encode ?i

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define ch1 where "ch1 = Cn 4 r_ifeq
    [Cn 4 rs [Cn 4 r_snoc [Id 4 1, r_constn 3 1]],
     Cn 4 rs [Id 4 1],
     r_dummy 3 (r_const z),
     r_constn 3 1]"
[PROOF STATE]
proof (state)
this:
ch1 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 1]], Cn 4 rs [recf.Id 4 1], r_dummy 3 (r_const z), r_constn 3 1]

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ch1 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 1]], Cn 4 rs [recf.Id 4 1], r_dummy 3 (r_const z), r_constn 3 1]
[PROOF STEP]
have ch1: "recfn 4 ch1" "total ch1"
[PROOF STATE]
proof (prove)
using this:
ch1 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 1]], Cn 4 rs [recf.Id 4 1], r_dummy 3 (r_const z), r_constn 3 1]

goal (1 subgoal):
 1. recfn 4 ch1 &&& Partial_Recursive.total ch1
[PROOF STEP]
using Cn_total prim_recfn_total rs
[PROOF STATE]
proof (prove)
using this:
ch1 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 1]], Cn 4 rs [recf.Id 4 1], r_dummy 3 (r_const z), r_constn 3 1]
\<lbrakk>\<forall>g\<in>set ?gs. Partial_Recursive.total g; Partial_Recursive.total ?f; recfn ?n (Cn ?n ?f ?gs)\<rbrakk> \<Longrightarrow> Partial_Recursive.total (Cn ?n ?f ?gs)
prim_recfn ?n ?f \<Longrightarrow> Partial_Recursive.total ?f
recfn 1 rs
Partial_Recursive.total rs
(\<lambda>x. eval rs [x]) = s

goal (1 subgoal):
 1. recfn 4 ch1 &&& Partial_Recursive.total ch1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 4 ch1
Partial_Recursive.total ch1

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define ch0 where "ch0 = Cn 4 r_ifeq
    [Cn 4 rs [Cn 4 r_snoc [Id 4 1, r_constn 3 0]],
     Cn 4 rs [Id 4 1],
     ch1,
     r_constn 3 0]"
[PROOF STATE]
proof (state)
this:
ch0 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 0]], Cn 4 rs [recf.Id 4 1], ch1, r_constn 3 0]

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ch0 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 0]], Cn 4 rs [recf.Id 4 1], ch1, r_constn 3 0]
[PROOF STEP]
have ch0_total: "total ch0" "recfn 4 ch0"
[PROOF STATE]
proof (prove)
using this:
ch0 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 0]], Cn 4 rs [recf.Id 4 1], ch1, r_constn 3 0]

goal (1 subgoal):
 1. Partial_Recursive.total ch0 &&& recfn 4 ch0
[PROOF STEP]
using Cn_total prim_recfn_total rs ch1
[PROOF STATE]
proof (prove)
using this:
ch0 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 0]], Cn 4 rs [recf.Id 4 1], ch1, r_constn 3 0]
\<lbrakk>\<forall>g\<in>set ?gs. Partial_Recursive.total g; Partial_Recursive.total ?f; recfn ?n (Cn ?n ?f ?gs)\<rbrakk> \<Longrightarrow> Partial_Recursive.total (Cn ?n ?f ?gs)
prim_recfn ?n ?f \<Longrightarrow> Partial_Recursive.total ?f
recfn 1 rs
Partial_Recursive.total rs
(\<lambda>x. eval rs [x]) = s
recfn 4 ch1
Partial_Recursive.total ch1

goal (1 subgoal):
 1. Partial_Recursive.total ch0 &&& recfn 4 ch0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Partial_Recursive.total ch0
recfn 4 ch0

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
have "eval ch1 [l, v, i, j] \<down>= (if s (e_snoc v 1) = s v then z else 1)" for l v i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval ch1 [l, v, i, j] \<down>= (if s (e_snoc v 1) = s v then z else 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval ch1 [l, v, i, j] \<down>= (if s (e_snoc v 1) = s v then z else 1)
[PROOF STEP]
have "eval ch1 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval ch1 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]
[PROOF STEP]
unfolding ch1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 1]], Cn 4 rs [recf.Id 4 1], r_dummy 3 (r_const z), r_constn 3 1]) [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]
[PROOF STEP]
using rs
[PROOF STATE]
proof (prove)
using this:
recfn 1 rs
Partial_Recursive.total rs
(\<lambda>x. eval rs [x]) = s

goal (1 subgoal):
 1. eval (Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 1]], Cn 4 rs [recf.Id 4 1], r_dummy 3 (r_const z), r_constn 3 1]) [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval ch1 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]

goal (1 subgoal):
 1. eval ch1 [l, v, i, j] \<down>= (if s (e_snoc v 1) = s v then z else 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval ch1 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval ch1 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]

goal (1 subgoal):
 1. eval ch1 [l, v, i, j] \<down>= (if s (e_snoc v 1) = s v then z else 1)
[PROOF STEP]
by (simp add: s_total option.expand)
[PROOF STATE]
proof (state)
this:
eval ch1 [l, v, i, j] \<down>= (if s (e_snoc v 1) = s v then z else 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval ch1 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 1) = s ?v then z else 1)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval ch1 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 1) = s ?v then z else 1)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
have "eval ch0 [l, v, i, j] \<down>=
    (if s (e_snoc v 0) = s v then the (eval ch1 [l, v, i, j]) else 0)" for l v i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval ch0 [l, v, i, j] \<down>= (if s (e_snoc v 0) = s v then the (eval ch1 [l, v, i, j]) else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval ch0 [l, v, i, j] \<down>= (if s (e_snoc v 0) = s v then the (eval ch1 [l, v, i, j]) else 0)
[PROOF STEP]
have "eval ch0 [l, v, i, j] =
        eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval ch0 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]
[PROOF STEP]
unfolding ch0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 0]], Cn 4 rs [recf.Id 4 1], ch1, r_constn 3 0]) [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]
[PROOF STEP]
using rs ch1
[PROOF STATE]
proof (prove)
using this:
recfn 1 rs
Partial_Recursive.total rs
(\<lambda>x. eval rs [x]) = s
recfn 4 ch1
Partial_Recursive.total ch1

goal (1 subgoal):
 1. eval (Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [recf.Id 4 1, r_constn 3 0]], Cn 4 rs [recf.Id 4 1], ch1, r_constn 3 0]) [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval ch0 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]

goal (1 subgoal):
 1. eval ch0 [l, v, i, j] \<down>= (if s (e_snoc v 0) = s v then the (eval ch1 [l, v, i, j]) else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval ch0 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval ch0 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]

goal (1 subgoal):
 1. eval ch0 [l, v, i, j] \<down>= (if s (e_snoc v 0) = s v then the (eval ch1 [l, v, i, j]) else 0)
[PROOF STEP]
by (simp add: s_total option.expand)
[PROOF STATE]
proof (state)
this:
eval ch0 [l, v, i, j] \<down>= (if s (e_snoc v 0) = s v then the (eval ch1 [l, v, i, j]) else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval ch0 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 0) = s ?v then the (eval ch1 [?l, ?v, ?i, ?j]) else 0)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval ch1 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 1) = s ?v then z else 1)
eval ch0 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 0) = s ?v then the (eval ch1 [?l, ?v, ?i, ?j]) else 0)
[PROOF STEP]
have ch0: "\<And>l v i j. eval ch0 [l, v, i, j] \<down>=
    (if s (e_snoc v 0) \<noteq> s v then 0
     else if s (e_snoc v 1) \<noteq> s v then 1 else z)"
[PROOF STATE]
proof (prove)
using this:
eval ch1 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 1) = s ?v then z else 1)
eval ch0 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 0) = s ?v then the (eval ch1 [?l, ?v, ?i, ?j]) else 0)

goal (1 subgoal):
 1. \<And>l v i j. eval ch0 [l, v, i, j] \<down>= (if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval ch0 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define app where "app = Cn 4 r_ifz [Id 4 0, Id 4 3, ch0]"
[PROOF STATE]
proof (state)
this:
app = Cn 4 r_ifz [recf.Id 4 0, recf.Id 4 3, ch0]

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
app = Cn 4 r_ifz [recf.Id 4 0, recf.Id 4 3, ch0]
[PROOF STEP]
have "recfn 4 app" "total app"
[PROOF STATE]
proof (prove)
using this:
app = Cn 4 r_ifz [recf.Id 4 0, recf.Id 4 3, ch0]

goal (1 subgoal):
 1. recfn 4 app &&& Partial_Recursive.total app
[PROOF STEP]
using ch0_total totalI4
[PROOF STATE]
proof (prove)
using this:
app = Cn 4 r_ifz [recf.Id 4 0, recf.Id 4 3, ch0]
Partial_Recursive.total ch0
recfn 4 ch0
\<lbrakk>recfn 4 ?f; \<And>w x y z. eval ?f [w, x, y, z] \<down>\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f

goal (1 subgoal):
 1. recfn 4 app &&& Partial_Recursive.total app
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 4 app
Partial_Recursive.total app

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
have "eval app [l, v, i, j] \<down>= (if l = 0 then j else the (eval ch0 [l, v, i, j]))" for l v i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval app [l, v, i, j] \<down>= (if l = 0 then j else the (eval ch0 [l, v, i, j]))
[PROOF STEP]
unfolding app_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 4 r_ifz [recf.Id 4 0, recf.Id 4 3, ch0]) [l, v, i, j] \<down>= (if l = 0 then j else the (eval ch0 [l, v, i, j]))
[PROOF STEP]
using ch0_total
[PROOF STATE]
proof (prove)
using this:
Partial_Recursive.total ch0
recfn 4 ch0

goal (1 subgoal):
 1. eval (Cn 4 r_ifz [recf.Id 4 0, recf.Id 4 3, ch0]) [l, v, i, j] \<down>= (if l = 0 then j else the (eval ch0 [l, v, i, j]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval app [?l, ?v, ?i, ?j] \<down>= (if ?l = 0 then ?j else the (eval ch0 [?l, ?v, ?i, ?j]))

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
with ch0
[PROOF STATE]
proof (chain)
picking this:
eval ch0 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)
eval app [?l, ?v, ?i, ?j] \<down>= (if ?l = 0 then ?j else the (eval ch0 [?l, ?v, ?i, ?j]))
[PROOF STEP]
have app: "\<And>l v i j. eval app [l, v, i, j] \<down>=
    (if l = 0 then j
     else if s (e_snoc v 0) \<noteq> s v then 0
     else if s (e_snoc v 1) \<noteq> s v then 1 else z)"
[PROOF STATE]
proof (prove)
using this:
eval ch0 [?l, ?v, ?i, ?j] \<down>= (if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)
eval app [?l, ?v, ?i, ?j] \<down>= (if ?l = 0 then ?j else the (eval ch0 [?l, ?v, ?i, ?j]))

goal (1 subgoal):
 1. \<And>l v i j. eval app [l, v, i, j] \<down>= (if l = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval app [?l, ?v, ?i, ?j] \<down>= (if ?l = 0 then ?j else if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define g where "g = Cn 4 r_snoc [Id 4 1, app]"
[PROOF STATE]
proof (state)
this:
g = Cn 4 r_snoc [recf.Id 4 1, app]

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
with app
[PROOF STATE]
proof (chain)
picking this:
eval app [?l, ?v, ?i, ?j] \<down>= (if ?l = 0 then ?j else if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)
g = Cn 4 r_snoc [recf.Id 4 1, app]
[PROOF STEP]
have g: "\<And>l v i j. eval g [l, v, i, j] \<down>= e_snoc v
    (if l = 0 then j
     else if s (e_snoc v 0) \<noteq> s v then 0
     else if s (e_snoc v 1) \<noteq> s v then 1 else z)"
[PROOF STATE]
proof (prove)
using this:
eval app [?l, ?v, ?i, ?j] \<down>= (if ?l = 0 then ?j else if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)
g = Cn 4 r_snoc [recf.Id 4 1, app]

goal (1 subgoal):
 1. \<And>l v i j. eval g [l, v, i, j] \<down>= e_snoc v (if l = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z)
[PROOF STEP]
using \<open>recfn 4 app\<close>
[PROOF STATE]
proof (prove)
using this:
eval app [?l, ?v, ?i, ?j] \<down>= (if ?l = 0 then ?j else if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)
g = Cn 4 r_snoc [recf.Id 4 1, app]
recfn 4 app

goal (1 subgoal):
 1. \<And>l v i j. eval g [l, v, i, j] \<down>= e_snoc v (if l = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval g [?l, ?v, ?i, ?j] \<down>= e_snoc ?v (if ?l = 0 then ?j else if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
from g_def
[PROOF STATE]
proof (chain)
picking this:
g = Cn 4 r_snoc [recf.Id 4 1, app]
[PROOF STEP]
have "recfn 4 g" "total g"
[PROOF STATE]
proof (prove)
using this:
g = Cn 4 r_snoc [recf.Id 4 1, app]

goal (1 subgoal):
 1. recfn 4 g &&& Partial_Recursive.total g
[PROOF STEP]
using \<open>recfn 4 app\<close> \<open>total app\<close> Cn_total Mn_free_imp_total
[PROOF STATE]
proof (prove)
using this:
g = Cn 4 r_snoc [recf.Id 4 1, app]
recfn 4 app
Partial_Recursive.total app
\<lbrakk>\<forall>g\<in>set ?gs. Partial_Recursive.total g; Partial_Recursive.total ?f; recfn ?n (Cn ?n ?f ?gs)\<rbrakk> \<Longrightarrow> Partial_Recursive.total (Cn ?n ?f ?gs)
\<lbrakk>wellf ?f; Mn_free ?f\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f

goal (1 subgoal):
 1. recfn 4 g &&& Partial_Recursive.total g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 4 g
Partial_Recursive.total g

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define b where "b = Pr 2 f g"
[PROOF STATE]
proof (state)
this:
b = Pr 2 f g

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = Pr 2 f g
[PROOF STEP]
have "recfn 3 b"
[PROOF STATE]
proof (prove)
using this:
b = Pr 2 f g

goal (1 subgoal):
 1. recfn 3 b
[PROOF STEP]
using \<open>recfn 2 f\<close> \<open>recfn 4 g\<close>
[PROOF STATE]
proof (prove)
using this:
b = Pr 2 f g
recfn 2 f
recfn 4 g

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

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
have b: "eval b [x, i, j] \<down>= list_encode (prefixes z i j x)" for x i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)
[PROOF STEP]
proof (induction x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval b [0, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j 0)
 2. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. eval b [0, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j 0)
 2. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval b [0, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j 0)
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 2 f g) [0, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j 0)
[PROOF STEP]
using f \<open>recfn 2 f\<close> \<open>recfn 4 g\<close>
[PROOF STATE]
proof (prove)
using this:
eval f [?i, ?j] \<down>= singleton_encode ?i
recfn 2 f
recfn 4 g

goal (1 subgoal):
 1. eval (Pr 2 f g) [0, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval b [0, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j 0)

goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)

goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)
[PROOF STEP]
have "eval b [Suc x, i, j] = eval g [x, the (eval b [x, i, j]), i, j]"
[PROOF STATE]
proof (prove)
using this:
eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)

goal (1 subgoal):
 1. eval b [Suc x, i, j] = eval g [x, the (eval b [x, i, j]), i, j]
[PROOF STEP]
using b_def \<open>recfn 3 b\<close>
[PROOF STATE]
proof (prove)
using this:
eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)
b = Pr 2 f g
recfn 3 b

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

goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval b [Suc x, i, j] = eval g [x, the (eval b [x, i, j]), i, j]

goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
have "... \<down>=
     (let v = list_encode (prefixes z i j x)
      in e_snoc v
        (if x = 0 then j
         else if s (e_snoc v 0) \<noteq> s v then 0
              else if s (e_snoc v 1) \<noteq> s v then 1 else z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval g [x, the (eval b [x, i, j]), i, j] \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z))
[PROOF STEP]
using g Suc
[PROOF STATE]
proof (prove)
using this:
eval g [?l, ?v, ?i, ?j] \<down>= e_snoc ?v (if ?l = 0 then ?j else if s (e_snoc ?v 0) \<noteq> s ?v then 0 else if s (e_snoc ?v 1) \<noteq> s ?v then 1 else z)
eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)

goal (1 subgoal):
 1. eval g [x, the (eval b [x, i, j]), i, j] \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval g [x, the (eval b [x, i, j]), i, j] \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z))

goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval g [x, the (eval b [x, i, j]), i, j] \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z))

goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
have "... \<down>=
     (let v = list_encode (prefixes z i j x)
      in e_snoc v
        (if x = 0 then j
         else if s (list_encode (prefixes z i j x @ [0])) \<noteq> s v then 0
              else if s (list_encode (prefixes z i j x @ [1])) \<noteq> s v then 1 else z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z)) \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s v then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s v then 1 else z))
[PROOF STEP]
using list_decode_encode
[PROOF STATE]
proof (prove)
using this:
Partial_Recursive.list_decode (Partial_Recursive.list_encode ?xs) = ?xs

goal (1 subgoal):
 1. Some (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z)) \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s v then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s v then 1 else z))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
Some (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \<noteq> s v then 0 else if s (e_snoc v 1) \<noteq> s v then 1 else z)) \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s v then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s v then 1 else z))

goal (1 subgoal):
 1. \<And>x. eval b [x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x) \<Longrightarrow> eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval b [Suc x, i, j] \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s v then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s v then 1 else z))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval b [Suc x, i, j] \<down>= (let v = Partial_Recursive.list_encode (local.prefixes z i j x) in e_snoc v (if x = 0 then j else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s v then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s v then 1 else z))

goal (1 subgoal):
 1. eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval b [Suc x, i, j] \<down>= Partial_Recursive.list_encode (local.prefixes z i j (Suc x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval b [?x, ?i, ?j] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define b' where "b' = Cn 3 b [Id 3 2, Id 3 0, Id 3 1]"
[PROOF STATE]
proof (state)
this:
b' = Cn 3 b [recf.Id 3 2, recf.Id 3 0, recf.Id 3 1]

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b' = Cn 3 b [recf.Id 3 2, recf.Id 3 0, recf.Id 3 1]
[PROOF STEP]
have "recfn 3 b'"
[PROOF STATE]
proof (prove)
using this:
b' = Cn 3 b [recf.Id 3 2, recf.Id 3 0, recf.Id 3 1]

goal (1 subgoal):
 1. recfn 3 b'
[PROOF STEP]
using \<open>recfn 3 b\<close>
[PROOF STATE]
proof (prove)
using this:
b' = Cn 3 b [recf.Id 3 2, recf.Id 3 0, recf.Id 3 1]
recfn 3 b

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

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
eval b [?x, ?i, ?j] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)
recfn 3 b'
[PROOF STEP]
have b': "\<And>i j x. eval b' [i, j, x] \<down>= list_encode (prefixes z i j x)"
[PROOF STATE]
proof (prove)
using this:
eval b [?x, ?i, ?j] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)
recfn 3 b'

goal (1 subgoal):
 1. \<And>i j x. eval b' [i, j, x] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)
[PROOF STEP]
using b'_def
[PROOF STATE]
proof (prove)
using this:
eval b [?x, ?i, ?j] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)
recfn 3 b'
b' = Cn 3 b [recf.Id 3 2, recf.Id 3 0, recf.Id 3 1]

goal (1 subgoal):
 1. \<And>i j x. eval b' [i, j, x] \<down>= Partial_Recursive.list_encode (local.prefixes z i j x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval b' [?i, ?j, ?x] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
define r where "r = Cn 3 r_last [b']"
[PROOF STATE]
proof (state)
this:
r = Cn 3 r_last [b']

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = Cn 3 r_last [b']
[PROOF STEP]
have "recfn 3 r"
[PROOF STATE]
proof (prove)
using this:
r = Cn 3 r_last [b']

goal (1 subgoal):
 1. recfn 3 r
[PROOF STEP]
using \<open>recfn 3 b'\<close>
[PROOF STATE]
proof (prove)
using this:
r = Cn 3 r_last [b']
recfn 3 b'

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

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
with b'
[PROOF STATE]
proof (chain)
picking this:
eval b' [?i, ?j, ?x] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)
recfn 3 r
[PROOF STEP]
have "\<And>i j x. eval r [i, j, x] \<down>= last (prefixes z i j x)"
[PROOF STATE]
proof (prove)
using this:
eval b' [?i, ?j, ?x] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)
recfn 3 r

goal (1 subgoal):
 1. \<And>i j x. eval r [i, j, x] \<down>= last (local.prefixes z i j x)
[PROOF STEP]
using r_def prefixes_length
[PROOF STATE]
proof (prove)
using this:
eval b' [?i, ?j, ?x] \<down>= Partial_Recursive.list_encode (local.prefixes z ?i ?j ?x)
recfn 3 r
r = Cn 3 r_last [b']
length (local.prefixes ?z ?i ?j ?x) = Suc ?x

goal (1 subgoal):
 1. \<And>i j x. eval r [i, j, x] \<down>= last (local.prefixes z i j x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)
[PROOF STEP]
have "total r"
[PROOF STATE]
proof (prove)
using this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)

goal (1 subgoal):
 1. Partial_Recursive.total r
[PROOF STEP]
using totalI3 \<open>recfn 3 r\<close>
[PROOF STATE]
proof (prove)
using this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)
\<lbrakk>recfn 3 ?f; \<And>x y z. eval ?f [x, y, z] \<down>\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f
recfn 3 r

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

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)
Partial_Recursive.total r
[PROOF STEP]
have "(\<lambda>i j x. eval r [i, j, x]) = adverse z"
[PROOF STATE]
proof (prove)
using this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)
Partial_Recursive.total r

goal (1 subgoal):
 1. (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
unfolding adverse_def
[PROOF STATE]
proof (prove)
using this:
eval r [?i, ?j, ?x] \<down>= last (local.prefixes z ?i ?j ?x)
Partial_Recursive.total r

goal (1 subgoal):
 1. (\<lambda>i j x. eval r [i, j, x]) = (\<lambda>i j x. Some (last (local.prefixes z i j x)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
with \<open>recfn 3 r\<close> \<open>total r\<close>
[PROOF STATE]
proof (chain)
picking this:
recfn 3 r
Partial_Recursive.total r
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
recfn 3 r
Partial_Recursive.total r
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z

goal (1 subgoal):
 1. \<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adverse_in_R1: "adverse z i j \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
from adverse_in_R3
[PROOF STATE]
proof (chain)
picking this:
\<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse ?z
[PROOF STEP]
obtain r where
    r: "recfn 3 r" "total r" "(\<lambda>i j x. eval r [i, j, x]) = adverse z"
[PROOF STATE]
proof (prove)
using this:
\<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse ?z

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>recfn 3 r; Partial_Recursive.total r; (\<lambda>i j x. eval r [i, j, x]) = local.adverse z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
recfn 3 r
Partial_Recursive.total r
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z

goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
define rij where "rij = Cn 1 r [r_const i, r_const j, Id 1 0]"
[PROOF STATE]
proof (state)
this:
rij = Cn 1 r [r_const i, r_const j, recf.Id 1 0]

goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rij = Cn 1 r [r_const i, r_const j, recf.Id 1 0]
[PROOF STEP]
have "recfn 1 rij" "total rij"
[PROOF STATE]
proof (prove)
using this:
rij = Cn 1 r [r_const i, r_const j, recf.Id 1 0]

goal (1 subgoal):
 1. recfn 1 rij &&& Partial_Recursive.total rij
[PROOF STEP]
using r(1,2) Cn_total Mn_free_imp_total
[PROOF STATE]
proof (prove)
using this:
rij = Cn 1 r [r_const i, r_const j, recf.Id 1 0]
recfn 3 r
Partial_Recursive.total r
\<lbrakk>\<forall>g\<in>set ?gs. Partial_Recursive.total g; Partial_Recursive.total ?f; recfn ?n (Cn ?n ?f ?gs)\<rbrakk> \<Longrightarrow> Partial_Recursive.total (Cn ?n ?f ?gs)
\<lbrakk>wellf ?f; Mn_free ?f\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f

goal (1 subgoal):
 1. recfn 1 rij &&& Partial_Recursive.total rij
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 rij
Partial_Recursive.total rij

goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
from rij_def
[PROOF STATE]
proof (chain)
picking this:
rij = Cn 1 r [r_const i, r_const j, recf.Id 1 0]
[PROOF STEP]
have "\<And>x. eval rij [x] = eval r [i, j, x]"
[PROOF STATE]
proof (prove)
using this:
rij = Cn 1 r [r_const i, r_const j, recf.Id 1 0]

goal (1 subgoal):
 1. \<And>x. eval rij [x] = eval r [i, j, x]
[PROOF STEP]
using r(1)
[PROOF STATE]
proof (prove)
using this:
rij = Cn 1 r [r_const i, r_const j, recf.Id 1 0]
recfn 3 r

goal (1 subgoal):
 1. \<And>x. eval rij [x] = eval r [i, j, x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval rij [?x] = eval r [i, j, ?x]

goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
with r(3)
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z
eval rij [?x] = eval r [i, j, ?x]
[PROOF STEP]
have "\<And>x. eval rij [x] = adverse z i j x"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z
eval rij [?x] = eval r [i, j, ?x]

goal (1 subgoal):
 1. \<And>x. eval rij [x] = local.adverse z i j x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
eval rij [?x] = local.adverse z i j ?x

goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
with \<open>recfn 1 rij\<close> \<open>total rij\<close>
[PROOF STATE]
proof (chain)
picking this:
recfn 1 rij
Partial_Recursive.total rij
eval rij [?x] = local.adverse z i j ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
recfn 1 rij
Partial_Recursive.total rij
eval rij [?x] = local.adverse z i j ?x

goal (1 subgoal):
 1. local.adverse z i j \<in> \<R>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.adverse z i j \<in> \<R>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_translate_adverse: "\<exists>f\<in>\<R>\<^sup>2.\<forall>i j. \<phi> (the (f i j)) = adverse z i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
obtain r where r: "recfn 3 r" "total r" "(\<lambda>i j x. eval r [i, j, x]) = adverse z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>recfn 3 r; Partial_Recursive.total r; (\<lambda>i j x. eval r [i, j, x]) = local.adverse z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using adverse_in_R3
[PROOF STATE]
proof (prove)
using this:
\<exists>r. recfn 3 r \<and> Partial_Recursive.total r \<and> (\<lambda>i j x. eval r [i, j, x]) = local.adverse ?z

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>recfn 3 r; Partial_Recursive.total r; (\<lambda>i j x. eval r [i, j, x]) = local.adverse z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
recfn 3 r
Partial_Recursive.total r
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
let ?p = "encode r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
define rf where "rf = Cn 2 (r_smn 1 2) [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]"
[PROOF STATE]
proof (state)
this:
rf = Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r)), recf.Id 2 0, recf.Id 2 1]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rf = Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r)), recf.Id 2 0, recf.Id 2 1]
[PROOF STEP]
have "recfn 2 rf" and "total rf"
[PROOF STATE]
proof (prove)
using this:
rf = Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r)), recf.Id 2 0, recf.Id 2 1]

goal (1 subgoal):
 1. recfn 2 rf &&& Partial_Recursive.total rf
[PROOF STEP]
using Mn_free_imp_total
[PROOF STATE]
proof (prove)
using this:
rf = Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r)), recf.Id 2 0, recf.Id 2 1]
\<lbrakk>wellf ?f; Mn_free ?f\<rbrakk> \<Longrightarrow> Partial_Recursive.total ?f

goal (1 subgoal):
 1. recfn 2 rf &&& Partial_Recursive.total rf
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
recfn 2 rf
Partial_Recursive.total rf

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
define f where "f \<equiv> \<lambda>i j. eval rf [i, j]"
[PROOF STATE]
proof (state)
this:
f \<equiv> \<lambda>i j. eval rf [i, j]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
with \<open>recfn 2 rf\<close> \<open>total rf\<close>
[PROOF STATE]
proof (chain)
picking this:
recfn 2 rf
Partial_Recursive.total rf
f \<equiv> \<lambda>i j. eval rf [i, j]
[PROOF STEP]
have "f \<in> \<R>\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
recfn 2 rf
Partial_Recursive.total rf
f \<equiv> \<lambda>i j. eval rf [i, j]

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

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have rf: "eval rf [i, j] = eval (r_smn 1 2) [?p, i, j]" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval rf [i, j] = eval (r_smn 1 2) [encode r, i, j]
[PROOF STEP]
unfolding rf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r)), recf.Id 2 0, recf.Id 2 1]) [i, j] = eval (r_smn 1 2) [encode r, i, j]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval rf [?i, ?j] = eval (r_smn 1 2) [encode r, ?i, ?j]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
eval rf [?i, ?j] = eval (r_smn 1 2) [encode r, ?i, ?j]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
fix i j x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have "\<phi> (the (f i j)) x = eval r_phi [the (f i j), x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (the (f i j)) x = eval r_phi [the (f i j), x]
[PROOF STEP]
using phi_def
[PROOF STATE]
proof (prove)
using this:
\<phi> ?i ?x \<equiv> eval r_phi [?i, ?x]

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

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> (the (f i j)) x = eval r_phi [the (f i j), x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have "... = eval r_phi [the (eval rf [i, j]), x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_phi [the (f i j), x] = eval r_phi [the (eval rf [i, j]), x]
[PROOF STEP]
using f_def
[PROOF STATE]
proof (prove)
using this:
f \<equiv> \<lambda>i j. eval rf [i, j]

goal (1 subgoal):
 1. eval r_phi [the (f i j), x] = eval r_phi [the (eval rf [i, j]), x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_phi [the (f i j), x] = eval r_phi [the (eval rf [i, j]), x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval r_phi [the (f i j), x] = eval r_phi [the (eval rf [i, j]), x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have "... = eval (r_universal 1) [the (eval (r_smn 1 2) [?p, i, j]), x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_phi [the (eval rf [i, j]), x] = eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x]
[PROOF STEP]
using rf r_phi_def
[PROOF STATE]
proof (prove)
using this:
eval rf [?i, ?j] = eval (r_smn 1 2) [encode r, ?i, ?j]
r_phi \<equiv> r_universal 1

goal (1 subgoal):
 1. eval r_phi [the (eval rf [i, j]), x] = eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_phi [the (eval rf [i, j]), x] = eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval r_phi [the (eval rf [i, j]), x] = eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have "... = eval (r_universal (2 + 1)) (?p # [i, j] @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x] = eval (r_universal (2 + 1)) (encode r # [i, j] @ [x])
[PROOF STEP]
using smn_lemma[of 1 "[i, j]" 2 "[x]"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < 1; length [i, j] = 2; length [x] = 1\<rbrakk> \<Longrightarrow> eval (r_universal (2 + 1)) (?p # [i, j] @ [x]) = eval (r_universal 1) [the (eval (r_smn 1 2) [?p, i, j]), x]

goal (1 subgoal):
 1. eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x] = eval (r_universal (2 + 1)) (encode r # [i, j] @ [x])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x] = eval (r_universal (2 + 1)) (encode r # [i, j] @ [x])

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval (r_universal 1) [the (eval (r_smn 1 2) [encode r, i, j]), x] = eval (r_universal (2 + 1)) (encode r # [i, j] @ [x])

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have "... = eval (r_universal 3) [?p, i, j, x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (r_universal (2 + 1)) (encode r # [i, j] @ [x]) = eval (r_universal 3) [encode r, i, j, x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (r_universal (2 + 1)) (encode r # [i, j] @ [x]) = eval (r_universal 3) [encode r, i, j, x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval (r_universal (2 + 1)) (encode r # [i, j] @ [x]) = eval (r_universal 3) [encode r, i, j, x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have "... = eval r [i, j, x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (r_universal 3) [encode r, i, j, x] = eval r [i, j, x]
[PROOF STEP]
using r_universal r
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>recfn ?n ?f; length ?xs = ?n\<rbrakk> \<Longrightarrow> eval (r_universal ?n) (encode ?f # ?xs) = eval ?f ?xs
recfn 3 r
Partial_Recursive.total r
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z

goal (1 subgoal):
 1. eval (r_universal 3) [encode r, i, j, x] = eval r [i, j, x]
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
eval (r_universal 3) [encode r, i, j, x] = eval r [i, j, x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval (r_universal 3) [encode r, i, j, x] = eval r [i, j, x]

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
have "... = adverse z i j x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r [i, j, x] = local.adverse z i j x
[PROOF STEP]
using r(3)
[PROOF STATE]
proof (prove)
using this:
(\<lambda>i j x. eval r [i, j, x]) = local.adverse z

goal (1 subgoal):
 1. eval r [i, j, x] = local.adverse z i j x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
eval r [i, j, x] = local.adverse z i j x

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (f i j)) x = local.adverse z i j x
[PROOF STEP]
have "\<phi> (the (f i j)) x = adverse z i j x"
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (f i j)) x = local.adverse z i j x

goal (1 subgoal):
 1. \<phi> (the (f i j)) x = local.adverse z i j x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<phi> (the (f i j)) x = local.adverse z i j x

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<phi> (the (f ?i2 ?j2)) ?x2 = local.adverse z ?i2 ?j2 ?x2

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
with \<open>f \<in> \<R>\<^sup>2\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> \<R>\<^sup>2
\<phi> (the (f ?i2 ?j2)) ?x2 = local.adverse z ?i2 ?j2 ?x2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in> \<R>\<^sup>2
\<phi> (the (f ?i2 ?j2)) ?x2 = local.adverse z ?i2 ?j2 ?x2

goal (1 subgoal):
 1. \<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse z i j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adverse_in_V01: "\<exists>m n. adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> adverse 1 m n \<in> V\<^sub>0\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
obtain f\<^sub>0 where f0: "f\<^sub>0 \<in> \<R>\<^sup>2" "\<forall>i j. \<phi> (the (f\<^sub>0 i j)) = adverse 0 i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f\<^sub>0. \<lbrakk>f\<^sub>0 \<in> \<R>\<^sup>2; \<forall>i j. \<phi> (the (f\<^sub>0 i j)) = local.adverse 0 i j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using phi_translate_adverse[of 0]
[PROOF STATE]
proof (prove)
using this:
\<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse 0 i j

goal (1 subgoal):
 1. (\<And>f\<^sub>0. \<lbrakk>f\<^sub>0 \<in> \<R>\<^sup>2; \<forall>i j. \<phi> (the (f\<^sub>0 i j)) = local.adverse 0 i j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f\<^sub>0 \<in> \<R>\<^sup>2
\<forall>i j. \<phi> (the (f\<^sub>0 i j)) = local.adverse 0 i j

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
obtain f\<^sub>1 where f1: "f\<^sub>1 \<in> \<R>\<^sup>2" "\<forall>i j. \<phi> (the (f\<^sub>1 i j)) = adverse 1 i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f\<^sub>1. \<lbrakk>f\<^sub>1 \<in> \<R>\<^sup>2; \<forall>i j. \<phi> (the (f\<^sub>1 i j)) = local.adverse 1 i j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using phi_translate_adverse[of 1]
[PROOF STATE]
proof (prove)
using this:
\<exists>f\<in>\<R>\<^sup>2. \<forall>i j. \<phi> (the (f i j)) = local.adverse 1 i j

goal (1 subgoal):
 1. (\<And>f\<^sub>1. \<lbrakk>f\<^sub>1 \<in> \<R>\<^sup>2; \<forall>i j. \<phi> (the (f\<^sub>1 i j)) = local.adverse 1 i j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f\<^sub>1 \<in> \<R>\<^sup>2
\<forall>i j. \<phi> (the (f\<^sub>1 i j)) = local.adverse 1 i j

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
obtain m n where "\<phi> m = \<phi> (the (f\<^sub>0 m n))" and "\<phi> n = \<phi> (the (f\<^sub>1 m n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>\<phi> m = \<phi> (the (f\<^sub>0 m n)); \<phi> n = \<phi> (the (f\<^sub>1 m n))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using smullyan_double_fixed_point[OF f0(1) f1(1)]
[PROOF STATE]
proof (prove)
using this:
(\<And>m n. \<lbrakk>\<phi> m = \<phi> (the (f\<^sub>0 m n)); \<phi> n = \<phi> (the (f\<^sub>1 m n))\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>\<phi> m = \<phi> (the (f\<^sub>0 m n)); \<phi> n = \<phi> (the (f\<^sub>1 m n))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> m = \<phi> (the (f\<^sub>0 m n))
\<phi> n = \<phi> (the (f\<^sub>1 m n))

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
with f0(2) f1(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>i j. \<phi> (the (f\<^sub>0 i j)) = local.adverse 0 i j
\<forall>i j. \<phi> (the (f\<^sub>1 i j)) = local.adverse 1 i j
\<phi> m = \<phi> (the (f\<^sub>0 m n))
\<phi> n = \<phi> (the (f\<^sub>1 m n))
[PROOF STEP]
have "\<phi> m = adverse 0 m n" and "\<phi> n = adverse 1 m n"
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. \<phi> (the (f\<^sub>0 i j)) = local.adverse 0 i j
\<forall>i j. \<phi> (the (f\<^sub>1 i j)) = local.adverse 1 i j
\<phi> m = \<phi> (the (f\<^sub>0 m n))
\<phi> n = \<phi> (the (f\<^sub>1 m n))

goal (1 subgoal):
 1. \<phi> m = local.adverse 0 m n &&& \<phi> n = local.adverse 1 m n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<phi> m = local.adverse 0 m n
\<phi> n = local.adverse 1 m n

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> m = local.adverse 0 m n
\<phi> n = local.adverse 1 m n

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
have "the (adverse 0 m n 0) = m" and "the (adverse 1 m n 1) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (local.adverse 0 m n 0) = m &&& the (local.adverse 1 m n 1) = n
[PROOF STEP]
using adverse_at_01
[PROOF STATE]
proof (prove)
using this:
local.adverse ?z ?i ?j 0 \<down>= ?i
local.adverse ?z ?i ?j 1 \<down>= ?j

goal (1 subgoal):
 1. the (local.adverse 0 m n 0) = m &&& the (local.adverse 1 m n 1) = n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
the (local.adverse 0 m n 0) = m
the (local.adverse 1 m n 1) = n

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> m = local.adverse 0 m n
\<phi> n = local.adverse 1 m n
the (local.adverse 0 m n 0) = m
the (local.adverse 1 m n 1) = n
[PROOF STEP]
have
    "\<phi> (the (adverse 0 m n 0)) = adverse 0 m n"
    "\<phi> (the (adverse 1 m n 1)) = adverse 1 m n"
[PROOF STATE]
proof (prove)
using this:
\<phi> m = local.adverse 0 m n
\<phi> n = local.adverse 1 m n
the (local.adverse 0 m n 0) = m
the (local.adverse 1 m n 1) = n

goal (1 subgoal):
 1. \<phi> (the (local.adverse 0 m n 0)) = local.adverse 0 m n &&& \<phi> (the (local.adverse 1 m n 1)) = local.adverse 1 m n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<phi> (the (local.adverse 0 m n 0)) = local.adverse 0 m n
\<phi> (the (local.adverse 1 m n 1)) = local.adverse 1 m n

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (the (local.adverse 0 m n 0)) = local.adverse 0 m n
\<phi> (the (local.adverse 1 m n 1)) = local.adverse 1 m n

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
have "adverse 0 m n \<in> \<R>" and "adverse 1 m n \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse 0 m n \<in> \<R> &&& local.adverse 1 m n \<in> \<R>
[PROOF STEP]
using adverse_in_R1
[PROOF STATE]
proof (prove)
using this:
local.adverse ?z ?i ?j \<in> \<R>

goal (1 subgoal):
 1. local.adverse 0 m n \<in> \<R> &&& local.adverse 1 m n \<in> \<R>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
local.adverse 0 m n \<in> \<R>
local.adverse 1 m n \<in> \<R>

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (the (local.adverse 0 m n 0)) = local.adverse 0 m n
\<phi> (the (local.adverse 1 m n 1)) = local.adverse 1 m n
local.adverse 0 m n \<in> \<R>
local.adverse 1 m n \<in> \<R>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (local.adverse 0 m n 0)) = local.adverse 0 m n
\<phi> (the (local.adverse 1 m n 1)) = local.adverse 1 m n
local.adverse 0 m n \<in> \<R>
local.adverse 1 m n \<in> \<R>

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
using V01_def
[PROOF STATE]
proof (prove)
using this:
\<phi> (the (local.adverse 0 m n 0)) = local.adverse 0 m n
\<phi> (the (local.adverse 1 m n 1)) = local.adverse 1 m n
local.adverse 0 m n \<in> \<R>
local.adverse 1 m n \<in> \<R>
V\<^sub>0\<^sub>1 = {f \<in> \<R>. \<phi> (the (f 0)) = f \<or> \<phi> (the (f 1)) = f}

goal (1 subgoal):
 1. \<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m n. local.adverse 0 m n \<in> V\<^sub>0\<^sub>1 \<and> local.adverse 1 m n \<in> V\<^sub>0\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adverse_Suc:
  assumes "x > 0"
  shows "adverse z i j (Suc x) \<down>=
    (if s (e_snoc ((adverse z i j) \<triangleright> x) 0) \<noteq> s ((adverse z i j) \<triangleright> x)
     then 0
     else if s (e_snoc ((adverse z i j) \<triangleright> x) 1) \<noteq> s ((adverse z i j) \<triangleright> x)
          then 1 else z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= (if s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) then 0 else if s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) then 1 else z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= (if s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) then 0 else if s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) then 1 else z)
[PROOF STEP]
have "adverse z i j (Suc x) \<down>=
    (if s (list_encode (prefixes z i j x @ [0])) \<noteq> s (list_encode (prefixes z i j x))
     then 0
     else if s (list_encode (prefixes z i j x @ [1])) \<noteq> s (list_encode (prefixes z i j x))
          then 1 else z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= (if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 1 else z)
[PROOF STEP]
using assms adverse_def
[PROOF STATE]
proof (prove)
using this:
0 < x
local.adverse ?z ?i ?j ?x \<equiv> Some (last (local.prefixes ?z ?i ?j ?x))

goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= (if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 1 else z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc x) \<down>= (if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 1 else z)

goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= (if s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) then 0 else if s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) then 1 else z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.adverse z i j (Suc x) \<down>= (if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 1 else z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.adverse z i j (Suc x) \<down>= (if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [0])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 0 else if s (Partial_Recursive.list_encode (local.prefixes z i j x @ [1])) \<noteq> s (Partial_Recursive.list_encode (local.prefixes z i j x)) then 1 else z)

goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= (if s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) then 0 else if s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) then 1 else z)
[PROOF STEP]
by (simp add: init_adverse_eq_prefixes)
[PROOF STATE]
proof (state)
this:
local.adverse z i j (Suc x) \<down>= (if s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) then 0 else if s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x) then 1 else z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adverse_Suc_not_hyp_change:
  assumes "x > 0" and "\<not> hyp_change z i j x"
  shows "adverse z i j (Suc x) \<down>= z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= z
[PROOF STEP]
using assms adverse_Suc
[PROOF STATE]
proof (prove)
using this:
0 < x
\<not> (s (e_snoc (local.adverse z i j \<triangleright> x) 0) \<noteq> s (local.adverse z i j \<triangleright> x) \<or> s (e_snoc (local.adverse z i j \<triangleright> x) 1) \<noteq> s (local.adverse z i j \<triangleright> x))
0 < ?x \<Longrightarrow> local.adverse ?z ?i ?j (Suc ?x) \<down>= (if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 0) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 0 else if s (e_snoc (local.adverse ?z ?i ?j \<triangleright> ?x) 1) \<noteq> s (local.adverse ?z ?i ?j \<triangleright> ?x) then 1 else ?z)

goal (1 subgoal):
 1. local.adverse z i j (Suc x) \<down>= z
[PROOF STEP]
by simp