theory GraphProof

theorem restr_trace_refine_Leaf:
  "wf_graph_function f1 ilen1 olen1 \<Longrightarrow> Gamma1 fn1 = Some f1
    \<Longrightarrow> wf_graph_function f2 ilen2 olen2 \<Longrightarrow> Gamma2 fn2 = Some f2
    \<Longrightarrow> pc Ret rs1 tr \<Longrightarrow> prec \<longrightarrow> pc Ret rs2 tr'
    \<Longrightarrow> output_rel orel (f1, f2) (rs1, rs2) (tr, tr')
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" apply (clarsimp simp only: restr_trace_refine_def) apply (clarsimp simp: trace_refine2_def trace_refine_def) apply (frule(1) pc_Ret_trace_end) apply (case_tac "trace_end tr'") apply (clarsimp split: option.split) apply (cut_tac tr=tr' in pc_Ret_trace_end, blast, assumption+) apply clarsimp apply (clarsimp simp: output_rel_def) apply (drule(1) exec_trace_end_SomeD)+ apply (safe del: impCE, simp_all) apply (erule rsubst[where P=orel], rule ext) apply (clarsimp simp: tuple_switch_def switch_val_def double_visit_def
                        wf_graph_function_init_extract restrs_list_def
                        wf_graph_function_length_function_inputs
                        function_outputs_st_def trace_end_visit_Ret
                        init_state_def wf_graph_function_acc_vars_save_vals) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr')\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<rbrakk> \<Longrightarrow> trace_refine2 prec (f1, f2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> 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 | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 a) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); \<exists>st g. trace_end tr = Some [(Ret, st, g)]\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> 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 | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 a) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xs ys. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); \<exists>st g. trace_end tr = Some [(Ret, st, g)]; trace_end tr' = None\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> 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 | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 a) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False
 2. \<And>xs ys a. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); \<exists>st g. trace_end tr = Some [(Ret, st, g)]; trace_end tr' = Some a\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> 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 | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 a) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xs ys st g. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); trace_end tr' = None; trace_end tr = Some [(Ret, st, g)]; prec; pc Ret rs2 tr'\<rbrakk> \<Longrightarrow> False
 2. \<And>xs ys a. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); \<exists>st g. trace_end tr = Some [(Ret, st, g)]; trace_end tr' = Some a\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> 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 | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 a) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xs ys st g. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); trace_end tr' = None; trace_end tr = Some [(Ret, st, g)]; prec; pc Ret rs2 tr'; \<exists>st g. trace_end tr' = Some [(Ret, st, g)]\<rbrakk> \<Longrightarrow> False
 2. \<And>xs ys a. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); \<exists>st g. trace_end tr = Some [(Ret, st, g)]; trace_end tr' = Some a\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> 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 | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 a) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xs ys a. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; output_rel orel (f1, f2) (rs1, rs2) (tr, tr'); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); \<exists>st g. trace_end tr = Some [(Ret, st, g)]; trace_end tr' = Some a\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> 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 | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 a) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xs ys a st g. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; orel (\<lambda>(x, y). acc_vars (tuple_switch (function_inputs, function_outputs) y (tuple_switch (f1, f2) x)) (the (double_visit (x, tuple_switch (NextNode (entry_point (tuple_switch (f1, f2) x)), Ret) y, tuple_switch (restrs_list [], tuple_switch (rs1, rs2) x) y) (tr, tr')))); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); trace_end tr' = Some a; trace_end tr = Some [(Ret, st, g)]\<rbrakk> \<Longrightarrow> case a of [] \<Rightarrow> False | (NextNode nat, b) # list \<Rightarrow> False | [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 st) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | (Ret, st', xa) # ab # lista \<Rightarrow> False | [(Err, xa, xb)] \<Rightarrow> True | (Err, xa, xb) # ab # lista \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xs ys a st g. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; orel (\<lambda>(x, y). acc_vars (tuple_switch (function_inputs, function_outputs) y (tuple_switch (f1, f2) x)) (the (double_visit (x, tuple_switch (NextNode (entry_point (tuple_switch (f1, f2) x)), Ret) y, tuple_switch (restrs_list [], tuple_switch (rs1, rs2) x) y) (tr, tr')))); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); \<exists>n. tr' n = Some a \<and> tr' (Suc n) = None \<and> (\<exists>nn st g. a = [(nn, st, g)] \<and> nn \<in> {Ret, Err}); \<exists>n. tr n = Some [(Ret, st, g)] \<and> tr (Suc n) = None \<and> (\<exists>nn sta ga. [(Ret, st, g)] = [(nn, sta, ga)] \<and> nn \<in> {Ret, Err})\<rbrakk> \<Longrightarrow> case a of [] \<Rightarrow> False | (NextNode nat, b) # list \<Rightarrow> False | [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 st) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 st') \<circ> snd)) | (Ret, st', xa) # ab # lista \<Rightarrow> False | [(Err, xa, xb)] \<Rightarrow> True | (Err, xa, xb) # ab # lista \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xs ys n na sta ga stb gb. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; orel (\<lambda>(x, y). acc_vars (tuple_switch (function_inputs, function_outputs) y (tuple_switch (f1, f2) x)) (the (double_visit (x, tuple_switch (NextNode (entry_point (tuple_switch (f1, f2) x)), Ret) y, tuple_switch (restrs_list [], tuple_switch (rs1, rs2) x) y) (tr, tr')))); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); tr' n = Some [(Ret, sta, ga)]; tr na = Some [(Ret, stb, gb)]; tr' (Suc n) = None; tr (Suc na) = None\<rbrakk> \<Longrightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 stb) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 sta) \<circ> snd)) proof (prove)
goal (1 subgoal):
 1. \<And>xs ys n na sta ga stb gb x. \<lbrakk>wf_graph_function f1 ilen1 olen1; Gamma1 fn1 = Some f1; wf_graph_function f2 ilen2 olen2; Gamma2 fn2 = Some f2; pc Ret rs1 tr; prec \<longrightarrow> pc Ret rs2 tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); tr' n = Some [(Ret, sta, ga)]; tr na = Some [(Ret, stb, gb)]; tr' (Suc n) = None; tr (Suc na) = None\<rbrakk> \<Longrightarrow> (case x of (x, y) \<Rightarrow> acc_vars (tuple_switch (function_inputs, function_outputs) y (tuple_switch (f1, f2) x)) (the (double_visit (x, tuple_switch (NextNode (entry_point (tuple_switch (f1, f2) x)), Ret) y, tuple_switch (restrs_list [], tuple_switch (rs1, rs2) x) y) (tr, tr')))) = switch_val fst (tuple_switch (acc_vars (function_inputs f1) (fst (snd (init_state fn1 f1 xs))), function_outputs_st f1 stb) \<circ> snd) (tuple_switch (acc_vars (function_inputs f2) (fst (snd (init_state fn2 f2 ys))), function_outputs_st f2 sta) \<circ> snd) x proof (prove)
goal:
No subgoals!