theory GraphProof

lemma stepwise_graph_refine_Call_same:
  "stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (nn # nns, nn' # nns') rel orel otr (Suc N)
    \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2
    \<Longrightarrow> function_graph gf1 n = Some (Call nn fname inputs outputs)
    \<Longrightarrow> function_graph gf2 n' = Some (Call nn' fname inputs' outputs')
    \<Longrightarrow> Gamma fname = Some gf3
    \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'
    \<Longrightarrow> \<forall>x xs y ys zs st. rel (x # xs, y # ys)
        \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)
    \<Longrightarrow> \<forall>sts. fst (fst sts) = Err \<longrightarrow> fst (snd sts) = Err \<longrightarrow> orel sts
    \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns')
        (NextNode n # nns, NextNode n' # nns') rel orel otr N" apply (rule stepwise_graph_refineI, clarsimp) apply (simp only: all_simps[symmetric]) apply (frule(4) exec_trace_drop_n_Cons[where gf=gf1]) apply (frule(4) exec_trace_drop_n_Cons[where gf=gf2]) apply (frule_tac i=i and tr=tr in exec_trace_step_cases) apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def init_vars_def
                 split: graph_function.split_asm) apply (subgoal_tac "trace_drop_n (Suc i) (length (the (tr i))) tr
    = trace_drop_n (Suc j) (length (the (tr' j))) tr'") apply (frule_tac f=trace_end in arg_cong) apply (drule fun_eq_iff[THEN iffD1]) apply (case_tac "trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr)") apply simp apply (drule(1) trace_end_trace_drop_n_None, simp)+ apply simp apply clarsimp apply (drule(1) exec_trace_end_SomeD)+ apply clarsimp apply (erule disjE) apply (frule_tac tr=tr and i=i and k=na in exec_trace_drop_n_rest_Cons[rule_format],
      (simp only: function_graph.simps)+) apply (frule_tac tr=tr' and i=j and k=na in exec_trace_drop_n_rest_Cons[rule_format],
      (simp only: function_graph.simps)+) apply (frule_tac i="Suc i + na" and tr=tr in exec_trace_step_cases) apply (frule_tac i="Suc j + na" and tr=tr' in exec_trace_step_cases) apply (clarsimp simp: field_simps exec_graph_step_def) apply (drule_tac tr=tr and tr'=tr' and i="i + na + 2" and j="j + na + 2"
      in stepwise_graph_refineD) apply (simp add: ) apply auto[1] apply auto[1] apply (drule(1) trace_end_trace_drop_n_Err[rotated], simp add: trace_end_exec_SomeI)+ apply (case_tac "hd (the (trace_end tr))") apply (case_tac "hd (the (trace_end tr'))") apply clarsimp apply (rule ext) apply (rule exec_trace_deterministic, simp+) apply (simp add: trace_drop_n_def) apply (simp only: all_simps[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (nn # nns, nn' # nns') rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys zs st. rel (x # xs, y # ys) \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys); \<forall>sts. fst (fst sts) = Err \<longrightarrow> fst (snd sts) = Err \<longrightarrow> orel sts\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (NextNode n # nns, NextNode n' # nns') rel orel otr N proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some gf3; \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys zs st. rel (x # xs, y # ys) \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa))\<rbrakk> \<Longrightarrow> \<forall>y. (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr = Some y \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys zs st. rel (x # xs, y # ys) \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> \<forall>y. (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr = Some y \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys zs st. rel (x # xs, y # ys) \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> \<forall>y. (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr = Some y \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys zs st. rel (x # xs, y # ys) \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; tr i = None \<and> tr (Suc i) = None \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) \<or> tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<forall>y. (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr = Some y \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys zs st. rel (x # xs, y # ys) \<longrightarrow> rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; tr i = None \<and> tr (Suc i) = None \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) \<or> tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma; tr' j = None \<and> tr' (Suc j) = None \<or> (\<exists>state. tr' j = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr' (Suc j) = None) \<or> tr' j \<noteq> None \<and> tr' (Suc j) \<noteq> None \<and> (the (tr' j), the (tr' (Suc j))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<forall>y. (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr = Some y \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr'\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr'; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = trace_end (trace_drop_n (Suc j) (length (the (tr' j))) tr')\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = trace_end (trace_drop_n (Suc j) (length (the (tr' j))) tr'); \<forall>x. trace_drop_n (Suc i) (length (the (tr i))) tr x = trace_drop_n (Suc j) (length (the (tr' j))) tr' x\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = trace_end (trace_drop_n (Suc j) (length (the (tr' j))) tr'); \<forall>x. trace_drop_n (Suc i) (length (the (tr i))) tr x = trace_drop_n (Suc j) (length (the (tr' j))) tr' x; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = None\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b a. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = trace_end (trace_drop_n (Suc j) (length (the (tr' j))) tr'); \<forall>x. trace_drop_n (Suc i) (length (the (tr i))) tr x = trace_drop_n (Suc j) (length (the (tr' j))) tr' x; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (Suc (length zs)) tr) = None; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_end (trace_drop_n (Suc j) (Suc (length zsa)) tr') = None\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b a. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = trace_end (trace_drop_n (Suc j) (length (the (tr' j))) tr'); \<forall>x. trace_drop_n (Suc i) (length (the (tr i))) tr x = trace_drop_n (Suc j) (length (the (tr' j))) tr' x; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_end tr = None; trace_end tr' = None\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b a. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = trace_end (trace_drop_n (Suc j) (length (the (tr' j))) tr'); \<forall>x. trace_drop_n (Suc i) (length (the (tr i))) tr x = trace_drop_n (Suc j) (length (the (tr' j))) tr' x; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b a. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = trace_end (trace_drop_n (Suc j) (length (the (tr' j))) tr'); \<forall>x. trace_drop_n (Suc i) (length (the (tr i))) tr x = trace_drop_n (Suc j) (length (the (tr' j))) tr' x; trace_end (trace_drop_n (Suc i) (length (the (tr i))) tr) = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b a. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; trace_end (trace_drop_n (Suc i) (Suc (length zs)) tr) = Some a; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_end (trace_drop_n (Suc j) (Suc (length zsa)) tr') = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b a. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; \<exists>n. trace_drop_n (Suc i) (Suc (length zs)) tr n = Some a \<and> trace_drop_n (Suc i) (Suc (length zs)) tr (Suc n) = None \<and> (\<exists>nn st g. a = [(nn, st, g)] \<and> nn \<in> {Ret, Err}); \<exists>n. trace_drop_n (Suc j) (Suc (length zsa)) tr' n = Some a \<and> trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc n) = None \<and> (\<exists>nn st g. a = [(nn, st, g)] \<and> nn \<in> {Ret, Err})\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Ret \<or> nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Ret\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Ret; tr (Suc i + na) = Some ([(Ret, st, g)] @ (NextNode n, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Ret; tr (Suc i + na) = Some ([(Ret, st, g)] @ (NextNode n, aa, f1) # zs); tr' (Suc j + na) = Some ([(Ret, st, g)] @ (NextNode n', ac, f2) # zsa)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Ret; tr (Suc i + na) = Some ([(Ret, st, g)] @ (NextNode n, aa, f1) # zs); tr' (Suc j + na) = Some ([(Ret, st, g)] @ (NextNode n', ac, f2) # zsa); tr (Suc i + na) = None \<and> tr (Suc (Suc i + na)) = None \<or> (\<exists>state. tr (Suc i + na) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (Suc i + na)) = None) \<or> tr (Suc i + na) \<noteq> None \<and> tr (Suc (Suc i + na)) \<noteq> None \<and> (the (tr (Suc i + na)), the (tr (Suc (Suc i + na)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Ret; tr (Suc i + na) = Some ([(Ret, st, g)] @ (NextNode n, aa, f1) # zs); tr' (Suc j + na) = Some ([(Ret, st, g)] @ (NextNode n', ac, f2) # zsa); tr (Suc i + na) = None \<and> tr (Suc (Suc i + na)) = None \<or> (\<exists>state. tr (Suc i + na) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (Suc i + na)) = None) \<or> tr (Suc i + na) \<noteq> None \<and> tr (Suc (Suc i + na)) \<noteq> None \<and> (the (tr (Suc i + na)), the (tr (Suc (Suc i + na)))) \<in> exec_graph_step Gamma; tr' (Suc j + na) = None \<and> tr' (Suc (Suc j + na)) = None \<or> (\<exists>state. tr' (Suc j + na) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr' (Suc (Suc j + na)) = None) \<or> tr' (Suc j + na) \<noteq> None \<and> tr' (Suc (Suc j + na)) \<noteq> None \<and> (the (tr' (Suc j + na)), the (tr' (Suc (Suc j + na)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; tr (Suc (i + na)) = Some ((Ret, st, g) # (NextNode n, aa, f1) # zs); tr' (Suc (j + na)) = Some ((Ret, st, g) # (NextNode n', ac, f2) # zsa); tr (Suc (Suc (i + na))) = Some ((nn, return_vars x2b outputs st aa, f1) # zs); tr' (Suc (Suc (j + na))) = Some ((nn', return_vars x2b outputs' st ac, f2) # zsa)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (4 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; tr (Suc (i + na)) = Some ((Ret, st, g) # (NextNode n, aa, f1) # zs); tr' (Suc (j + na)) = Some ((Ret, st, g) # (NextNode n', ac, f2) # zsa); tr (Suc (Suc (i + na))) = Some ((nn, return_vars x2b outputs st aa, f1) # zs); tr' (Suc (Suc (j + na))) = Some ((nn', return_vars x2b outputs' st ac, f2) # zsa)\<rbrakk> \<Longrightarrow> Suc N \<le> i + na + 2 \<and> Suc N \<le> j + na + 2 \<and> tr (i + na + 2) \<noteq> None \<and> tr' (j + na + 2) \<noteq> None \<and> (map fst (the (tr (i + na + 2))), map fst (the (tr' (j + na + 2)))) = (nn # map fst zs, nn' # map fst zsa) \<and> (map (snd \<circ> snd) (the (tr (i + na + 2))), map (snd \<circ> snd) (the (tr' (j + na + 2)))) = (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) \<and> rel (map (fst \<circ> snd) (the (tr (i + na + 2))), map (fst \<circ> snd) (the (tr' (j + na + 2)))) \<and> (otr \<noteq> None \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa))) \<and> tr' \<in> exec_trace Gamma (last (snd (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa)))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; tr (Suc (i + na)) = Some ((Ret, st, g) # (NextNode n, aa, f1) # zs); tr' (Suc (j + na)) = Some ((Ret, st, g) # (NextNode n', ac, f2) # zsa); tr (Suc (Suc (i + na))) = Some ((nn, return_vars x2b outputs st aa, f1) # zs); tr' (Suc (Suc (j + na))) = Some ((nn', return_vars x2b outputs' st ac, f2) # zsa); (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 4. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (4 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; tr (Suc (i + na)) = Some ((Ret, st, g) # (NextNode n, aa, f1) # zs); tr' (Suc (j + na)) = Some ((Ret, st, g) # (NextNode n', ac, f2) # zsa); tr (Suc (Suc (i + na))) = Some ((nn, return_vars x2b outputs st aa, f1) # zs); tr' (Suc (Suc (j + na))) = Some ((nn', return_vars x2b outputs' st ac, f2) # zsa)\<rbrakk> \<Longrightarrow> (zs = [] \<longrightarrow> (zsa = [] \<longrightarrow> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma f1 \<and> tr' \<in> exec_trace Gamma f2) \<and> (zsa \<noteq> [] \<longrightarrow> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma f1 \<and> tr' \<in> exec_trace Gamma (last (map (snd \<circ> snd) zsa)))) \<and> (zs \<noteq> [] \<longrightarrow> (zsa = [] \<longrightarrow> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (map (snd \<circ> snd) zs)) \<and> tr' \<in> exec_trace Gamma f2) \<and> (zsa \<noteq> [] \<longrightarrow> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (map (snd \<circ> snd) zs)) \<and> tr' \<in> exec_trace Gamma (last (map (snd \<circ> snd) zsa))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; tr (Suc (i + na)) = Some ((Ret, st, g) # (NextNode n, aa, f1) # zs); tr' (Suc (j + na)) = Some ((Ret, st, g) # (NextNode n', ac, f2) # zsa); tr (Suc (Suc (i + na))) = Some ((nn, return_vars x2b outputs st aa, f1) # zs); tr' (Suc (Suc (j + na))) = Some ((nn', return_vars x2b outputs' st ac, f2) # zsa); (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 4. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(Ret, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; tr (Suc (i + na)) = Some ((Ret, st, g) # (NextNode n, aa, f1) # zs); tr' (Suc (j + na)) = Some ((Ret, st, g) # (NextNode n', ac, f2) # zsa); tr (Suc (Suc (i + na))) = Some ((nn, return_vars x2b outputs st aa, f1) # zs); tr' (Suc (Suc (j + na))) = Some ((nn', return_vars x2b outputs' st ac, f2) # zsa); (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err; map_option (fst \<circ> hd) (trace_end tr) = Some Err; map_option (fst \<circ> hd) (trace_end tr') = Some Err\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g a b c. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err; map_option (fst \<circ> hd) (trace_end tr) = Some Err; map_option (fst \<circ> hd) (trace_end tr') = Some Err; hd (the (trace_end tr)) = (a, b, c)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b na nna st g a b c ab ba ca. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b; \<forall>x. trace_drop_n (Suc i) (Suc (length zs)) tr x = trace_drop_n (Suc j) (Suc (length zsa)) tr' x; trace_drop_n (Suc j) (Suc (length zsa)) tr' na = Some [(nna, st, g)]; trace_drop_n (Suc j) (Suc (length zsa)) tr' (Suc na) = None; nna = Err; map_option (fst \<circ> hd) (trace_end tr) = Some Err; map_option (fst \<circ> hd) (trace_end tr') = Some Err; hd (the (trace_end tr)) = (a, b, c); hd (the (trace_end tr')) = (ab, ba, ca)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (\<forall>y. trace_end tr = Some y \<longrightarrow> orel (hd y, hd (the (trace_end tr'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr = trace_drop_n (Suc j) (length (the (tr' j))) tr' proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b x. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (length (the (tr i))) tr x = trace_drop_n (Suc j) (length (the (tr' j))) tr' x proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); trace_drop_n (Suc i) (Suc (length zs)) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc j) (Suc (length zsa)) tr' \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc (length zs)) tr 0 = trace_drop_n (Suc j) (Suc (length zsa)) tr' 0 proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a x1b x2b x3b x4b. \<lbrakk>tr (Suc i) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i aa) inputs) default_state, fname) # (NextNode n, aa, f1) # zs); gf2 = GraphFunction x1a x2a x3a x4a; tr' (Suc j) = Some ((NextNode x4b, save_vals x1b (map (\<lambda>i. i ac) inputs') default_state, fname) # (NextNode n', ac, f2) # zsa); gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (nn # map fst zs, nn' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some (GraphFunction x1 x2 x3 x4); Gamma f2 = Some (GraphFunction x1a x2a x3a x4a); x3 n = Some (node.Call nn fname inputs outputs); x3a n' = Some (node.Call nn' fname inputs' outputs'); Gamma fname = Some (GraphFunction x1b x2b x3b x4b); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> map (\<lambda>i. i x) inputs = map (\<lambda>i. i y) inputs'; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> (\<forall>zs st. rel (return_vars zs outputs st x # xs, return_vars zs outputs' st y # ys)); \<forall>a b aa ba. orel ((Err, a, b), Err, aa, ba); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; \<forall>a b. otr = Some (a, b) \<longrightarrow> a = tr \<and> b = tr'; fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); (\<lambda>ia. if \<forall>j<ia. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length zs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length zs)) \<circ> rev) (tr (ia + Suc i)) else None) \<in> exec_trace Gamma fname; (\<lambda>i. if \<forall>ja<i. (\<exists>y. tr' (Suc (j + ja)) = Some y) \<and> continuing (rev (drop (Suc (length zsa)) (rev (the (tr' (Suc (j + ja))))))) then map_option (rev \<circ> drop (Suc (length zsa)) \<circ> rev) (tr' (i + Suc j)) else None) \<in> exec_trace Gamma fname; gf3 = GraphFunction x1b x2b x3b x4b\<rbrakk> \<Longrightarrow> save_vals x1b (map (\<lambda>i. i aa) inputs) default_state = save_vals x1b (map (\<lambda>i. i ac) inputs') default_state proof (prove)
goal:
No subgoals!