theory GraphProof

lemma restr_trace_refine_Call_single:
  "\<not> fst ccall \<and> (\<exists>nn outps. get_function_call gfs ccall = Some (nn, cfname, cinps, outps))
    \<Longrightarrow> Gamma1 cfname = Some cf \<Longrightarrow> wf_graph_function cf cilen colen
    \<Longrightarrow> fst acall \<and> (\<exists>nn outps. get_function_call gfs acall = Some (nn, afname, ainps, outps))
    \<Longrightarrow> Gamma2 afname = Some af \<Longrightarrow> wf_graph_function af ailen aolen
    \<Longrightarrow> graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel'
    \<Longrightarrow> double_pc ccall (tr, tr') \<longrightarrow> func_inputs_match gfs irel ccall acall (tr, tr')
    \<Longrightarrow> double_pc ccall (tr, tr') \<longrightarrow> double_pc acall (tr, tr')
    \<Longrightarrow> function_call_trace_embed (double_visit ccall (tr, tr')) tr
            (ctr (tr, tr')) Gamma1 cfname cinps
    \<Longrightarrow> function_call_trace_embed (double_visit acall (tr, tr')) tr'
            (ctr' (tr, tr')) Gamma2 afname ainps
    \<Longrightarrow> (double_pc ccall (tr, tr') \<longrightarrow> ctr (tr, tr') \<noteq> None \<and> ctr' (tr, tr') \<noteq> None
                  \<and> trace_end (the (ctr (tr, tr'))) \<noteq> None
                  \<and> trace_refine2 prec (cf, af) orel'
                      (the (ctr (tr, tr'))) (the (ctr' (tr, tr'))))
        \<longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 rs1 rs2 orel tr tr'
    \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 rs1 rs2 orel tr tr'" apply (clarsimp simp: restr_trace_refine_def) apply (case_tac "\<not> double_pc ccall (tr, tr')") apply (auto simp: double_trace_imp_def)[1] apply (clarsimp simp: function_call_trace_embed_def double_trace_imp_def double_visit_None) apply (drule(4) graph_function_refine_trace2[THEN iffD1, rotated -1, rule_format]) apply simp apply (rule conjI, assumption)+ apply simp apply (rule exI, rule conjI, rule refl, simp)+ apply (clarsimp simp: func_inputs_match_def) apply (erule rsubst[where P=irel]) apply (rule ext, simp add: tuple_switch_def switch_val_def) apply (case_tac "trace_end (the (ctr (tr, tr')))") apply (case_tac "trace_end (the (ctr' (tr, tr')))") apply (clarsimp simp: trace_refine2_def trace_refine_def) apply (clarsimp simp: trace_refine2_def trace_refine_def) apply (clarsimp simp: list.split[where P="Not", THEN consume_Not_eq]
                         next_node.split[where P="Not", THEN consume_Not_eq]
                         trace_end_Nil) apply (drule(1) exec_trace_end_SomeD)+ apply clarsimp apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> fst ccall \<and> (\<exists>nn outps. get_function_call gfs ccall = Some (nn, cfname, cinps, outps)); Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; fst acall \<and> (\<exists>nn outps. get_function_call gfs acall = Some (nn, afname, ainps, outps)); Gamma2 afname = Some af; wf_graph_function af ailen aolen; graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel'; double_pc ccall (tr, tr') \<longrightarrow> func_inputs_match gfs irel ccall acall (tr, tr'); double_pc ccall (tr, tr') \<longrightarrow> double_pc acall (tr, tr'); function_call_trace_embed (double_visit ccall (tr, tr')) tr (ctr (tr, tr')) Gamma1 cfname cinps; function_call_trace_embed (double_visit acall (tr, tr')) tr' (ctr' (tr, tr')) Gamma2 afname ainps; (double_pc ccall (tr, tr') \<longrightarrow> ctr (tr, tr') \<noteq> None \<and> ctr' (tr, tr') \<noteq> None \<and> trace_end (the (ctr (tr, tr'))) \<noteq> None \<and> trace_refine2 prec (cf, af) orel' (the (ctr (tr, tr'))) (the (ctr' (tr, tr')))) \<longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 rs1 rs2 orel tr tr'\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 rs1 rs2 orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' nn outps nna outpsa xs ys. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel'; double_pc ccall (tr, tr') \<longrightarrow> func_inputs_match gfs irel ccall acall (tr, tr'); double_pc ccall (tr, tr') \<longrightarrow> double_pc acall (tr, tr'); function_call_trace_embed (double_visit ccall (tr, tr')) tr (ctr (tr, tr')) Gamma1 cfname cinps; function_call_trace_embed (double_visit acall (tr, tr')) tr' (ctr' (tr, tr')) Gamma2 afname ainps; (double_pc ccall (tr, tr') \<longrightarrow> (\<exists>y. ctr (tr, tr') = Some y) \<and> (\<exists>y. ctr' (tr, tr') = Some y) \<and> (\<exists>y. trace_end (the (ctr (tr, tr'))) = Some y) \<and> trace_refine2 prec (cf, af) orel' (the (ctr (tr, tr'))) (the (ctr' (tr, tr')))) \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel'; double_pc ccall (tr, tr') \<longrightarrow> func_inputs_match gfs irel ccall acall (tr, tr'); double_pc ccall (tr, tr') \<longrightarrow> double_pc acall (tr, tr'); function_call_trace_embed (double_visit ccall (tr, tr')) tr (ctr (tr, tr')) Gamma1 cfname cinps; function_call_trace_embed (double_visit acall (tr, tr')) tr' (ctr' (tr, tr')) Gamma2 afname ainps; (double_pc ccall (tr, tr') \<longrightarrow> (\<exists>y. ctr (tr, tr') = Some y) \<and> (\<exists>y. ctr' (tr, tr') = Some y) \<and> (\<exists>y. trace_end (the (ctr (tr, tr'))) = Some y) \<and> trace_refine2 prec (cf, af) orel' (the (ctr (tr, tr'))) (the (ctr' (tr, tr')))) \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> double_pc ccall (tr, tr')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' nn outps nna outpsa xs ys. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel'; double_pc ccall (tr, tr') \<longrightarrow> func_inputs_match gfs irel ccall acall (tr, tr'); double_pc ccall (tr, tr') \<longrightarrow> double_pc acall (tr, tr'); function_call_trace_embed (double_visit ccall (tr, tr')) tr (ctr (tr, tr')) Gamma1 cfname cinps; function_call_trace_embed (double_visit acall (tr, tr')) tr' (ctr' (tr, tr')) Gamma2 afname ainps; (double_pc ccall (tr, tr') \<longrightarrow> (\<exists>y. ctr (tr, tr') = Some y) \<and> (\<exists>y. ctr' (tr, tr') = Some y) \<and> (\<exists>y. trace_end (the (ctr (tr, tr'))) = Some y) \<and> trace_refine2 prec (cf, af) orel' (the (ctr (tr, tr'))) (the (ctr' (tr, tr')))) \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc ccall (tr, tr')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' nn outps nna outpsa xs ys. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel'; double_pc ccall (tr, tr') \<longrightarrow> func_inputs_match gfs irel ccall acall (tr, tr'); double_pc ccall (tr, tr') \<longrightarrow> double_pc acall (tr, tr'); function_call_trace_embed (double_visit ccall (tr, tr')) tr (ctr (tr, tr')) Gamma1 cfname cinps; function_call_trace_embed (double_visit acall (tr, tr')) tr' (ctr' (tr, tr')) Gamma2 afname ainps; (double_pc ccall (tr, tr') \<longrightarrow> (\<exists>y. ctr (tr, tr') = Some y) \<and> (\<exists>y. ctr' (tr, tr') = Some y) \<and> (\<exists>y. trace_end (the (ctr (tr, tr'))) = Some y) \<and> trace_refine2 prec (cf, af) orel' (the (ctr (tr, tr'))) (the (ctr' (tr, tr')))) \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc ccall (tr, tr')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; graph_function_refine prec Gamma1 cfname Gamma2 afname irel orel'; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> (?tr58 gf gf' nn outps nna outpsa xs ys y ya \<in> exec_trace Gamma1 cfname \<and> ?tr'58 gf gf' nn outps nna outpsa xs ys y ya \<in> exec_trace Gamma2 afname) \<and> Gamma1 cfname = Some cf \<and> Gamma2 afname = Some af \<and> (\<exists>xsa ysa. the (?tr58 gf gf' nn outps nna outpsa xs ys y ya 0) = [init_state cfname cf xsa] \<and> length xsa = length (function_inputs cf) \<and> the (?tr'58 gf gf' nn outps nna outpsa xs ys y ya 0) = [init_state afname af ysa] \<and> length ysa = length (function_inputs af) \<and> irel (tuple_switch (xsa, ysa)))
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' (?tr58 gf gf' nn outps nna outpsa xs ys y ya) (?tr'58 gf gf' nn outps nna outpsa xs ys y ya)\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> ?tr58 gf gf' nn outps nna outpsa xs ys y ya \<in> exec_trace Gamma1 cfname \<and> ?tr'58 gf gf' nn outps nna outpsa xs ys y ya \<in> exec_trace Gamma2 afname \<and> (\<exists>xsa. the (?tr58 gf gf' nn outps nna outpsa xs ys y ya 0) = [init_state cfname cf xsa] \<and> length xsa = length (function_inputs cf) \<and> (\<exists>ysa. the (?tr'58 gf gf' nn outps nna outpsa xs ys y ya 0) = [init_state afname af ysa] \<and> length ysa = length (function_inputs af) \<and> irel (tuple_switch (xsa, ysa))))
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' (?tr58 gf gf' nn outps nna outpsa xs ys y ya) (?tr'58 gf gf' nn outps nna outpsa xs ys y ya)\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> \<exists>xs. the (y 0) = [init_state cfname cf xs] \<and> length xs = length (function_inputs cf) \<and> (\<exists>ys. the (ya 0) = [init_state afname af ys] \<and> length ys = length (function_inputs af) \<and> irel (tuple_switch (xs, ys)))
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> \<exists>xs. init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps) = init_state cfname cf xs \<and> length xs = length (function_inputs cf) \<and> (\<exists>ys. init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps) = init_state afname af ys \<and> length ys = length (function_inputs af) \<and> irel (tuple_switch (xs, ys)))
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> irel (tuple_switch (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps, map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps))
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; irel (\<lambda>x. map (\<lambda>f. f (the (double_visit (tuple_switch (ccall, acall) x) (tr, tr')))) (tuple_switch (cinps, ainps) x)); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> irel (tuple_switch (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps, map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps))
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]\<rbrakk> \<Longrightarrow> (\<lambda>x. map (\<lambda>f. f (the (double_visit (tuple_switch (ccall, acall) x) (tr, tr')))) (tuple_switch (cinps, ainps) x)) = tuple_switch (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps, map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = None\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (3 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = None; trace_end (the (ctr' (tr, tr'))) = None\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = None; trace_end (the (ctr' (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 3. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = None; trace_end (the (ctr' (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end tr = None; fst (hd a) = Err \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; case a of [] \<Rightarrow> False | [(Err, xa, xb)] \<Rightarrow> True | (Err, xa, xb) # aa # lista \<Rightarrow> False | (_, b) # list \<Rightarrow> False; trace_end y = None; trace_end ya = Some a\<rbrakk> \<Longrightarrow> case trace_end tr' of None \<Rightarrow> True | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya aa b z. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end tr = None; length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_end y = None; trace_end ya = Some [(Err, aa, b)]; trace_end tr' = Some z; fst (hd z) = Err\<rbrakk> \<Longrightarrow> \<exists>a b. z = [(Err, a, b)]
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya aa b z. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end tr = None; length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_end y = None; fst (hd z) = Err; \<exists>n. ya n = Some [(Err, aa, b)] \<and> ya (Suc n) = None \<and> (\<exists>nn st g. [(Err, aa, b)] = [(nn, st, g)] \<and> nn \<in> {Ret, Err}); \<exists>n. tr' n = Some z \<and> tr' (Suc n) = None \<and> (\<exists>nn st g. z = [(nn, st, g)] \<and> nn \<in> {Ret, Err})\<rbrakk> \<Longrightarrow> \<exists>a b. z = [(Err, a, b)]
 2. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); (\<exists>ya. trace_end y = Some ya) \<and> trace_refine2 prec (cf, af) orel' y ya \<longrightarrow> (\<exists>xsa. init_state f1 gf xs = init_state f1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end y = None \<longrightarrow> trace_end tr = None; trace_end ya = None \<longrightarrow> trace_end tr' = None; (\<exists>z. trace_end y = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end (the (ctr (tr, tr'))) = Some a\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' nn outps nna outpsa xs ys y ya a. \<lbrakk>Gamma1 cfname = Some cf; wf_graph_function cf cilen colen; Gamma2 afname = Some af; wf_graph_function af ailen aolen; func_inputs_match gfs irel ccall acall (tr, tr'); double_pc acall (tr, tr'); \<not> fst ccall; get_function_call gfs ccall = Some (nn, cfname, cinps, outps); fst acall; get_function_call gfs acall = Some (nna, afname, ainps, outpsa); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc ccall (tr, tr'); ctr (tr, tr') = Some y; ctr' (tr, tr') = Some ya; y \<in> exec_trace Gamma1 cfname; ya \<in> exec_trace Gamma2 afname; trace_end ya = None \<longrightarrow> trace_end tr' = None; fst (hd a) = Err \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err); (\<exists>z. trace_end ya = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr' = Some z \<and> fst (hd z) = Err); length cinps = length (function_inputs cf); y 0 = Some [init_state cfname cf (map (\<lambda>i. i (the (double_visit ccall (tr, tr')))) cinps)]; length ainps = length (function_inputs af); ya 0 = Some [init_state afname af (map (\<lambda>i. i (the (double_visit acall (tr, tr')))) ainps)]; trace_refine2 prec (cf, af) orel' y ya; trace_end y = Some a; (\<forall>xsa. init_state f1 gf xs = init_state f1 gf xsa \<longrightarrow> length xsa \<noteq> length (function_inputs gf)) \<or> (\<forall>ysa. init_state f2 gf' ys = init_state f2 gf' ysa \<longrightarrow> length ysa \<noteq> length (function_inputs gf'))\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal:
No subgoals!