theory GraphProof

lemma extended_pred_trace_drop_n:
  "trace_addr tr i = Some (NextNode n)
    \<Longrightarrow> trace_addr tr j = Some nn
    \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
    \<Longrightarrow> wf_graph_function f ilen olen
    \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs)
    \<Longrightarrow> Gamma fname = Some f'
    \<Longrightarrow> i < j \<Longrightarrow> nn \<noteq> Err
    \<Longrightarrow> trace_addr tr ` {Suc i ..< j} \<subseteq> {None}
    \<Longrightarrow> trace_bottom_addr tr ` {Suc i ..< j} \<subseteq> {Some (NextNode n)}
    \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fname
        \<and> Suc i < j
        \<and> (\<exists>st g. trace_drop_n (Suc i) 1 tr (j - Suc (Suc i)) = Some [(Ret, st, g)])
        \<and> trace_drop_n (Suc i) 1 tr (j - Suc i) = None" apply (clarsimp dest!: trace_addr_SomeD) apply (frule_tac i=i in exec_trace_invariant, simp) apply (simp add: exec_graph_invariant_Cons) apply (frule(3) exec_trace_drop_n, simp+) apply (rule context_conjI) apply (rule ccontr, simp add: linorder_not_less le_Suc_eq) apply (frule_tac i=i in exec_trace_step_cases, simp) apply (clarsimp simp: all_exec_graph_step_cases) apply (subgoal_tac "Suc (j - 2) = j - 1", simp_all) apply (rule context_conjI) prefer 2 apply (clarsimp simp: trace_drop_n_def if_x_None_eq_Some) apply (rule_tac x="j - Suc (Suc i)" in exI, simp) apply (frule subsetD, rule_tac x="j - 1" and f="trace_addr tr" in imageI, simp) apply (frule subsetD, rule_tac x="j - 1" and f="trace_bottom_addr tr" in imageI, simp) apply (frule_tac i="j - 1" in exec_trace_step_cases) apply clarsimp apply (simp add: all_exec_graph_step_cases, safe; (solves \<open>simp add: trace_addr_def\<close>)?) apply (simp(no_asm) add: trace_drop_n_def if_x_None_eq_Some) apply clarsimp apply (cut_tac tr=tr and i="Suc (i + ja)" in bottom_addr_only) apply (simp add: image_subset_iff) apply (simp add: image_subset_iff) apply (cut_tac tr=tr and i="Suc (Suc (i + ja))" in bottom_addr_only) apply (simp add: image_subset_iff) apply (simp add: image_subset_iff) apply (clarsimp simp: continuing_def split: list.split next_node.split) apply (case_tac "drop 2 (the (tr (Suc (i + ja))))", simp_all) apply (frule_tac i="Suc (i + ja)" in exec_trace_step_cases) apply (frule_tac i="Suc (i + ja)" in exec_trace_invariant, simp) apply (auto simp: all_exec_graph_step_cases exec_graph_invariant_Cons
             split: graph_function.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_addr tr i = Some (NextNode n); trace_addr tr j = Some nn; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fname \<and> Suc i < j \<and> (\<exists>st g. trace_drop_n (Suc i) 1 tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) 1 tr (j - Suc i) = None proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, g)]; tr j = Some [(nn, sta, ga)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname \<and> Suc i < j \<and> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, g)]; tr j = Some [(nn, sta, ga)]; exec_graph_invariant Gamma fn [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname \<and> Suc i < j \<and> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname \<and> Suc i < j \<and> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> Suc i < j \<and> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (2 subgoals):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> Suc i < j
 2. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j\<rbrakk> \<Longrightarrow> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (2 subgoals):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; j = Suc i\<rbrakk> \<Longrightarrow> False
 2. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j\<rbrakk> \<Longrightarrow> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (2 subgoals):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; tr i = Some [(NextNode n, st, fn)]; tr (Suc i) = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; j = Suc i; ([(NextNode n, st, fn)], [(nn, sta, ga)]) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> False
 2. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j\<rbrakk> \<Longrightarrow> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; i < j; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j\<rbrakk> \<Longrightarrow> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0\<rbrakk> \<Longrightarrow> (\<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (2 subgoals):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]
 2. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None proof (prove)
goal (2 subgoals):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr (j - Suc i) = None
 2. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (2 subgoals):
 1. \<And>st sta ga stb gb z. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; (\<lambda>ia. if \<forall>j<ia. (\<exists>y. tr (Suc (i + j)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + j))))))) then map_option (rev \<circ> drop (Suc 0) \<circ> rev) (tr (ia + Suc i)) else None) \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; \<forall>ja<j - Suc (Suc i). (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))); tr (j - Suc 0) = Some z; drop (Suc 0) (rev z) = [(Ret, stb, gb)]\<rbrakk> \<Longrightarrow> \<exists>ja<j - Suc i. tr (Suc (i + ja)) = None \<or> \<not> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja)))))))
 2. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - 1) \<in> {None}\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - 1) \<in> {None}; trace_bottom_addr tr (j - 1) \<in> {Some (NextNode n)}\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (1 subgoal):
 1. \<And>st sta g ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; g = fn; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - 1) \<in> {None}; trace_bottom_addr tr (j - 1) \<in> {Some (NextNode n)}; tr (j - 1) = None \<and> tr (Suc (j - 1)) = None \<or> (\<exists>state. tr (j - 1) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (j - 1)) = None) \<or> tr (j - 1) \<noteq> None \<and> tr (Suc (j - 1)) \<noteq> None \<and> (the (tr (j - 1)), the (tr (Suc (j - 1)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (1 subgoal):
 1. \<And>st sta ga y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, sta, ga)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); (y, [(nn, sta, ga)]) \<in> exec_graph_step Gamma; tr (j - Suc 0) = Some y\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (1 subgoal):
 1. \<And>st sta ga y a aa b x22 ab ac ba x22a x1 x2 x1a x2a x3 x4 x2b x31 x32 x33 x34 x2c x1b x2d x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a)\<rbrakk> \<Longrightarrow> \<exists>st g. trace_drop_n (Suc i) (Suc 0) tr (j - Suc (Suc i)) = Some [(Ret, st, g)] proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a)\<rbrakk> \<Longrightarrow> (\<forall>ja<j - Suc (Suc i). (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja)))))))) \<and> (\<exists>st g z. tr (Suc (j - Suc (Suc i) + i)) = Some z \<and> drop (Suc 0) (rev z) = [(Ret, st, g)]) proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i)\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))) proof (prove)
