theory GraphRefine

lemma simpl_to_graph_call_next_step:
  assumes graph: "nn = NextNode m" "GGamma p = Some gfc"
      "function_graph gfc m = Some (node.Call nn' p' args rets)"
  assumes next_step: "eq_impl nn eqs_inner (\<lambda>gst' sst'.
        ((exec_graph_step GGamma) ^^ steps) `` {[(nn', gst', p)]} \<subseteq> {[(nn'', f gst', p)]}
        \<and> (\<forall>k < steps. \<forall>st'. ([(nn', gst', p)], st') \<in> exec_graph_step GGamma ^^ k
        \<longrightarrow> continuing st')) I"
  and rel: "graph_fun_refines SGamma GGamma I inputs proc outputs p'"
  and modifies: "(\<forall>\<sigma>. SGamma \<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} com.Call proc (Q \<sigma>)) \<or> (Q = (\<lambda>_. UNIV))"
  and init: "eq_impl nn eqs (\<lambda>gst sst. initf sst \<in> I
            \<and> map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs) (I \<inter> P)"
  and ret: "eq_impl nn eqs (\<lambda>gst sst. (\<forall>sst' vs. map (\<lambda>i. i sst') outputs = vs
                  \<and> sst' \<in> I \<and> sst' \<in> Q (initf sst)
        \<longrightarrow> eqs2 (f (save_vals rets vs gst))
                (f' sst sst' (ret sst sst')) \<and> f' sst sst' (ret sst sst') \<in> I
            \<and> eqs_inner (save_vals rets vs gst) (f' sst sst' (ret sst sst')))) I"
  and cont: "simpl_to_graph SGamma GGamma p nn'' (add_cont com.Skip con) n tS UNIV I eqs2 out_eqs"
  shows "simpl_to_graph SGamma GGamma p nn
        (add_cont (call initf proc ret (\<lambda>x y. com.Basic (f' x y))) con)
        n tS P I eqs out_eqs" apply (rule simpl_to_graph_name_simpl_state) apply (clarsimp simp: call_def block_def block_exn_def graph) apply (rule_tac i=0 and j=3 and P'="{initf sst}"
        and inp_eqs'="\<lambda>gst _. eqs gst sst \<and> sst \<in> I" in simpl_to_graph_step_general) apply (simp add: init[THEN eq_implD] numeral_3_eq_3 eq_OO) apply (rule conjI[OF _ refl]) apply (intro relcomppI) apply (rule add_cont_step, rule step.DynCom) apply (simp add: add_cont_Cons[symmetric]) apply (rule add_cont_step, rule step.Basic) apply (simp add: add_cont_Cons(1), rule add_cont_step, rule step.SeqSkip) apply simp apply (clarsimp intro!: simpl_to_graphI) apply (frule init[THEN eq_implD], simp+) apply (cut_tac rel, clarsimp simp: graph_fun_refines_def) apply (frule exec_trace_drop_n, (rule graph | assumption)+) apply (drule(1) bspec) apply (drule_tac x="initf sst" in spec) apply (clarsimp simp: exec_trace_inputs_def graph) apply (subst(asm) trace_drop_n_init, (assumption | rule graph)+) apply (clarsimp simp: init_vars_def fetch_returned) apply (elim disjE exE conjE) apply (frule(1) c_trace_may_extend_steps) apply (rule rtranclp_trans) apply (rule add_cont_steps) apply (erule exec_impl_steps_Fault) apply (rule steps_Fault) apply assumption apply (clarsimp simp: c_trace_def) apply (rule exI, rule context_conjI) apply (erule(1) nat_trace_rel_final, fastforce simp: final_def) apply (simp add: trace_end_cut trace_end_match_def) apply (frule(2) trace_end_trace_drop_n_None) apply (frule(2) nontermination_to_c_trace) apply (auto simp: trace_end_match_def)[1] apply (frule trace_drop_n_end, (assumption | rule graph)+) apply (frule(1) c_trace_may_extend_steps) apply (rule rtranclp_trans) apply (rule add_cont_steps) apply (erule exec_impl_steps_Normal) apply (simp add: add_cont_Cons) apply (rule add_cont_steps) apply (rule exec_impl_steps_Normal) apply (rule exec.CatchMiss exec.Seq exec.Skip exec.DynCom exec.Basic | simp)+ apply clarsimp apply (frule ret[THEN eq_implD], simp, clarsimp) apply (drule_tac x=ssta in spec, drule mp, rule conjI, assumption) apply (rule disjE[OF modifies]) apply (drule spec, drule cvalidD[OF hoare_sound], simp+) apply clarsimp apply auto[1] apply simp apply clarsimp apply (frule next_step[THEN eq_implD], simp) apply (clarsimp simp: return_vars_def) apply (frule(3) exec_graph_trace_must_take_steps) apply (cut_tac tr=tr and tr'=trace' and n''="n'' + ja"
      and sst="f' a b c" for a b c in simpl_to_graphD[OF cont]) apply auto[1] apply (metis restrict_map_eq_mono[OF le_add1]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma p nn (add_cont (call initf proc ret (\<lambda>x y. com.Basic (f' x y))) con) n tS P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p nn (add_cont (call initf proc ret (\<lambda>x y. com.Basic (f' x y))) con) n tS {sst} I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (add_cont (DynCom (\<lambda>s. TRY
  com.Basic initf;;
com.Call proc
CATCH com.Basic (ret s);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret s);;
com.Basic (f' s t)))) con) n tS {sst} I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta \<in> {sst}; ssta \<in> I; eqs gst ssta\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 3) (add_cont (DynCom (\<lambda>s. TRY
  com.Basic initf;;
com.Call proc
CATCH com.Basic (ret s);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret s);;
com.Basic (f' s t)))) con, Normal ssta) (?com'2 sst, Normal sst') \<and> (exec_graph_step GGamma ^^ 0) `` {[(NextNode m, gst, p)]} \<subseteq> {[(?nn'2 sst, gst', p)]} \<and> (\<forall>k<0. \<forall>st'. ([(NextNode m, gst, p)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st') \<and> sst' \<in> {initf sst} \<and> sst' \<in> I \<and> eqs gst' sst \<and> sst \<in> I
 2. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (?nn'2 sst) (?com'2 sst) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> ((step SGamma OO step SGamma) OO step SGamma) (add_cont (DynCom (\<lambda>s. TRY
  com.Basic initf;;
com.Call proc
CATCH com.Basic (ret s);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret s);;
com.Basic (f' s t)))) con, Normal sst) (?com'2 sst, Normal (initf sst)) \<and> NextNode m = ?nn'2 sst
 2. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (?nn'2 sst) (?com'2 sst) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> ((step SGamma OO step SGamma) OO step SGamma) (add_cont (DynCom (\<lambda>s. TRY
  com.Basic initf;;
com.Call proc
CATCH com.Basic (ret s);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret s);;
com.Basic (f' s t)))) con, Normal sst) (?com'2 sst, Normal (initf sst))
 2. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (?com'2 sst) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (4 subgoals):
 1. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (DynCom (\<lambda>s. TRY
  com.Basic initf;;
com.Call proc
CATCH com.Basic (ret s);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret s);;
com.Basic (f' s t)))) con, Normal sst) \<rightarrow> ?b13 sst ssta gst
 2. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> ?b13 sst ssta gst \<rightarrow> ?b12 sst ssta gst
 3. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> ?b12 sst ssta gst \<rightarrow> (?com'2 sst, Normal (initf sst))
 4. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (?com'2 sst) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (3 subgoals):
 1. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (TRY
  com.Basic initf;;
com.Call proc
CATCH com.Basic (ret sst);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) con, Normal sst) \<rightarrow> ?b12 sst ssta gst
 2. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> ?b12 sst ssta gst \<rightarrow> (?com'2 sst, Normal (initf sst))
 3. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (?com'2 sst) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (3 subgoals):
 1. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (com.Basic initf) (Inl (com.Call proc) # Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal sst) \<rightarrow> ?b12 sst sst gst
 2. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> ?b12 sst ssta gst \<rightarrow> (?com'2 sst, Normal (initf sst))
 3. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (?com'2 sst) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst ssta gst. \<lbrakk>sst \<in> P; ssta = sst; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont SKIP (Inl (com.Call proc) # Inr (com.Basic (ret ssta);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret ssta);;
com.Basic (f' ssta t))) # con), Normal (initf ssta)) \<rightarrow> (?com'2 sst, Normal (initf sst))
 2. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (?com'2 sst) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con)) (n + min 0 3) tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma p (NextNode m) (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con)) n tS {initf sst} I (\<lambda>gst _. eqs gst sst \<and> sst \<in> I) out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n''. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; initf sst \<in> I; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n''. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I \<and> map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); \<forall>tr\<in>exec_trace GGamma p'. \<forall>s. map (\<lambda>i. i s) inputs = exec_trace_inputs gf tr \<and> s \<in> I \<longrightarrow> (\<exists>ft. SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft) \<or> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s \<or> (\<exists>gst sst. SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<and> trace_end tr = Some [(Ret, gst, p')] \<and> sst \<in> I \<and> map (\<lambda>j. j sst) outputs = acc_vars (function_outputs gf) gst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); \<forall>tr\<in>exec_trace GGamma p'. \<forall>s. map (\<lambda>i. i s) inputs = exec_trace_inputs gf tr \<and> s \<in> I \<longrightarrow> (\<exists>ft. SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft) \<or> trace_end tr = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s \<or> (\<exists>gst sst. SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<and> trace_end tr = Some [(Ret, gst, p')] \<and> sst \<in> I \<and> map (\<lambda>j. j sst) outputs = acc_vars (function_outputs gf) gst); trace_drop_n (Suc n') 1 tr \<in> exec_trace GGamma p'\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') 1 tr \<in> exec_trace GGamma p'; \<forall>s. map (\<lambda>i. i s) inputs = exec_trace_inputs gf (trace_drop_n (Suc n') 1 tr) \<and> s \<in> I \<longrightarrow> (\<exists>ft. SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Fault ft) \<or> trace_end (trace_drop_n (Suc n') 1 tr) = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal s \<or> (\<exists>gst sst. SGamma\<turnstile> \<langle>com.Call proc,Normal s\<rangle> \<Rightarrow> Normal sst \<and> trace_end (trace_drop_n (Suc n') 1 tr) = Some [(Ret, gst, p')] \<and> sst \<in> I \<and> map (\<lambda>j. j sst) outputs = acc_vars (function_outputs gf) gst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') 1 tr \<in> exec_trace GGamma p'; map (\<lambda>i. i (initf sst)) inputs = exec_trace_inputs gf (trace_drop_n (Suc n') 1 tr) \<and> initf sst \<in> I \<longrightarrow> (\<exists>ft. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft) \<or> trace_end (trace_drop_n (Suc n') 1 tr) = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst) \<or> (\<exists>gst ssta. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta \<and> trace_end (trace_drop_n (Suc n') 1 tr) = Some [(Ret, gst, p')] \<and> ssta \<in> I \<and> map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; map (\<lambda>i. i (initf sst)) inputs = (case trace_drop_n (Suc n') (Suc 0) tr 0 of Some [(nn, gst, xa)] \<Rightarrow> acc_vars (function_inputs gf) gst) \<longrightarrow> (\<exists>ft. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft) \<or> trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst) \<or> (\<exists>gst ssta. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta \<and> trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> ssta \<in> I \<and> map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; map (\<lambda>i. i (initf sst)) inputs = (case Some [(NextNode (entry_point gf), init_vars (function_inputs gf) args gst, p')] of Some [(nn, gst, xa)] \<Rightarrow> acc_vars (function_inputs gf) gst) \<longrightarrow> (\<exists>ft. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft) \<or> trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst) \<or> (\<exists>gst ssta. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta \<and> trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> ssta \<in> I \<and> map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (\<exists>ft. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft) \<or> trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None \<and> \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst) \<or> (\<exists>gst ssta. SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta \<and> trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> ssta \<in> I \<and> map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (5 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)) \<rightarrow>\<^sup>* (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft)
 2. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> (?y72 sst tr gst n' gf' tr' n'' gf ft, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)
 3. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y72 sst tr gst n' gf' tr' n'' gf ft, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 4. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 5. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (6 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)) \<rightarrow>\<^sup>* ?y77 sst tr gst n' gf' tr' n'' gf ft
 2. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> SGamma\<turnstile> ?y77 sst tr gst n' gf' tr' n'' gf ft \<rightarrow>\<^sup>* (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft)
 3. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> (?y72 sst tr gst n' gf' tr' n'' gf ft, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)
 4. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y72 sst tr gst n' gf' tr' n'' gf ft, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 5. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 6. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (6 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (com.Call proc, Normal (initf sst)) \<rightarrow>\<^sup>* (?com'80 sst tr gst n' gf' tr' n'' gf ft, ?xs'80 sst tr gst n' gf' tr' n'' gf ft)
 2. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (?com'80 sst tr gst n' gf' tr' n'' gf ft) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), ?xs'80 sst tr gst n' gf' tr' n'' gf ft) \<rightarrow>\<^sup>* (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft)
 3. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> (?y72 sst tr gst n' gf' tr' n'' gf ft, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)
 4. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y72 sst tr gst n' gf' tr' n'' gf ft, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 5. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 6. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (5 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont SKIP (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Fault ft) \<rightarrow>\<^sup>* (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft)
 2. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> (?y72 sst tr gst n' gf' tr' n'' gf ft, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)
 3. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'72 sst tr gst n' gf' tr' n'' gf ft, ?xst'72 sst tr gst n' gf' tr' n'' gf ft) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y72 sst tr gst n' gf' tr' n'' gf ft, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 4. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 5. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (4 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> (?y72 sst tr gst n' gf' tr' n'' gf ft, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)
 2. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (SKIP, Fault ft) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y72 sst tr gst n' gf' tr' n'' gf ft, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss72 sst tr gst n' gf' tr' n'' gf ft)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 3. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 4. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (SKIP, Fault ft) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set tS)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft j trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault ft); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set tS)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'} \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (4 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft j trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault ft); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set tS)\<rbrakk> \<Longrightarrow> ?tr''91 sst tr gst n' gf' tr' n'' gf ft j trace' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}
 2. \<And>sst tr gst n' gf' tr' n'' gf ft j trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault ft); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); ?tr''91 sst tr gst n' gf' tr' n'' gf ft j trace' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}\<rbrakk> \<Longrightarrow> ?tr''91 sst tr gst n' gf' tr' n'' gf ft j trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end (?tr''91 sst tr gst n' gf' tr' n'' gf ft j trace'))
 3. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 4. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf ft j trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Fault ft; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault ft); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); trace'|\<^bsub>{..n'' + j}\<^esub> \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}\<rbrakk> \<Longrightarrow> trace'|\<^bsub>{..n'' + j}\<^esub>|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end (trace'|\<^bsub>{..n'' + j}\<^esub>))
 2. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst); trace_end tr = None\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = None; \<not> SGamma\<turnstile>com.Call proc \<down> Normal (initf sst); trace_end tr = None; \<exists>tr'a. tr'a \<in> c_trace SGamma \<and> tr'a|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end tr'a = None\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)) \<rightarrow>\<^sup>* (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (4 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)) \<rightarrow>\<^sup>* ?y137 sst tr gst n' gf' tr' n'' gf gsta ssta
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> ?y137 sst tr gst n' gf' tr' n'' gf gsta ssta \<rightarrow>\<^sup>* (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 4. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (4 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (com.Call proc, Normal (initf sst)) \<rightarrow>\<^sup>* (?com'140 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xs'140 sst tr gst n' gf' tr' n'' gf gsta ssta)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (?com'140 sst tr gst n' gf' tr' n'' gf gsta ssta) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), ?xs'140 sst tr gst n' gf' tr' n'' gf gsta ssta) \<rightarrow>\<^sup>* (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 4. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont SKIP (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal ssta) \<rightarrow>\<^sup>* (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (TRY
  com.Call proc
CATCH com.Basic (ret sst);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) con, Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (TRY
  SKIP
CATCH com.Basic (ret sst);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) con, Normal ssta) \<rightarrow>\<^sup>* (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'132 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (TRY
  com.Call proc
CATCH com.Basic (ret sst);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) con, Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (TRY
  SKIP
CATCH com.Basic (ret sst);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t)), Normal ssta) \<rightarrow>\<^sup>* (?com'143 sst tr gst n' gf' tr' n'' gf gsta ssta, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (add_cont (?com'143 sst tr gst n' gf' tr' n'' gf gsta ssta) con, ?xst'132 sst tr gst n' gf' tr' n'' gf gsta ssta) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (TRY
  com.Call proc
CATCH com.Basic (ret sst);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) con, Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> \<langle>TRY
  SKIP
CATCH com.Basic (ret sst);;
THROW
END;;
DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t)),Normal ssta\<rangle> \<Rightarrow> Normal (?t145 sst tr gst n' gf' tr' n'' gf gsta ssta)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (add_cont SKIP con, Normal (?t145 sst tr gst n' gf' tr' n'' gf gsta ssta)) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y132 sst tr gst n' gf' tr' n'' gf gsta ssta, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss132 sst tr gst n' gf' tr' n'' gf gsta ssta)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; \<exists>j\<ge>2. tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set tS)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); \<forall>sst'. sst' \<in> I \<and> sst' \<in> Q (initf sst) \<longrightarrow> eqs2 (f (save_vals rets (map (\<lambda>i. i sst') outputs) gst)) (f' sst sst' (ret sst sst')) \<and> f' sst sst' (ret sst sst') \<in> I \<and> eqs_inner (save_vals rets (map (\<lambda>i. i sst') outputs) gst) (f' sst sst' (ret sst sst'))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS)\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (map (\<lambda>i. i ssta) outputs) gst)) (f' sst ssta (ret sst ssta)) \<and> f' sst ssta (ret sst ssta) \<in> I \<and> eqs_inner (save_vals rets (map (\<lambda>i. i ssta) outputs) gst) (f' sst ssta (ret sst ssta))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); \<forall>\<sigma>. SGamma\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} com.Call proc (Q \<sigma>)\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); Q = (\<lambda>_. UNIV)\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (map (\<lambda>i. i ssta) outputs) gst)) (f' sst ssta (ret sst ssta)) \<and> f' sst ssta (ret sst ssta) \<in> I \<and> eqs_inner (save_vals rets (map (\<lambda>i. i ssta) outputs) gst) (f' sst ssta (ret sst ssta))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (4 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS)\<rbrakk> \<Longrightarrow> Normal ssta \<notin> range Fault
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); Normal ssta \<in> Normal ` Q (initf sst) \<union> Abrupt ` {}\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); Q = (\<lambda>_. UNIV)\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 4. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (map (\<lambda>i. i ssta) outputs) gst)) (f' sst ssta (ret sst ssta)) \<and> f' sst ssta (ret sst ssta) \<in> I \<and> eqs_inner (save_vals rets (map (\<lambda>i. i ssta) outputs) gst) (f' sst ssta (ret sst ssta))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); Normal ssta \<in> Normal ` Q (initf sst) \<union> Abrupt ` {}\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); Q = (\<lambda>_. UNIV)\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 3. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (map (\<lambda>i. i ssta) outputs) gst)) (f' sst ssta (ret sst ssta)) \<and> f' sst ssta (ret sst ssta) \<in> I \<and> eqs_inner (save_vals rets (map (\<lambda>i. i ssta) outputs) gst) (f' sst ssta (ret sst ssta))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); Q = (\<lambda>_. UNIV)\<rbrakk> \<Longrightarrow> ssta \<in> Q (initf sst)
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (map (\<lambda>i. i ssta) outputs) gst)) (f' sst ssta (ret sst ssta)) \<and> f' sst ssta (ret sst ssta) \<in> I \<and> eqs_inner (save_vals rets (map (\<lambda>i. i ssta) outputs) gst) (f' sst ssta (ret sst ssta))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (map (\<lambda>i. i ssta) outputs) gst)) (f' sst ssta (ret sst ssta)) \<and> f' sst ssta (ret sst ssta) \<in> I \<and> eqs_inner (save_vals rets (map (\<lambda>i. i ssta) outputs) gst) (f' sst ssta (ret sst ssta))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (acc_vars (function_outputs gf) gsta) gst)) (f' sst ssta (ret sst ssta)); f' sst ssta (ret sst ssta) \<in> I; eqs_inner (save_vals rets (acc_vars (function_outputs gf) gsta) gst) (f' sst ssta (ret sst ssta))\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (acc_vars (function_outputs gf) gsta) gst)) (f' sst ssta (ret sst ssta)); f' sst ssta (ret sst ssta) \<in> I; eqs_inner (save_vals rets (acc_vars (function_outputs gf) gsta) gst) (f' sst ssta (ret sst ssta)); (exec_graph_step GGamma ^^ steps) `` {[(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]} \<subseteq> {[(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]} \<and> (\<forall>k<steps. \<forall>st'. ([(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st')\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (acc_vars (function_outputs gf) gsta) gst)) (f' sst ssta (ret sst ssta)); f' sst ssta (ret sst ssta) \<in> I; eqs_inner (save_vals rets (acc_vars (function_outputs gf) gsta) gst) (f' sst ssta (ret sst ssta)); (exec_graph_step GGamma ^^ steps) `` {[(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]} \<subseteq> {[(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]}; \<forall>k<steps. \<forall>st'. ([(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st'\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (acc_vars (function_outputs gf) gsta) gst)) (f' sst ssta (ret sst ssta)); f' sst ssta (ret sst ssta) \<in> I; eqs_inner (save_vals rets (acc_vars (function_outputs gf) gsta) gst) (f' sst ssta (ret sst ssta)); (exec_graph_step GGamma ^^ steps) `` {[(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]} \<subseteq> {[(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]}; \<forall>k<steps. \<forall>st'. ([(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st'; tr (n' + j + steps) = Some [(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (acc_vars (function_outputs gf) gsta) gst)) (f' sst ssta (ret sst ssta)); f' sst ssta (ret sst ssta) \<in> I; eqs_inner (save_vals rets (acc_vars (function_outputs gf) gsta) gst) (f' sst ssta (ret sst ssta)); (exec_graph_step GGamma ^^ steps) `` {[(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]} \<subseteq> {[(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]}; \<forall>k<steps. \<forall>st'. ([(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st'; tr (n' + j + steps) = Some [(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]\<rbrakk> \<Longrightarrow> tr (?n'212 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') = Some [(nn'', ?gst212 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace', ?gf'212 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace')] \<and> f' (?a216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?b216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?c216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') \<in> UNIV \<and> f' (?a216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?b216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?c216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') \<in> I \<and> eqs2 (?gst212 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (f' (?a216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?b216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?c216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace')) \<and> n \<le> ?n'212 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace' \<and> n \<le> n'' + ja \<and> tr \<in> exec_trace GGamma p \<and> (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS) \<and> trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' (?a216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?b216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace') (?c216 sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace')))
 2. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (acc_vars (function_outputs gf) gsta) gst)) (f' sst ssta (ret sst ssta)); f' sst ssta (ret sst ssta) \<in> I; eqs_inner (save_vals rets (acc_vars (function_outputs gf) gsta) gst) (f' sst ssta (ret sst ssta)); (exec_graph_step GGamma ^^ steps) `` {[(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]} \<subseteq> {[(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]}; \<forall>k<steps. \<forall>st'. ([(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st'; tr (n' + j + steps) = Some [(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n'' + ja}\<^esub> = trace'|\<^bsub>{..n'' + ja}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf gsta ssta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; sst \<in> I; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma p; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (add_cont (com.Call proc) (Inr (com.Basic (ret sst);;
THROW) # Inl (DynCom (\<lambda>t. com.Basic (ret sst);;
com.Basic (f' sst t))) # con), Normal (initf sst)); initf sst \<in> I; map (\<lambda>i. i gst) args = map (\<lambda>i. i (initf sst)) inputs; GGamma p' = Some gf; length (function_inputs gf) = length inputs; length (function_outputs gf) = length outputs; distinct (function_inputs gf); trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; SGamma\<turnstile> \<langle>com.Call proc,Normal (initf sst)\<rangle> \<Rightarrow> Normal ssta; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; ssta \<in> I; map (\<lambda>j. j ssta) outputs = acc_vars (function_outputs gf) gsta; 2 \<le> j; tr (n' + j) = Some [(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]; trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + ja) = Some (add_cont SKIP con, Normal (f' sst ssta (ret sst ssta))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); eqs2 (f (save_vals rets (acc_vars (function_outputs gf) gsta) gst)) (f' sst ssta (ret sst ssta)); f' sst ssta (ret sst ssta) \<in> I; eqs_inner (save_vals rets (acc_vars (function_outputs gf) gsta) gst) (f' sst ssta (ret sst ssta)); (exec_graph_step GGamma ^^ steps) `` {[(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)]} \<subseteq> {[(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]}; \<forall>k<steps. \<forall>st'. ([(nn', save_vals rets (acc_vars (function_outputs gf) gsta) gst, p)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st'; tr (n' + j + steps) = Some [(nn'', f (save_vals rets (acc_vars (function_outputs gf) gsta) gst), p)]; \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n'' + ja}\<^esub> = trace'|\<^bsub>{..n'' + ja}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal:
No subgoals!