theory GraphRefine

lemma graph_fun_refines_from_simpl_to_graph_with_refine:
  "\<lbrakk> SGamma proc = Some com; GGamma fname = Some gf;
    simple_simpl_refines SGamma com' com;
    \<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0
        [Q] UNIV I eqs
        (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs);
        eq_impl (NextNode (entry_point gf))
          (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins)
          eqs I;
        distinct (function_inputs gf); length ins = length (function_inputs gf);
        length outs = length (function_outputs gf) \<rbrakk>
    \<Longrightarrow> graph_fun_refines SGamma GGamma I ins proc outs fname" apply (clarsimp simp: graph_fun_refines_def) apply (frule exec_trace_def[THEN eqset_imp_iff, THEN iffD1]) apply clarsimp apply (erule_tac x="UNIV \<times> {[0 \<mapsto> (com', Normal s)]}" in meta_allE) apply (drule_tac tr=tr and tr'="[0 \<mapsto> (com', Normal s)]"
          and n'=0 and n''=0 and sst=s in simpl_to_graphD) apply (rule conjI, assumption) apply (simp add: suffix_tuple_closure_inter_def exec_trace_def) apply (rule conjI) apply (erule eq_implD) apply (simp add: fetch_returned exec_trace_inputs_def acc_vars_def) apply simp apply (simp add: add_cont_Nil nat_trace_rel_def) apply (clarsimp simp: trace_end_match_def dest!: fun_cong[where x=0]) apply (subgoal_tac "\<forall>st. trace_end tr'' = Some st
    \<longrightarrow> SGamma \<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st") apply (elim disjE exE conjE) apply (clarsimp simp: exec_final_step_def) apply clarsimp apply (drule step_preserves_termination[rotated]) apply (erule step.Call) apply (drule simple_simpl_refines_no_fault_terminatesD) apply (blast intro: exec.Call) apply (simp add: c_trace_nontermination simple_simpl_refines_def) apply (frule(1) trace_end_Ret_Err) apply (clarsimp simp: exec_final_step_def acc_vars_def) apply metis apply clarsimp apply (rule exec.Call, assumption) apply (erule simple_simpl_refines_no_fault_execD[rotated]) apply (blast intro: exec.Call) apply (simp add: exec_via_trace) apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; \<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0 [Q] UNIV I eqs (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs); eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf)\<rbrakk> \<Longrightarrow> graph_fun_refines SGamma GGamma I ins proc outs fname proof (prove)
goal (1 subgoal):
 1. \<And>tr s. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; \<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0 [Q] UNIV I eqs (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs); eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (1 subgoal):
 1. \<And>tr s. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; \<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0 [Q] UNIV I eqs (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs); eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> {trace. \<exists>gf. GGamma fname = Some gf \<and> (\<exists>st. trace 0 = Some [(NextNode (entry_point gf), st, fname)]) \<and> trace \<in> nat_trace_rel continuing (exec_graph_step GGamma)}\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (1 subgoal):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; \<And>Q. simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0 [Q] UNIV I eqs (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs); eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (1 subgoal):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; simpl_to_graph SGamma GGamma fname (NextNode (entry_point gf)) (add_cont com' []) 0 [UNIV \<times> {[0 \<mapsto> (com', Normal s)]}] UNIV I eqs (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs)\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (2 subgoals):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> tr 0 = Some [(NextNode (entry_point gf), ?gst14 tr s st, ?gf'14 tr s st)] \<and> s \<in> UNIV \<and> s \<in> I \<and> eqs (?gst14 tr s st) s \<and> 0 \<le> 0 \<and> 0 \<le> 0 \<and> tr \<in> exec_trace GGamma fname \<and> (tr, [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub>) \<in> suffix_tuple_closure_inter (set [UNIV \<times> {[0 \<mapsto> (com', Normal s)]}]) \<and> [0 \<mapsto> (com', Normal s)] \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> [0 \<mapsto> (com', Normal s)] 0 = Some (add_cont com' [], Normal s)
 2. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (2 subgoals):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> s \<in> UNIV \<and> s \<in> I \<and> eqs st s \<and> 0 \<le> 0 \<and> 0 \<le> 0 \<and> tr \<in> exec_trace GGamma fname \<and> (tr, [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub>) \<in> suffix_tuple_closure_inter (set [UNIV \<times> {[0 \<mapsto> (com', Normal s)]}]) \<and> [0 \<mapsto> (com', Normal s)] \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> [0 \<mapsto> (com', Normal s)] 0 = Some (add_cont com' [], Normal s)
 2. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (2 subgoals):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> eqs st s \<and> [0 \<mapsto> (com', Normal s)] \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> com' = add_cont com' []
 2. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (3 subgoals):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> eqs st s
 2. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> [0 \<mapsto> (com', Normal s)] \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> com' = add_cont com' []
 3. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (4 subgoals):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> map (\<lambda>i. var_acc i st) (function_inputs gf) = map (\<lambda>i. i s) ins
 2. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> s \<in> I
 3. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> [0 \<mapsto> (com', Normal s)] \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> com' = add_cont com' []
 4. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (3 subgoals):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> s \<in> I
 2. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> [0 \<mapsto> (com', Normal s)] \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> com' = add_cont com' []
 3. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (2 subgoals):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]\<rbrakk> \<Longrightarrow> [0 \<mapsto> (com', Normal s)] \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> com' = add_cont com' []
 2. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (1 subgoal):
 1. \<And>tr s st. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..0}\<^esub> = [0 \<mapsto> (com', Normal s)]|\<^bsub>{..0}\<^esub> \<and> trace_end_match (\<lambda>s s'. map (\<lambda>i. var_acc i s) (function_outputs gf) = map (\<lambda>i. i s') outs) I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (1 subgoal):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s proof (prove)
goal (2 subgoals):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 2. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (4 subgoals):
 1. \<And>tr s st tr'' ft. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr'' = Some (SKIP, Fault ft)\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 2. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = None; trace_end tr'' = None\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 3. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 4. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (3 subgoals):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = None; trace_end tr'' = None\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 2. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 3. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (3 subgoals):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); trace_end tr = None; trace_end tr'' = None; SGamma\<turnstile>com.Call proc \<down> Normal s\<rbrakk> \<Longrightarrow> False
 2. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 3. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (4 subgoals):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); trace_end tr = None; trace_end tr'' = None\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (com.Call proc, Normal s) \<rightarrow> (?c'43 tr s st tr'', ?s'43 tr s st tr'')
 2. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); trace_end tr = None; trace_end tr'' = None; SGamma\<turnstile>?c'43 tr s st tr'' \<down> ?s'43 tr s st tr''\<rbrakk> \<Longrightarrow> False
 3. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 4. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (3 subgoals):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); trace_end tr = None; trace_end tr'' = None; SGamma\<turnstile>com \<down> Normal s\<rbrakk> \<Longrightarrow> False
 2. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 3. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (4 subgoals):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); trace_end tr = None; trace_end tr'' = None; SGamma\<turnstile>com \<down> Normal s\<rbrakk> \<Longrightarrow> \<forall>ft. \<not> SGamma\<turnstile> \<langle>com,Normal (?s47 tr s st tr'')\<rangle> \<Rightarrow> Fault ft
 2. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); trace_end tr = None; trace_end tr'' = None; SGamma\<turnstile>com \<down> Normal s; \<not> SGamma\<turnstile>com' \<down> Normal (?s47 tr s st tr'') \<longrightarrow> \<not> SGamma\<turnstile>com \<down> Normal (?s47 tr s st tr'')\<rbrakk> \<Longrightarrow> False
 3. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 4. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (3 subgoals):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); trace_end tr = None; trace_end tr'' = None; SGamma\<turnstile>com \<down> Normal s; \<not> SGamma\<turnstile>com' \<down> Normal s \<longrightarrow> \<not> SGamma\<turnstile>com \<down> Normal s\<rbrakk> \<Longrightarrow> False
 2. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 3. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (2 subgoals):
 1. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 2. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (2 subgoals):
 1. \<And>tr s st tr'' sst' gst' gf'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st; trace_end tr = Some [(Ret, gst', gf')]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I; \<exists>gst er. [(Ret, gst', gf')] = [(er, gst, fname)] \<and> er \<in> {Ret, Err}\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s
 2. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (2 subgoals):
 1. \<And>tr s st tr'' sst' gst'. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>sst. sst \<in> I \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> (\<exists>x\<in>set outs. x sst \<noteq> x sst'); tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; tr'' 0 = Some (com', Normal s); SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst'; trace_end tr = Some [(Ret, gst', fname)]; trace_end tr'' = Some (SKIP, Normal sst'); map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs; sst' \<in> I\<rbrakk> \<Longrightarrow> False
 2. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (1 subgoal):
 1. \<And>tr s st tr''. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; (\<exists>ft. trace_end tr'' = Some (SKIP, Fault ft)) \<or> trace_end tr = None \<and> trace_end tr'' = None \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> trace_end tr'' = Some (SKIP, Normal sst') \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s)\<rbrakk> \<Longrightarrow> \<forall>st. trace_end tr'' = Some st \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step st proof (prove)
goal (1 subgoal):
 1. \<And>tr s st tr'' a b. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; a = SKIP \<and> (\<exists>ft. b = Fault ft) \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> a = SKIP \<and> b = Normal sst' \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s); trace_end tr'' = Some (a, b)\<rbrakk> \<Longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>tr s st tr'' a b. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; simple_simpl_refines SGamma com' com; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; a = SKIP \<and> (\<exists>ft. b = Fault ft) \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> a = SKIP \<and> b = Normal sst' \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s); trace_end tr'' = Some (a, b)\<rbrakk> \<Longrightarrow> SGamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>tr s st tr'' a b. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; a = SKIP \<and> (\<exists>ft. b = Fault ft) \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> a = SKIP \<and> b = Normal sst' \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s); trace_end tr'' = Some (a, b)\<rbrakk> \<Longrightarrow> \<forall>ft. \<not> SGamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> Fault ft
 2. \<And>tr s st tr'' a b. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; a = SKIP \<and> (\<exists>ft. b = Fault ft) \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> a = SKIP \<and> b = Normal sst' \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s); trace_end tr'' = Some (a, b)\<rbrakk> \<Longrightarrow> SGamma\<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>tr s st tr'' a b. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<not> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; a = SKIP \<and> (\<exists>ft. b = Fault ft) \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> a = SKIP \<and> b = Normal sst' \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s); trace_end tr'' = Some (a, b)\<rbrakk> \<Longrightarrow> SGamma\<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>tr s st tr'' a b. \<lbrakk>SGamma proc = Some com; GGamma fname = Some gf; eq_impl (NextNode (entry_point gf)) (\<lambda>gst sst. map (\<lambda>i. var_acc i gst) (function_inputs gf) = map (\<lambda>i. i sst) ins) eqs I; distinct (function_inputs gf); length ins = length (function_inputs gf); length outs = length (function_outputs gf); tr \<in> exec_trace GGamma fname; map (\<lambda>i. i s) ins = exec_trace_inputs gf tr; s \<in> I; \<forall>ft. \<forall>tr\<in>c_trace SGamma. tr 0 = Some (com.Call proc, Normal s) \<longrightarrow> (\<forall>a b. trace_end tr = Some (a, b) \<longrightarrow> exec_final_step (a, b) \<noteq> Fault ft); \<forall>gst sst. sst \<in> I \<longrightarrow> trace_end tr = Some [(Ret, gst, fname)] \<longrightarrow> (\<exists>tr\<in>c_trace SGamma. tr 0 = Some (com.Call proc, Normal s) \<and> (\<exists>a b. trace_end tr = Some (a, b) \<and> exec_final_step (a, b) = Normal sst)) \<longrightarrow> map (\<lambda>j. j sst) outs \<noteq> acc_vars (function_outputs gf) gst; tr \<in> nat_trace_rel continuing (exec_graph_step GGamma); tr 0 = Some [(NextNode (entry_point gf), st, fname)]; tr'' \<in> c_trace SGamma; a = SKIP \<and> (\<exists>ft. b = Fault ft) \<or> (\<exists>sst' gst'. (\<exists>gf'. trace_end tr = Some [(Ret, gst', gf')]) \<and> a = SKIP \<and> b = Normal sst' \<and> map (\<lambda>i. var_acc i gst') (function_outputs gf) = map (\<lambda>i. i sst') outs \<and> sst' \<in> I); tr'' 0 = Some (com', Normal s); trace_end tr'' = Some (a, b)\<rbrakk> \<Longrightarrow> \<exists>tr\<in>c_trace SGamma. tr 0 = Some (com', Normal s) \<and> (\<exists>aa ba. trace_end tr = Some (aa, ba) \<and> exec_final_step (aa, ba) = exec_final_step (a, b)) proof (prove)
goal:
No subgoals!