theory GraphRefine

lemma simpl_to_graph_call_asm_fun:
  assumes graph: "nn = NextNode m" "GGamma p = Some gfc"
      "function_graph gfc m = Some (node.Call nn' p' args rets)"
  and rel: "asm_fun_refines specname ret enc len GGamma p'"
  and init: "eq_impl nn eqs (\<lambda>gst sst. sst \<in> I
            \<and> map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst)
                (asm_fetch (globals sst))
            \<and> length args = len) (I \<inter> P)"
  and ret: "eq_impl nn eqs (\<lambda>gst sst. (\<forall>m' v' (ms' :: 'a).
            gdata (asm_store gdata (m', ms') (globals sst)) = gdata (globals sst)
            \<and> (v', (m', ms')) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst))
            \<longrightarrow> eqs2 (save_vals rets (asm_rets_to_list ret enc v' (m', ms')) gst)
                 (asm_ret v' (globals_update (asm_store gdata (m', ms')) sst))
                \<and> asm_ret v' (globals_update (asm_store gdata (m', ms')) sst) \<in> I)) 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 (Spec (asm_spec (ti :: 'a itself) gdata vol specname asm_ret asm_args)) con)
        n tS P I eqs out_eqs" apply (rule simpl_to_graph_name_simpl_state) apply (clarsimp simp: graph intro!: simpl_to_graphI) apply (frule init[THEN eq_implD], simp+) apply (cut_tac rel, clarsimp simp: asm_fun_refines_def) apply (frule exec_trace_drop_n, (rule graph | assumption)+) apply (drule(1) bspec) apply (clarsimp simp: exec_trace_inputs_def graph) apply (subst(asm) trace_drop_n_init, (assumption | rule graph)+) apply (clarsimp simp: init_vars_def) apply (subst(asm) fetch_returned, simp_all) apply (drule arg_cong[where f=length])+ apply simp apply (simp add: asm_args_to_list_inj) apply (drule spec, drule mp, rule refl) apply clarsimp apply (frule trace_drop_n_end, (assumption | rule graph)+) apply clarsimp apply (frule(1) c_trace_may_extend_steps) apply (rule add_cont_steps) apply (rule exec_impl_steps_Normal) apply (rule exec.Spec) apply (simp add: asm_spec_def) apply (erule rev_bexI) apply simp apply simp apply clarsimp apply (frule ret[THEN eq_implD], simp) apply (cut_tac tr=tr and tr'=trace' and n''="n'' + ja"
      and sst="asm_ret a b" for a b in simpl_to_graphD[OF cont]) apply (auto simp: return_vars_def asm_store_eq)[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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con) n tS {sst} I eqs 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')]; sst \<in> I; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal 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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I \<and> map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)) \<and> length args = len\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; \<forall>tr\<in>exec_trace GGamma p'. \<forall>inp_vs a b. exec_trace_inputs gf tr = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end tr = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; \<forall>tr\<in>exec_trace GGamma p'. \<forall>inp_vs a b. exec_trace_inputs gf tr = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end tr = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba))); 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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') 1 tr \<in> exec_trace GGamma p'; \<forall>inp_vs a b. exec_trace_inputs gf (trace_drop_n (Suc n') 1 tr) = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') 1 tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<forall>inp_vs a b. (case trace_drop_n (Suc n') (Suc 0) tr 0 of Some [(nn, gst, x)] \<Rightarrow> acc_vars (function_inputs gf) gst) = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<forall>inp_vs a b. (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) = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<forall>inp_vs a b. acc_vars (function_inputs gf) (save_vals (function_inputs gf) (asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst))) default_state) = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'\<rbrakk> \<Longrightarrow> length args = length (asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)))
 2. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<forall>inp_vs a b. asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)) = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; length (map (\<lambda>i. i gst) args) = length (asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)))\<rbrakk> \<Longrightarrow> length args = length (asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)))
 2. \<And>sst tr gst n' gf' tr' n'' gf. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<forall>inp_vs a b. asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)) = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<forall>inp_vs a b. asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)) = asm_args_to_list enc inp_vs (a, b) \<longrightarrow> (\<exists>aa ab ba. (aa, ab, ba) \<in> asm_semantics specname inp_vs (a, b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc aa (ab, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<forall>b. enc (snd (asm_fetch (globals sst))) = enc b \<longrightarrow> (\<exists>a aa ba. (a, aa, ba) \<in> asm_semantics specname (asm_args sst) (fst (asm_fetch (globals sst)), b) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc a (aa, ba)))\<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; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; \<exists>a aa b. (a, aa, b) \<in> asm_semantics specname (asm_args sst) (fst (asm_fetch (globals sst)), snd (asm_fetch (globals sst))) \<and> (\<exists>gst. trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gst, p')] \<and> acc_vars (function_outputs gf) gst = asm_rets_to_list ret enc a (aa, b))\<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 a aa b gsta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b)\<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 a aa b gsta. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); \<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 (1 subgoal):
 1. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; 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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst) \<rightarrow>\<^sup>* (?com'62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, ?xst'62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 3. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>ja trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + ja) = Some (?com'62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, ?xst'62 sst tr gst n' gf' tr' n'' gf a aa b gsta j) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)\<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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (Spec (asm_spec ti gdata vol specname asm_ret asm_args), Normal sst) \<rightarrow>\<^sup>* (?com'67 sst tr gst n' gf' tr' n'' gf a aa b gsta j, ?xst'62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 3. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>ja trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + ja) = Some (add_cont (?com'67 sst tr gst n' gf' tr' n'' gf a aa b gsta j) con, ?xst'62 sst tr gst n' gf' tr' n'' gf a aa b gsta j) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)\<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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> SGamma\<turnstile> \<langle>Spec (asm_spec ti gdata vol specname asm_ret asm_args),Normal sst\<rangle> \<Rightarrow> Normal (?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 3. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>ja trace'. 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 (?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j)) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)\<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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (sst, ?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j) \<in> asm_spec ti gdata vol specname asm_ret asm_args
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 3. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>ja trace'. 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 (?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j)) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)\<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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec {(s, s'). \<exists>x\<in>asm_semantics specname (asm_args s) (asm_fetch (globals s)). case x of (v', gl') \<Rightarrow> s' = asm_ret v' (globals_update (asm_store gdata gl') s)}) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> \<exists>x\<in>asm_semantics specname (asm_args sst) (asm_fetch (globals sst)). case x of (v', gl') \<Rightarrow> ?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j = asm_ret v' (globals_update (asm_store gdata gl') sst)
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 3. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>ja trace'. 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 (?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j)) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)\<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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec {(s, s'). \<exists>x\<in>asm_semantics specname (asm_args s) (asm_fetch (globals s)). case x of (v', gl') \<Rightarrow> s' = asm_ret v' (globals_update (asm_store gdata gl') s)}) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> case (a, aa, b) of (v', gl') \<Rightarrow> ?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j = asm_ret v' (globals_update (asm_store gdata gl') sst)
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 3. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>ja trace'. 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 (?t69 sst tr gst n' gf' tr' n'' gf a aa b gsta j)) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)\<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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]\<rbrakk> \<Longrightarrow> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; tr (n' + j) = Some [(nn', return_vars (function_outputs gf) rets gsta gst, p)]; \<exists>ja trace'. 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 (asm_ret a (globals_update (asm_store gdata (aa, b)) sst))) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y62 sst tr gst n' gf' tr' n'' gf a aa b gsta j, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss62 sst tr gst n' gf' tr' n'' gf a aa b gsta j)\<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 a aa b gsta j. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 2 \<le> j; 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 (asm_ret a (globals_update (asm_store gdata (aa, b)) sst))) \<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 a aa b gsta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 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 (asm_ret a (globals_update (asm_store gdata (aa, b)) sst))); 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 a aa b gsta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 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 (asm_ret a (globals_update (asm_store gdata (aa, b)) sst))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); \<forall>m' v' ms'. gdata (asm_store gdata (m', ms') (globals sst)) = gdata (globals sst) \<and> (v', m', ms') \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)) \<longrightarrow> eqs2 (save_vals rets (asm_rets_to_list ret enc v' (m', ms')) gst) (asm_ret v' (globals_update (asm_store gdata (m', ms')) sst)) \<and> asm_ret v' (globals_update (asm_store gdata (m', ms')) sst) \<in> I\<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 a aa b gsta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 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 (asm_ret a (globals_update (asm_store gdata (aa, b)) sst))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); \<forall>m' v' ms'. gdata (asm_store gdata (m', ms') (globals sst)) = gdata (globals sst) \<and> (v', m', ms') \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)) \<longrightarrow> eqs2 (save_vals rets (asm_rets_to_list ret enc v' (m', ms')) gst) (asm_ret v' (globals_update (asm_store gdata (m', ms')) sst)) \<and> asm_ret v' (globals_update (asm_store gdata (m', ms')) sst) \<in> I\<rbrakk> \<Longrightarrow> tr (?n'91 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') = Some [(nn', ?gst91 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace', ?gf'91 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace')] \<and> asm_ret (?ab95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') (?ba95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') \<in> UNIV \<and> asm_ret (?ab95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') (?ba95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') \<in> I \<and> eqs2 (?gst91 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') (asm_ret (?ab95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') (?ba95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace')) \<and> n \<le> ?n'91 sst tr gst n' gf' tr' n'' gf a aa b gsta 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 (asm_ret (?ab95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace') (?ba95 sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace')))
 2. \<And>sst tr gst n' gf' tr' n'' gf a aa b gsta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 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 (asm_ret a (globals_update (asm_store gdata (aa, b)) sst))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); \<forall>m' v' ms'. gdata (asm_store gdata (m', ms') (globals sst)) = gdata (globals sst) \<and> (v', m', ms') \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)) \<longrightarrow> eqs2 (save_vals rets (asm_rets_to_list ret enc v' (m', ms')) gst) (asm_ret v' (globals_update (asm_store gdata (m', ms')) sst)) \<and> asm_ret v' (globals_update (asm_store gdata (m', ms')) sst) \<in> I; \<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 a aa b gsta j ja trace'. \<lbrakk>sst \<in> P; tr n' = Some [(NextNode m, gst, gf')]; eqs gst sst; 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 (Spec (asm_spec ti gdata vol specname asm_ret asm_args)) con, Normal sst); sst \<in> I; GGamma p' = Some gf; map (\<lambda>i. i gst) args = asm_args_to_list enc (asm_args sst) (asm_fetch (globals sst)); len = length args; distinct (function_inputs gf); length (function_inputs gf) = length args; trace_drop_n (Suc n') (Suc 0) tr \<in> exec_trace GGamma p'; (a, aa, b) \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)); trace_end (trace_drop_n (Suc n') (Suc 0) tr) = Some [(Ret, gsta, p')]; acc_vars (function_outputs gf) gsta = asm_rets_to_list ret enc a (aa, b); 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 (asm_ret a (globals_update (asm_store gdata (aa, b)) sst))); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + ja}\<^esub>) \<in> suffix_tuple_closure_inter (set tS); \<forall>m' v' ms'. gdata (asm_store gdata (m', ms') (globals sst)) = gdata (globals sst) \<and> (v', m', ms') \<in> asm_semantics specname (asm_args sst) (asm_fetch (globals sst)) \<longrightarrow> eqs2 (save_vals rets (asm_rets_to_list ret enc v' (m', ms')) gst) (asm_ret v' (globals_update (asm_store gdata (m', ms')) sst)) \<and> asm_ret v' (globals_update (asm_store gdata (m', ms')) sst) \<in> I; \<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!