theory GraphLangLemmas

lemma exec_trace_drop_n_Cons:
  assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn'' = Some gf"
  shows "tr i = Some ((NextNode n, st, fn'') # xs)
    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
    \<Longrightarrow> Gamma fn' = Some gf'
    \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> exec_trace Gamma fn'" using tr apply (clarsimp simp: exec_trace_def) apply (intro conjI) apply (simp add: trace_drop_n_def) apply (cut_tac exec_trace_step_cases[where i=i, OF tr(1)]) apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons
                  split: graph_function.split_asm) apply (clarsimp simp: nat_trace_rel_def trace_drop_n_def
                        all_less_Suc_eq
             split del: if_split) apply (cut_tac i="Suc i + na" in exec_trace_Nil[OF tr(1)]) apply (drule_tac x="Suc i + na" in spec)+ apply (clarsimp simp: field_simps) apply (safe, simp_all) apply (safe intro!: rev_drop_step) apply (auto dest!: rev_drop_continuing) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> exec_trace Gamma fn' proof (prove)
using this:
tr \<in> exec_trace Gamma fn
Gamma fn'' = Some gf

goal (1 subgoal):
 1. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> exec_trace Gamma fn' proof (prove)
goal (1 subgoal):
 1. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> (\<exists>st. trace_drop_n (Suc i) (Suc (length xs)) tr 0 = Some [(NextNode (entry_point gf'), st, fn')]) \<and> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> nat_trace_rel continuing (exec_graph_step Gamma) proof (prove)
goal (2 subgoals):
 1. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> \<exists>st. trace_drop_n (Suc i) (Suc (length xs)) tr 0 = Some [(NextNode (entry_point gf'), st, fn')]
 2. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> nat_trace_rel continuing (exec_graph_step Gamma) proof (prove)
goal (2 subgoals):
 1. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> \<exists>st z. tr (Suc i) = Some z \<and> drop (Suc (length xs)) (rev z) = [(NextNode (entry_point gf'), st, fn')]
 2. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> nat_trace_rel continuing (exec_graph_step Gamma) proof (prove)
goal (2 subgoals):
 1. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; 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> \<exists>st z. tr (Suc i) = Some z \<and> drop (Suc (length xs)) (rev z) = [(NextNode (entry_point gf'), st, fn')]
 2. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> nat_trace_rel continuing (exec_graph_step Gamma) proof (prove)
goal (1 subgoal):
 1. \<And>gfa sta. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> nat_trace_rel continuing (exec_graph_step Gamma) proof (prove)
goal (1 subgoal):
 1. \<And>gfa sta na. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; \<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>y. tr (Suc n) = Some y) \<longrightarrow> (the (tr n), the (tr (Suc n))) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. tr n = Some y) \<and> continuing (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]\<rbrakk> \<Longrightarrow> ((if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None) = None \<longrightarrow> (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = None) \<and> ((\<exists>y. (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = Some y) \<longrightarrow> (the (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None), the (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None)) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None) = Some y) \<and> continuing (the (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None)) \<longrightarrow> (\<exists>y. (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>gfa sta na. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; \<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>y. tr (Suc n) = Some y) \<longrightarrow> (the (tr n), the (tr (Suc n))) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. tr n = Some y) \<and> continuing (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; tr (Suc i + na) \<noteq> Some []\<rbrakk> \<Longrightarrow> ((if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None) = None \<longrightarrow> (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = None) \<and> ((\<exists>y. (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = Some y) \<longrightarrow> (the (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None), the (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None)) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None) = Some y) \<and> continuing (the (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None)) \<longrightarrow> (\<exists>y. (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>gfa sta na. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; tr (Suc i + na) \<noteq> Some []; (tr (Suc i + na) = None \<longrightarrow> tr (Suc (Suc i + na)) = None) \<and> ((\<exists>y. tr (Suc (Suc i + na)) = Some y) \<longrightarrow> (the (tr (Suc i + na)), the (tr (Suc (Suc i + na)))) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. tr (Suc i + na) = Some y) \<and> continuing (the (tr (Suc i + na))) \<longrightarrow> (\<exists>y. tr (Suc (Suc i + na)) = Some y))\<rbrakk> \<Longrightarrow> ((if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None) = None \<longrightarrow> (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = None) \<and> ((\<exists>y. (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = Some y) \<longrightarrow> (the (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None), the (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None)) \<in> exec_graph_step Gamma) \<and> ((\<exists>y. (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None) = Some y) \<and> continuing (the (if \<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (na + Suc i)) else None)) \<longrightarrow> (\<exists>y. (if (\<exists>y. tr (Suc (i + na)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + na))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (i + j)))))))) then map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc na + Suc i)) else None) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>gfa sta na. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; tr (Suc (na + i)) \<noteq> Some []; tr (Suc (na + i)) = None \<longrightarrow> tr (Suc (Suc (na + i))) = None; (\<exists>y. tr (Suc (Suc (na + i))) = Some y) \<longrightarrow> (the (tr (Suc (na + i))), the (tr (Suc (Suc (na + i))))) \<in> exec_graph_step Gamma; (\<exists>y. tr (Suc (na + i)) = Some y) \<and> continuing (the (tr (Suc (na + i)))) \<longrightarrow> (\<exists>y. tr (Suc (Suc (na + i))) = Some y)\<rbrakk> \<Longrightarrow> ((\<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i)))))))) \<longrightarrow> ((\<exists>y. tr (Suc (na + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (na + i))))))) \<longrightarrow> ((\<exists>z. tr (Suc (Suc (na + i))) = Some z) \<longrightarrow> (the (map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc (na + i)))), the (map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc (Suc (na + i)))))) \<in> exec_graph_step Gamma) \<and> (continuing (the (map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc (na + i))))) \<longrightarrow> (\<exists>z. tr (Suc (Suc (na + i))) = Some z))) \<and> ((continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (na + i))))))) \<longrightarrow> tr (Suc (na + i)) = None \<or> (\<exists>j<na. tr (Suc (j + i)) = None \<or> \<not> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))))) \<longrightarrow> tr (Suc (na + i)) = None \<or> \<not> continuing (the (map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc (na + i))))))) \<and> ((\<exists>j<na. tr (Suc (j + i)) = None \<or> \<not> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i)))))))) \<longrightarrow> (\<exists>y. tr (Suc (na + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (na + i))))))) \<and> (\<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i)))))))) \<longrightarrow> ((\<exists>z. tr (Suc (Suc (na + i))) = Some z) \<longrightarrow> (the (map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc (na + i)))), the (map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc (Suc (na + i)))))) \<in> exec_graph_step Gamma) \<and> (continuing (the (map_option (rev \<circ> drop (Suc (length xs)) \<circ> rev) (tr (Suc (na + i))))) \<longrightarrow> (\<exists>z. tr (Suc (Suc (na + i))) = Some z))) proof (prove)
