theory GraphProof

lemma visit_Call:
  "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> length inputs = length (function_inputs f')
    \<Longrightarrow> converse (reachable_step' f) `` {nn} \<subseteq> {NextNode n}
    \<Longrightarrow> nn \<noteq> NextNode (entry_point f) \<Longrightarrow> nn \<noteq> Err
    \<Longrightarrow> (nn, NextNode n) \<notin> rtrancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})
    \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})
    \<Longrightarrow> let v = visit tr nn restrs; v' = visit tr (NextNode n) (pred_restrs' n restrs);
            tr' = function_call_trace n (pred_restrs' n restrs) tr
        in function_call_trace_embed v' tr tr' Gamma fname inputs
            \<and> v = option_map (\<lambda>st. return_vars (function_outputs f') outputs
                    (fst (snd (hd (the (trace_end (the tr')))))) st)
            (option_guard (\<lambda>_. tr' \<noteq> None \<and> trace_end (the tr') \<noteq> None
                \<and> fst (hd (the (trace_end (the tr')))) = Ret) v')" apply (cases "visit tr (NextNode n) (pred_restrs' n restrs)",
         simp_all split del: if_split) apply (clarsimp simp: visit_eqs function_call_trace_embed_def) apply (rule context_conjI) apply (clarsimp simp: function_call_trace_def pc_def visit_eqs) apply clarsimp apply (frule(6) visit_extended_pred) apply clarsimp apply (drule visit_eqs[THEN iffD1]) apply (drule(2) visit_Call_loop_lemma) apply (frule_tac nn="NextNode n" in pred_restrs_cut2) apply (clarsimp simp: Let_def split del: if_split) apply (frule trace_addr_SomeD, clarsimp split del: if_split) apply (frule(1) exec_trace_invariant) apply (clarsimp simp: exec_graph_invariant_Cons split del: if_split) apply (frule(4) exec_trace_drop_n) apply (clarsimp simp: function_call_trace_eq visit_eqs Let_def
              simp del: imp_disjL split del: if_split) apply (rule conjI) apply (clarsimp simp: function_call_trace_embed_def simp del: map_option_eq_Some) apply (rule conjI, blast intro: trace_end_trace_drop_n_None) apply (rule conjI, metis trace_end_trace_drop_n_Err) apply (clarsimp simp: trace_drop_n_def) apply (frule_tac i=i in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def init_state_def init_vars_def
                  split: graph_function.split_asm dest!: trace_addr_SomeD) apply (simp del: imp_disjL) apply (rule conjI) apply (clarsimp simp: visit_eqs) apply (drule(1) exec_trace_end_SomeD, clarsimp) apply (frule(4) exec_trace_drop_n_rest[rule_format], simp) apply (frule_tac i="Suc i + na" in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def split: graph_function.split_asm) apply (subgoal_tac "restrs_condition tr restrs (Suc (Suc i + na))") apply (rule exI, rule conjI, assumption) apply (clarsimp simp: trace_addr_SomeI) apply (drule(2) restrs_single_visit2[OF trace_addr_SomeI, OF exI], simp+)[1] apply (rule_tac i="Suc i" in restrs_condition_no_change) apply (simp add: pred_restrs[unfolded trace_bottom_addr_def]) apply simp apply clarsimp apply (rule ccontr, clarsimp dest!: trace_addr_SomeD) apply (case_tac "trace_drop_n (Suc i) 1 tr (k - Suc i)") apply simp apply (drule(1) exec_trace_None_dom_subset)+ apply auto[1] apply (frule(2) exec_trace_drop_n_rest[rule_format], fastforce, assumption+) apply (clarsimp simp: exec_trace_Nil) apply (intro impI allI notI conjI) apply (clarsimp simp: visit_eqs) apply (rename_tac k) apply (frule(6) visit_extended_pred) apply clarsimp apply (drule(8) restrs_single_visit[rotated 3]) apply clarsimp apply (frule(10) extended_pred_trace_drop_n) apply (clarsimp simp: trace_end_exec_SomeI Suc_diff_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})\<rbrakk> \<Longrightarrow> let v = visit tr nn restrs; v' = visit tr (NextNode n) (pred_restrs' n restrs); tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> v = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (option_guard (\<lambda>_. tr' \<noteq> None \<and> trace_end (the tr') \<noteq> None \<and> fst (hd (the (trace_end (the tr')))) = Ret) v') proof (prove)
goal (2 subgoals):
 1. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = None\<rbrakk> \<Longrightarrow> function_call_trace_embed None tr (function_call_trace n (pred_restrs' n restrs) tr) Gamma fname inputs \<and> visit tr nn restrs = None
 2. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (2 subgoals):
 1. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> function_call_trace n (pred_restrs' n restrs) tr = None \<and> (\<forall>tr''. function_call_trace n (pred_restrs' n restrs) tr = Some tr'' \<longrightarrow> tr'' \<in> exec_trace Gamma fname \<and> (trace_end tr'' = None \<longrightarrow> trace_end tr = None) \<and> ((\<exists>z. trace_end tr'' = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err)) \<and> tr'' 0 = Some [init_state fname f' (map (\<lambda>i. i (the None)) inputs)]) \<and> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)
 2. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (3 subgoals):
 1. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i\<rbrakk> \<Longrightarrow> function_call_trace n (pred_restrs' n restrs) tr = None
 2. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; function_call_trace n (pred_restrs' n restrs) tr = None\<rbrakk> \<Longrightarrow> (\<forall>tr''. function_call_trace n (pred_restrs' n restrs) tr = Some tr'' \<longrightarrow> tr'' \<in> exec_trace Gamma fname \<and> (trace_end tr'' = None \<longrightarrow> trace_end tr = None) \<and> ((\<exists>z. trace_end tr'' = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err)) \<and> tr'' 0 = Some [init_state fname f' (map (\<lambda>i. i (the None)) inputs)]) \<and> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)
 3. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (2 subgoals):
 1. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; function_call_trace n (pred_restrs' n restrs) tr = None\<rbrakk> \<Longrightarrow> (\<forall>tr''. function_call_trace n (pred_restrs' n restrs) tr = Some tr'' \<longrightarrow> tr'' \<in> exec_trace Gamma fname \<and> (trace_end tr'' = None \<longrightarrow> trace_end tr = None) \<and> ((\<exists>z. trace_end tr'' = Some z \<and> fst (hd z) = Err) \<longrightarrow> (\<exists>z. trace_end tr = Some z \<and> fst (hd z) = Err)) \<and> tr'' 0 = Some [init_state fname f' (map (\<lambda>i. i (the None)) inputs)]) \<and> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)
 2. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; function_call_trace n (pred_restrs' n restrs) tr = None; trace_addr tr i = Some nn; restrs_condition tr restrs i\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; function_call_trace n (pred_restrs' n restrs) tr = None; trace_addr tr i = Some nn; restrs_condition tr restrs i; \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> {NextNode n} \<and> j < i \<and> trace_addr tr ` {Suc j..<i} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<i} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; (nn, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<exists>i. restrs_condition tr (pred_restrs' n restrs) i \<and> trace_addr tr i = Some (NextNode n) \<and> a = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n))\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<exists>i. restrs_condition tr (pred_restrs' n restrs) i \<and> trace_addr tr i = Some (NextNode n) \<and> a = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n)); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+ \<and> (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<exists>i. restrs_condition tr (pred_restrs' n restrs) i \<and> trace_addr tr i = Some (NextNode n) \<and> a = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n)); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+ \<and> (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y})\<rbrakk> \<Longrightarrow> let v' = Some a; tr' = function_call_trace n (pred_restrs' n restrs) tr in function_call_trace_embed v' tr tr' Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the tr'))))))) (if (\<exists>y. tr' = Some y) \<and> (\<exists>y. trace_end (the tr') = Some y) \<and> fst (hd (the (trace_end (the tr')))) = Ret then v' else None) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> function_call_trace_embed (Some (fst (snd (hd (the (tr i)))))) tr (function_call_trace n (pred_restrs' n restrs) tr) Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)))))))) (if (\<exists>y. function_call_trace n (pred_restrs' n restrs) tr = Some y) \<and> (\<exists>y. trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)) = Some y) \<and> fst (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr))))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> function_call_trace_embed (Some st) tr (function_call_trace n (pred_restrs' n restrs) tr) Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)))))))) (if (\<exists>y. function_call_trace n (pred_restrs' n restrs) tr = Some y) \<and> (\<exists>y. trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)) = Some y) \<and> fst (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr))))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, g)]; exec_graph_invariant Gamma fn [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> function_call_trace_embed (Some st) tr (function_call_trace n (pred_restrs' n restrs) tr) Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)))))))) (if (\<exists>y. function_call_trace n (pred_restrs' n restrs) tr = Some y) \<and> (\<exists>y. trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)) = Some y) \<and> fst (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr))))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]\<rbrakk> \<Longrightarrow> function_call_trace_embed (Some st) tr (function_call_trace n (pred_restrs' n restrs) tr) Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)))))))) (if (\<exists>y. function_call_trace n (pred_restrs' n restrs) tr = Some y) \<and> (\<exists>y. trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)) = Some y) \<and> fst (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr))))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> function_call_trace_embed (Some st) tr (function_call_trace n (pred_restrs' n restrs) tr) Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)))))))) (if (\<exists>y. function_call_trace n (pred_restrs' n restrs) tr = Some y) \<and> (\<exists>y. trace_end (the (function_call_trace n (pred_restrs' n restrs) tr)) = Some y) \<and> fst (hd (the (trace_end (the (function_call_trace n (pred_restrs' n restrs) tr))))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> function_call_trace_embed (Some st) tr (Some (trace_drop_n (Suc i) (Suc 0) tr)) Gamma fname inputs \<and> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> function_call_trace_embed (Some st) tr (Some (trace_drop_n (Suc i) (Suc 0) tr)) Gamma fname inputs
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> (trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<longrightarrow> trace_end tr = None) \<and> (map_option (fst \<circ> hd) (trace_end (trace_drop_n (Suc i) (Suc 0) tr)) = Some Err \<longrightarrow> map_option (fst \<circ> hd) (trace_end tr) = Some Err) \<and> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [init_state fname f' (map (\<lambda>i. i st) inputs)]
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> (map_option (fst \<circ> hd) (trace_end (trace_drop_n (Suc i) (Suc 0) tr)) = Some Err \<longrightarrow> map_option (fst \<circ> hd) (trace_end tr) = Some Err) \<and> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [init_state fname f' (map (\<lambda>i. i st) inputs)]
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [init_state fname f' (map (\<lambda>i. i st) inputs)]
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; (\<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\<rbrakk> \<Longrightarrow> \<exists>z. tr (Suc i) = Some z \<and> drop (Suc 0) (rev z) = [init_state fname f' (map (\<lambda>i. i st) inputs)]
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; (\<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; 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>z. tr (Suc i) = Some z \<and> drop (Suc 0) (rev z) = [init_state fname f' (map (\<lambda>i. i st) inputs)]
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> visit tr nn restrs = map_option (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr))))))) (if (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret then Some (fst (snd (hd (the (tr i))))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> ((\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret \<longrightarrow> visit tr nn restrs = Some (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))))) st)) \<and> (trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None) proof (prove)
goal (2 subgoals):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> (\<exists>y. trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y) \<and> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) = Ret \<longrightarrow> visit tr nn restrs = Some (return_vars (function_outputs f') outputs (fst (snd (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))))) st)
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st 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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; fst (hd y) = Ret; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some y\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> return_vars (function_outputs f') outputs (fst (snd (hd y))) st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn)
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> return_vars (function_outputs f') outputs sta st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn)
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc i + na) = Some ([(Ret, sta, g)] @ [(NextNode n, st, fn)])\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> return_vars (function_outputs f') outputs sta st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn)
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc i + na) = Some ([(Ret, sta, g)] @ [(NextNode n, st, fn)]); 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> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> return_vars (function_outputs f') outputs sta st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn)
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> return_vars x2a outputs sta st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn)
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (3 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; restrs_condition tr restrs (Suc (Suc i + na))\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some nn \<and> return_vars x2a outputs sta st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn)
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc (Suc i + na))
 3. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (3 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; restrs_condition tr restrs (Suc (Suc i + na))\<rbrakk> \<Longrightarrow> trace_addr tr (Suc (Suc i + na)) = Some nn \<and> return_vars x2a outputs sta st = fst (snd (hd (the (tr (Suc (Suc i + na)))))) \<and> (\<forall>j<Suc (Suc i + na). restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some nn)
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc (Suc i + na))
 3. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (3 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a j. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; restrs_condition tr restrs (Suc (Suc (i + na))); j < Suc (Suc (i + na)); restrs_condition tr restrs j; trace_addr tr j = Some nn\<rbrakk> \<Longrightarrow> False
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc (Suc i + na))
 3. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc (Suc i + na))
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (4 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc i)
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> Suc i \<le> Suc (Suc i + na)
 3. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> \<forall>k\<in>{Suc i..<Suc (Suc i + na)}. trace_addr tr k = None
 4. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (3 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> Suc i \<le> Suc (Suc i + na)
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> \<forall>k\<in>{Suc i..<Suc (Suc i + na)}. trace_addr tr k = None
 3. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]\<rbrakk> \<Longrightarrow> \<forall>k\<in>{Suc i..<Suc (Suc i + na)}. trace_addr tr k = None
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na))\<rbrakk> \<Longrightarrow> trace_addr tr k = None
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]\<rbrakk> \<Longrightarrow> False
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (3 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; trace_drop_n (Suc i) 1 tr (k - Suc i) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; trace_drop_n (Suc i) 1 tr (k - Suc i) = Some a\<rbrakk> \<Longrightarrow> False
 3. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (3 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; trace_drop_n (Suc i) (Suc 0) tr (k - Suc i) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; trace_drop_n (Suc i) 1 tr (k - Suc i) = Some a\<rbrakk> \<Longrightarrow> False
 3. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (3 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; dom (trace_drop_n (Suc i) (Suc 0) tr) \<subseteq> {..<Suc na}; dom (trace_drop_n (Suc i) (Suc 0) tr) \<subseteq> {..<k - Suc i}\<rbrakk> \<Longrightarrow> False
 2. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; trace_drop_n (Suc i) 1 tr (k - Suc i) = Some a\<rbrakk> \<Longrightarrow> False
 3. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; trace_drop_n (Suc i) 1 tr (k - Suc i) = Some a\<rbrakk> \<Longrightarrow> False
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (2 subgoals):
 1. \<And>i st na sta g x1 x2 x3 x4 x1a x2a x3a x4a k y stc gb a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); wf_graph_function (GraphFunction x1 x2 x3 x4) ilen olen; x3 n = Some (node.Call nn fname inputs outputs); Gamma fname = Some (GraphFunction x1a x2a x3a x4a); length inputs = length x1a; (reachable_step x3)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step x3 \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, sta, g)]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None; tr (Suc (i + na)) = Some [(Ret, sta, g), (NextNode n, st, fn)]; f = GraphFunction x1 x2 x3 x4; f' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + na))) = Some [(nn, return_vars x2a outputs sta st, fn)]; Suc i \<le> k; k < Suc (Suc (i + na)); tr i = Some [(NextNode n, st, fn)]; tr k = Some [(y, stc, gb)]; trace_drop_n (Suc i) 1 tr (k - Suc i) = Some a; tr (Suc i + (k - Suc i)) = Some (a @ [(NextNode n, st, fn)])\<rbrakk> \<Longrightarrow> False
 2. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (1 subgoal):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname\<rbrakk> \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret \<longrightarrow> visit tr nn restrs = None proof (prove)
goal (1 subgoal):
 1. \<And>i st. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret\<rbrakk> \<Longrightarrow> visit tr nn restrs = None proof (prove)
goal (1 subgoal):
 1. \<And>i st ia. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret; trace_addr tr ia = Some nn; restrs_condition tr restrs ia\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st k. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret; trace_addr tr k = Some nn; restrs_condition tr restrs k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st k. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret; trace_addr tr k = Some nn; restrs_condition tr restrs k; \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> {NextNode n} \<and> j < k \<and> trace_addr tr ` {Suc j..<k} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<k} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st k j. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; trace_addr tr i = Some (NextNode n); \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret; trace_addr tr k = Some nn; restrs_condition tr restrs k; trace_addr tr j = Some (NextNode n); j < k; trace_addr tr ` {Suc j..<k} \<subseteq> {None}; trace_bottom_addr tr ` {Suc j..<k} \<subseteq> {Some (NextNode n)}; restrs_condition tr (pred_restrs' n restrs) j\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st k j. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; restrs_condition tr (pred_restrs' n restrs) i; \<forall>j<i. restrs_condition tr (pred_restrs' n restrs) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n); tr i = Some [(NextNode n, st, fn)]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc i) (Suc 0) tr)))) \<noteq> Ret; trace_addr tr k = Some nn; restrs_condition tr restrs k; trace_addr tr j = Some (NextNode n); j < k; trace_addr tr ` {Suc j..<k} \<subseteq> {None}; trace_bottom_addr tr ` {Suc j..<k} \<subseteq> {Some (NextNode n)}; restrs_condition tr (pred_restrs' n restrs) j; i = j\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>st k j. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; \<forall>ja<j. restrs_condition tr (pred_restrs' n restrs) ja \<longrightarrow> trace_addr tr ja \<noteq> Some (NextNode n); tr j = Some [(NextNode n, st, fn)]; trace_drop_n (Suc j) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc j) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc j) (Suc 0) tr)))) \<noteq> Ret; trace_addr tr k = Some nn; restrs_condition tr restrs k; trace_addr tr j = Some (NextNode n); j < k; trace_addr tr ` {Suc j..<k} \<subseteq> {None}; trace_bottom_addr tr ` {Suc j..<k} \<subseteq> {Some (NextNode n)}; restrs_condition tr (pred_restrs' n restrs) j\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>st k j. \<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'; length inputs = length (function_inputs f'); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point f); nn \<noteq> Err; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+; \<forall>ja<j. restrs_condition tr (pred_restrs' n restrs) ja \<longrightarrow> trace_addr tr ja \<noteq> Some (NextNode n); tr j = Some [(NextNode n, st, fn)]; trace_drop_n (Suc j) (Suc 0) tr \<in> exec_trace Gamma fname; trace_end (trace_drop_n (Suc j) (Suc 0) tr) = None \<or> fst (hd (the (trace_end (trace_drop_n (Suc j) (Suc 0) tr)))) \<noteq> Ret; trace_addr tr k = Some nn; restrs_condition tr restrs k; trace_addr tr j = Some (NextNode n); j < k; trace_addr tr ` {Suc j..<k} \<subseteq> {None}; trace_bottom_addr tr ` {Suc j..<k} \<subseteq> {Some (NextNode n)}; restrs_condition tr (pred_restrs' n restrs) j; trace_drop_n (Suc j) 1 tr \<in> exec_trace Gamma fname \<and> Suc j < k \<and> (\<exists>st g. trace_drop_n (Suc j) 1 tr (k - Suc (Suc j)) = Some [(Ret, st, g)]) \<and> trace_drop_n (Suc j) 1 tr (k - Suc j) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!