theory GraphProof

lemma stepwise_graph_refine_Cond:
  "stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (l # nns, l' # nns') rel orel otr (Suc N)
    \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (r # nns, r' # nns') rel orel otr (Suc N)
    \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2
    \<Longrightarrow> function_graph gf1 n = Some (Cond l r cond)
    \<Longrightarrow> function_graph gf2 n' = Some (Cond l' r' cond')
    \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> cond x = cond' y
    \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns')
        (NextNode n # nns, NextNode n' # nns') rel orel otr N" apply (rule stepwise_graph_refineI) apply (clarsimp simp del: last.simps not_None_eq) 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 exec_graph_invariant_Cons
                 split: graph_function.split_asm split: if_split_asm
              simp del: last.simps not_None_eq) apply (simp_all only: exI all_simps[symmetric] simp_thms) apply (erule_tac i="Suc i" and j="Suc j"
     and nns="(l # xs, ys)" for xs ys in stepwise_graph_refineD, simp) apply (erule_tac i="Suc i" and j="Suc j"
    and nns="(r # xs, ys)" for xs ys in stepwise_graph_refineD, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (l # nns, l' # nns') rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (r # nns, r' # nns') rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Cond l r cond); function_graph gf2 n' = Some (node.Cond l' r' cond'); \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> cond x = cond' y\<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. \<lbrakk>stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (l # nns, l' # nns') rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (r # nns, r' # nns') rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Cond l r cond); function_graph gf2 n' = Some (node.Cond l' r' cond'); \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> cond x = cond' y; N \<le> i \<and> N \<le> j \<and> tr i \<noteq> None \<and> tr' j \<noteq> None \<and> (map fst (the (tr i)), map fst (the (tr' j))) = (NextNode n # nns, NextNode n' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (f1 # fns, f2 # fns') \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> (otr \<noteq> None \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (f1 # fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (f1 # fns, f2 # fns')))\<rbrakk> \<Longrightarrow> (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')))) 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) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Cond l r cond); function_graph gf2 n' = Some (node.Cond l' r' cond'); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa))\<rbrakk> \<Longrightarrow> (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')))) 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) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Cond l r cond); function_graph gf2 n' = Some (node.Cond l' r' cond'); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); 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> (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')))) 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) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # map fst zsa) rel orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Cond l r cond); function_graph gf2 n' = Some (node.Cond l' r' cond'); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); 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> (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')))) proof (prove)
goal (4 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # 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.Cond l r cond); x3a n' = Some (node.Cond l' r' cond'); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); cond aa; gf2 = GraphFunction x1a x2a x3a x4a; cond' ac; tr' (Suc j) = Some ((l', ac, f2) # zsa); tr (Suc i) = Some ((l, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (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'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # 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.Cond l r cond); x3a n' = Some (node.Cond l' r' cond'); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); cond aa; gf2 = GraphFunction x1a x2a x3a x4a; \<not> cond' ac; tr' (Suc j) = Some ((r', ac, f2) # zsa); tr (Suc i) = Some ((l, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (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'))))
 3. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # 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.Cond l r cond); x3a n' = Some (node.Cond l' r' cond'); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); \<not> cond aa; gf2 = GraphFunction x1a x2a x3a x4a; cond' ac; tr' (Suc j) = Some ((l', ac, f2) # zsa); tr (Suc i) = Some ((r, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (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'))))
 4. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # 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.Cond l r cond); x3a n' = Some (node.Cond l' r' cond'); \<forall>x xs y. (\<exists>ys. rel (x # xs, y # ys)) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); \<not> cond aa; gf2 = GraphFunction x1a x2a x3a x4a; \<not> cond' ac; tr' (Suc j) = Some ((r', ac, f2) # zsa); tr (Suc i) = Some ((r, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (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')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # 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.Cond l r cond); x3a n' = Some (node.Cond l' r' cond'); \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); True; gf2 = GraphFunction x1a x2a x3a x4a; cond' ac; tr' (Suc j) = Some ((l', ac, f2) # zsa); tr (Suc i) = Some ((l, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (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'))))
 2. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # 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.Cond l r cond); x3a n' = Some (node.Cond l' r' cond'); \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); True; gf2 = GraphFunction x1a x2a x3a x4a; \<not> cond' ac; tr' (Suc j) = Some ((r', ac, f2) # zsa); tr (Suc i) = Some ((r, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (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')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>gf1 = GraphFunction x1 x2 x3 x4; stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (l # map fst zs, l' # map fst zsa) rel orel otr (Suc N); stepwise_graph_refine Gamma (f1 # map (snd \<circ> snd) zs, f2 # map (snd \<circ> snd) zsa) (r # map fst zs, r' # 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.Cond l r cond); x3a n' = Some (node.Cond l' r' cond'); \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> cond x = cond' y; 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; otr \<noteq> None \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (last (f1 # map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (last (f2 # map (snd \<circ> snd) zsa)); True; gf2 = GraphFunction x1a x2a x3a x4a; \<not> cond' ac; tr' (Suc j) = Some ((r', ac, f2) # zsa); tr (Suc i) = Some ((r, aa, f1) # zs)\<rbrakk> \<Longrightarrow> (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')))) proof (prove)
goal:
No subgoals!