goal (3 subgoals):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i)\<rbrakk> \<Longrightarrow> trace_addr tr (Suc (i + ja)) = None
 2. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i)\<rbrakk> \<Longrightarrow> trace_bottom_addr tr (Suc (i + ja)) = Some (?nn859 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja)
 3. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> ?nn859 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))) proof (prove)
goal (2 subgoals):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i)\<rbrakk> \<Longrightarrow> trace_bottom_addr tr (Suc (i + ja)) = Some (?nn859 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja)
 2. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> ?nn859 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))) proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))) proof (prove)
goal (3 subgoals):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> trace_addr tr (Suc (Suc (i + ja))) = None
 2. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> trace_bottom_addr tr (Suc (Suc (i + ja))) = Some (?nn1107 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja)
 3. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs)); \<exists>x x' xs. tr (Suc (Suc (i + ja))) = Some (x # x' # xs) \<and> ?nn1107 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))) proof (prove)
goal (2 subgoals):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> trace_bottom_addr tr (Suc (Suc (i + ja))) = Some (?nn1107 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja)
 2. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs)); \<exists>x x' xs. tr (Suc (Suc (i + ja))) = Some (x # x' # xs) \<and> ?nn1107 st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))) proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (NextNode n)}; tr i = Some [(NextNode n, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (NextNode n); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); \<exists>x x' xs. tr (Suc (i + ja)) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs)); \<exists>x x' xs. tr (Suc (Suc (i + ja))) = Some (x # x' # xs) \<and> NextNode n = fst (last (x' # xs))\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc (i + ja)) = Some y) \<and> continuing (rev (drop (Suc 0) (rev (the (tr (Suc (i + ja))))))) proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja a ab ad ae bb bc af ag ah ai bd be xs xsa aj ak bf. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some (fst (if xs = [] then (af, ah, bd) else last xs))}; tr i = Some [(fst (if xs = [] then (af, ah, bd) else last xs), st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some (fst (if xs = [] then (af, ah, bd) else last xs)); tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); tr (Suc (i + ja)) = Some ((a, ad, bb) # (af, ah, bd) # xs); fst (if xsa = [] then (ag, ai, be) else last xsa) = fst (if xs = [] then (af, ah, bd) else last xs); tr (Suc (Suc (i + ja))) = Some ((ab, ae, bc) # (ag, ai, be) # xsa); NextNode n = fst (if xs = [] then (af, ah, bd) else last xs)\<rbrakk> \<Longrightarrow> (aj = Ret \<longrightarrow> drop (Suc 0) (rev xs) @ drop (Suc 0 - length xs) [(af, ah, bd), (a, ad, bb)] \<noteq> [(Ret, ak, bf)]) \<and> (aj = Err \<longrightarrow> drop (Suc 0) (rev xs) @ drop (Suc 0 - length xs) [(af, ah, bd), (a, ad, bb)] \<noteq> [(Err, ak, bf)]) proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja a ab ad ae bb bc af ag ah ai bd be xs xsa aj ak bf. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some af}; tr i = Some [(af, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some af; tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); tr (Suc (i + ja)) = Some [(a, ad, bb), (af, ah, bd)]; fst (if xsa = [] then (ag, ai, be) else last xsa) = af; tr (Suc (Suc (i + ja))) = Some ((ab, ae, bc) # (ag, ai, be) # xsa); NextNode n = af; xs = []\<rbrakk> \<Longrightarrow> (aj = Ret \<longrightarrow> ad = ak \<longrightarrow> a = Ret \<longrightarrow> bb \<noteq> bf) \<and> (aj = Err \<longrightarrow> ad = ak \<longrightarrow> a = Err \<longrightarrow> bb \<noteq> bf) proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja a ab ad ae bb bc af ag ah ai bd be xs xsa aj ak bf. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some af}; tr i = Some [(af, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some af; tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); tr (Suc (i + ja)) = Some [(a, ad, bb), (af, ah, bd)]; fst (if xsa = [] then (ag, ai, be) else last xsa) = af; tr (Suc (Suc (i + ja))) = Some ((ab, ae, bc) # (ag, ai, be) # xsa); NextNode n = af; xs = []; tr (Suc (i + ja)) = None \<and> tr (Suc (Suc (i + ja))) = None \<or> (\<exists>state. tr (Suc (i + ja)) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (Suc (i + ja))) = None) \<or> tr (Suc (i + ja)) \<noteq> None \<and> tr (Suc (Suc (i + ja))) \<noteq> None \<and> (the (tr (Suc (i + ja))), the (tr (Suc (Suc (i + ja))))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> (aj = Ret \<longrightarrow> ad = ak \<longrightarrow> a = Ret \<longrightarrow> bb \<noteq> bf) \<and> (aj = Err \<longrightarrow> ad = ak \<longrightarrow> a = Err \<longrightarrow> bb \<noteq> bf) proof (prove)
