[STATEMENT]
lemma wf_termi_call_steps: "wf termi_call_steps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf termi_call_steps
[PROOF STEP]
apply(unfold termi_call_steps_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))}
[PROOF STEP]
apply(simp only:wf_iff_no_infinite_down_chain)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>f. \<forall>i. (f (Suc i), f i) \<in> {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))}
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<forall>i. (f (Suc i), f i) \<in> {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))} \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac S)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<forall>i. (S (Suc i), S i) \<in> {((q, t), p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))} \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac
 "\<exists>Cs. Cs 0 = [] & (\<forall>i. (body(fst(S i)) # Cs i,snd(S i)) \<rightarrow>\<^sup>*
                        (CALL(fst(S(i+1)))# Cs(i+1), snd(S(i+1))))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
 2. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rule_tac x = "cseq S" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> cseq S 0 = [] \<and> (\<forall>i. (body (fst (S i)) # cseq S i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # cseq S (i + 1), snd (S (i + 1))))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i. \<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> (body (fst (S i)) # cseq S i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # (SOME cs. ([body (fst (S i))], snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # cs, snd (S (Suc i)))) @ cseq S i, snd (S (Suc i)))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule_tac x=i in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i) \<Longrightarrow> (body (fst (S i)) # cseq S i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # (SOME cs. ([body (fst (S i))], snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # cs, snd (S (Suc i)))) @ cseq S i, snd (S (Suc i)))
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i x y xa ya cs. \<lbrakk>S (Suc i) = (x, y); S i = (xa, ya); body xa \<down> ya; ([body xa], ya) \<rightarrow>\<^sup>* (CALL x # cs, y)\<rbrakk> \<Longrightarrow> (body xa # cseq S i, ya) \<rightarrow>\<^sup>* (CALL x # (SOME cs. ([body xa], ya) \<rightarrow>\<^sup>* (CALL x # cs, y)) @ cseq S i, y)
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac q t p s cs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i q t p s cs. \<lbrakk>S (Suc i) = (q, t); S i = (p, s); body p \<down> s; ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t)\<rbrakk> \<Longrightarrow> (body p # cseq S i, s) \<rightarrow>\<^sup>* (CALL q # (SOME cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t)) @ cseq S i, t)
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule_tac P = "\<lambda>cs.([body p],s) \<rightarrow>\<^sup>* (CALL q# cs, t)" in someI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S i q t p s cs x. \<lbrakk>S (Suc i) = (q, t); S i = (p, s); body p \<down> s; ([body p], s) \<rightarrow>\<^sup>* (CALL q # x, t)\<rbrakk> \<Longrightarrow> (body p # cseq S i, s) \<rightarrow>\<^sup>* (CALL q # x @ cseq S i, t)
 2. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(fastforce dest:app_execs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); \<exists>Cs. Cs 0 = [] \<and> (\<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac
 "\<forall>i. ((body(fst(S i))# Cs i,snd(S i)), (body(fst(S(i+1)))# Cs(i+1), snd(S(i+1)))) : exec1^+")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1)))\<rbrakk> \<Longrightarrow> \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1)))\<rbrakk> \<Longrightarrow> \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(blast intro:rtrancl_into_trancl1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "\<exists>f. f 0 = ([body(fst(S 0))],snd(S 0)) \<and> (\<forall>i. (f i, f(i+1)) : exec1^+)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f (0::?'a42) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + (1::?'a42))) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rule_tac x = "\<lambda>i.(body(fst(S i))#Cs i,snd(S i))" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> (body (fst (S 0)) # Cs 0, snd (S 0)) = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+)
 2. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>\<forall>i. (case S (Suc i) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S i); Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule_tac x=0 in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (i + 1))) # Cs (i + 1), snd (S (i + 1))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+); (case S (Suc 0) of (q, t) \<Rightarrow> \<lambda>(p, s). body p \<down> s \<and> (\<exists>cs. ([body p], s) \<rightarrow>\<^sup>* (CALL q # cs, t))) (S 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; \<exists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+); body (fst (S 0)) \<down> snd (S 0) \<and> (\<exists>cs. ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs f cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; body (fst (S 0)) \<down> snd (S 0); ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))); f 0 = ([body (fst (S 0))], snd (S 0)); \<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule termi_impl_no_inf_chain)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs f cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))); f 0 = ([body (fst (S 0))], snd (S 0)); \<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+; \<nexists>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<and> (\<forall>i. (f i, f (i + 1)) \<in> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S Cs f cs. \<lbrakk>Cs 0 = []; \<forall>i. (body (fst (S i)) # Cs i, snd (S i)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))); \<forall>i. ((body (fst (S i)) # Cs i, snd (S i)), body (fst (S (Suc i))) # Cs (Suc i), snd (S (Suc i))) \<in> exec1\<^sup>+; ([body (fst (S 0))], snd (S 0)) \<rightarrow>\<^sup>* (CALL (fst (S (Suc 0))) # cs, snd (S (Suc 0))); f 0 = ([body (fst (S 0))], snd (S 0)); \<forall>i. (f i, f (Suc i)) \<in> exec1\<^sup>+; \<forall>f. f 0 = ([body (fst (S 0))], snd (S 0)) \<longrightarrow> (\<exists>i. (f i, f (Suc i)) \<notin> exec1\<^sup>+)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done