goal (17 subgoals):
 1. \<And>gfa sta na y ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; tr (Suc (Suc (na + i))) = None; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>gfa sta na y ya j. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; tr (Suc (Suc (na + i))) = None; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; j < na; tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 3. \<And>gfa sta na y j ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; tr (Suc (Suc (na + i))) = None; \<not> continuing y; j < na; tr (Suc (na + i)) = Some y; continuing (rev (drop (Suc (length xs)) (rev y))); \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 4. \<And>gfa sta na y ya z. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; (y, z) \<in> exec_graph_step Gamma; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; tr (Suc (Suc (na + i))) = Some z\<rbrakk> \<Longrightarrow> (rev (drop (Suc (length xs)) (rev y)), rev (drop (Suc (length xs)) (rev z))) \<in> exec_graph_step Gamma
 5. \<And>gfa sta na y ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; (y, the (tr (Suc (Suc (na + i))))) \<in> exec_graph_step Gamma; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y\<rbrakk> \<Longrightarrow> \<exists>z. tr (Suc (Suc (na + i))) = Some z
 6. \<And>gfa sta na y ya j. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; (y, the (tr (Suc (Suc (na + i))))) \<in> exec_graph_step Gamma; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; j < na; tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 7. \<And>gfa sta na y j ya z. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; (y, z) \<in> exec_graph_step Gamma; \<not> continuing y; j < na; tr (Suc (na + i)) = Some y; continuing (rev (drop (Suc (length xs)) (rev y))); \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (j + i)) = None; tr (Suc (Suc (na + i))) = Some z\<rbrakk> \<Longrightarrow> (rev (drop (Suc (length xs)) (rev y)), rev (drop (Suc (length xs)) (rev z))) \<in> exec_graph_step Gamma
 8. \<And>gfa sta na y j ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; ya = y; (y, the (tr (Suc (Suc (na + i))))) \<in> exec_graph_step Gamma; \<not> continuing y; j < na; tr (Suc (na + i)) = Some y; continuing (rev (drop (Suc (length xs)) (rev y))); \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> \<exists>z. tr (Suc (Suc (na + i))) = Some z
 9. \<And>gfa sta na y ya yb z. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; yb = y; (y, ya) \<in> exec_graph_step Gamma; z = ya; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; tr (Suc (Suc (na + i))) = Some ya\<rbrakk> \<Longrightarrow> (rev (drop (Suc (length xs)) (rev y)), rev (drop (Suc (length xs)) (rev ya))) \<in> exec_graph_step Gamma
 10. \<And>gfa sta na y ya yb j. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; yb = y; (y, ya) \<in> exec_graph_step Gamma; tr (Suc (Suc (na + i))) = Some ya; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; j < na; tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
