[STATEMENT]
lemma Minr_lemma: "
  \<lbrakk>primerec rf (Suc (length xs))\<rbrakk> 
     \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = 
            Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
let ?rf = "(Cn (Suc (Suc (length xs))) 
    rec_not [Cn (Suc (Suc (length xs))) rf 
    (get_fstn_args (Suc (Suc (length xs))) (length xs) @ 
                [recf.id (Suc (Suc (length xs))) 
    (Suc ((length xs)))])])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
let ?rq = "(rec_all ?rt ?rf)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
assume h: "primerec rf (Suc (length xs))"
[PROOF STATE]
proof (state)
this:
primerec rf (Suc (length xs))

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
have h1: "primerec ?rq (Suc (length xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))
[PROOF STEP]
apply(rule_tac primerec_all_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. primerec (recf.id (Suc (length xs)) (length xs)) (Suc (length xs))
 2. primerec (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])]) (Suc (Suc (length xs)))
 3. 0 < Suc (length xs)
[PROOF STEP]
apply(auto simp: h nth_append)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
have "arity rf = Suc (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arity rf = Suc (length xs)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
primerec rf (Suc (length xs))

goal (1 subgoal):
 1. arity rf = Suc (length xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arity rf = Suc (length xs)

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))
arity rf = Suc (length xs)
[PROOF STEP]
show "rec_exec (rec_Minr rf) (xs @ [w]) = 
    Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
[PROOF STATE]
proof (prove)
using this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))
arity rf = Suc (length xs)

goal (1 subgoal):
 1. rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
apply(simp add: arity.simps Let_def sigma_lemma all_lemma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs)); arity rf = Suc (length xs)\<rbrakk> \<Longrightarrow> UF.Sigma (rec_exec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])]))) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
apply(rule_tac  sigma_minr_lemma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs)); arity rf = Suc (length xs)\<rbrakk> \<Longrightarrow> primerec rf (Suc (length xs))
[PROOF STEP]
apply(simp add: h)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w

goal:
No subgoals!
[PROOF STEP]
qed