goal (1 subgoal):
 1. \<And>st aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a ja a ab ad ae bb bc af ag ah ai bd be xs xsa aj ak bf. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; nn \<noteq> Err; trace_addr tr ` {Suc i..<j} \<subseteq> {None}; trace_bottom_addr tr ` {Suc i..<j} \<subseteq> {Some af}; tr i = Some [(af, st, fn)]; tr j = Some [(nn, return_vars x2d x34 aa ac, ba)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; Suc i < j; Suc (j - 2) = j - Suc 0; trace_addr tr (j - Suc 0) = None; trace_bottom_addr tr (j - Suc 0) = Some af; tr (j - Suc 0) = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a); ja < j - Suc (Suc i); tr (Suc (i + ja)) = Some [(a, ad, bb), (af, ah, bd)]; fst (if xsa = [] then (ag, ai, be) else last xsa) = af; tr (Suc (Suc (i + ja))) = Some ((ab, ae, bc) # (ag, ai, be) # xsa); NextNode n = af; xs = []; tr (Suc (i + ja)) = None \<and> tr (Suc (Suc (i + ja))) = None \<or> (\<exists>state. tr (Suc (i + ja)) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (Suc (i + ja))) = None) \<or> tr (Suc (i + ja)) \<noteq> None \<and> tr (Suc (Suc (i + ja))) \<noteq> None \<and> (the (tr (Suc (i + ja))), the (tr (Suc (Suc (i + ja))))) \<in> exec_graph_step Gamma; exec_graph_invariant Gamma fn ((a, ad, bb) # (af, ah, bd) # xs)\<rbrakk> \<Longrightarrow> (aj = Ret \<longrightarrow> ad = ak \<longrightarrow> a = Ret \<longrightarrow> bb \<noteq> bf) \<and> (aj = Err \<longrightarrow> ad = ak \<longrightarrow> a = Err \<longrightarrow> bb \<noteq> bf) proof (prove)
goal:
No subgoals!