A total of 17 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>gfa sta na y ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; tr (Suc (Suc (na + i))) = None; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>gfa sta na y ya j. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; tr (Suc (Suc (na + i))) = None; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; j < na; tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 3. \<And>gfa sta na y j ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; tr (Suc (Suc (na + i))) = None; \<not> continuing y; j < na; tr (Suc (na + i)) = Some y; continuing (rev (drop (Suc (length xs)) (rev y))); \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 4. \<And>gfa sta na y ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; (y, the (tr (Suc (Suc (na + i))))) \<in> exec_graph_step Gamma; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y\<rbrakk> \<Longrightarrow> \<exists>z. tr (Suc (Suc (na + i))) = Some z
 5. \<And>gfa sta na y ya j. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; (y, the (tr (Suc (Suc (na + i))))) \<in> exec_graph_step Gamma; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; j < na; tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 6. \<And>gfa sta na y j ya. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; (y, the (tr (Suc (Suc (na + i))))) \<in> exec_graph_step Gamma; \<not> continuing y; j < na; tr (Suc (na + i)) = Some y; continuing (rev (drop (Suc (length xs)) (rev y))); \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> \<exists>z. tr (Suc (Suc (na + i))) = Some z
 7. \<And>gfa sta na y ya yb j. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; (y, ya) \<in> exec_graph_step Gamma; tr (Suc (Suc (na + i))) = Some ya; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; j < na; tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 8. \<And>gfa sta na y. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; tr (Suc (Suc (na + i))) = None; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y\<rbrakk> \<Longrightarrow> False
 9. \<And>gfa sta na y j. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; tr (Suc (Suc (na + i))) = None; \<not> continuing y; \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); continuing (rev (drop (Suc (length xs)) (rev y))); tr (Suc (na + i)) = Some y; j < na; tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
 10. \<And>gfa sta na j y. \<lbrakk>tr i = Some ((NextNode n, st, fn'') # xs); function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; Gamma fn'' = Some gf; Gamma fn = Some gfa; tr 0 = Some [(NextNode (entry_point gfa), sta, fn)]; y \<noteq> []; tr (Suc (Suc (na + i))) = None; \<not> continuing y; j < na; tr (Suc (na + i)) = Some y; continuing (rev (drop (Suc (length xs)) (rev y))); \<forall>j<na. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (j + i)) = None\<rbrakk> \<Longrightarrow> False
A total of 13 subgoals... proof (prove)
goal:
No subgoals!