theory GraphProof

lemma visit_Cond:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> function_graph gf = graph
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> graph n = Some (Cond l r cond)
    \<Longrightarrow> converse (reachable_step graph) `` {nn} \<subseteq> {NextNode n}
    \<Longrightarrow> nn \<noteq> NextNode (entry_point gf)
    \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y})
    \<Longrightarrow> (l, NextNode n) \<notin> rtrancl (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})
    \<Longrightarrow> (r, NextNode n) \<notin> rtrancl (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})
    \<Longrightarrow> visit tr nn restrs = option_guard (\<lambda>st. (nn = l \<and> cond st) \<or> (nn = r \<and> \<not> cond st))
        (visit tr (NextNode n) (pred_restrs' n restrs))" apply (cases "visit tr (NextNode n) (pred_restrs' n restrs)"; simp) apply (clarsimp simp: visit_eqs) apply (frule(5) visit_immediate_pred) apply (clarsimp simp: pred_restrs) apply (frule(3) exec_trace_non_Call, simp) apply simp apply (clarsimp simp: visit_eqs simp del: imp_disjL) apply (frule trace_addr_SomeD, clarsimp simp del: imp_disjL) apply (frule_tac i=i in exec_trace_step_cases) apply (frule(1) exec_trace_invariant) apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons
              simp del: imp_disjL) apply (intro conjI impI) apply (rule_tac x="Suc i" in exI) apply (clarsimp simp: pred_restrs trace_bottom_addr_def) apply (rule conjI, simp add: trace_addr_def) apply clarsimp apply (frule(3) visit_immediate_pred, simp, simp) apply (clarsimp simp: pred_restrs) apply (frule(2) exec_trace_non_Call, simp+)[1] apply (rule_tac x="Suc i" in exI) apply (clarsimp simp: pred_restrs trace_bottom_addr_def) apply (rule conjI, simp add: trace_addr_def) apply clarsimp apply (frule(3) visit_immediate_pred, simp, simp) apply (clarsimp simp: pred_restrs) apply (frule(2) exec_trace_non_Call, simp+)[1] apply clarsimp apply (frule(3) visit_immediate_pred, simp, simp) apply (clarsimp simp: pred_restrs) apply (frule(2) exec_trace_non_Call, simp+) apply (drule(3) restrs_single_visit2, simp+) apply (clarsimp simp: reachable_step_def[THEN eqset_imp_iff] dest!: tranclD) apply auto[1] apply (clarsimp dest!: trace_addr_SomeD split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*\<rbrakk> \<Longrightarrow> visit tr nn restrs = option_guard (\<lambda>st. nn = l \<and> cond st \<or> nn = r \<and> \<not> cond st) (visit tr (NextNode n) (pred_restrs' n restrs)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; visit tr (NextNode n) (pred_restrs' n restrs) = None\<rbrakk> \<Longrightarrow> visit tr nn restrs = None
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> (nn = l \<and> cond a \<longrightarrow> visit tr l restrs = Some a) \<and> (nn = r \<and> \<not> cond a \<longrightarrow> visit tr r restrs = Some a) \<and> ((nn = l \<longrightarrow> \<not> cond a) \<and> (nn = r \<longrightarrow> cond a) \<longrightarrow> visit tr nn restrs = None) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; 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 gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> (nn = l \<and> cond a \<longrightarrow> visit tr l restrs = Some a) \<and> (nn = r \<and> \<not> cond a \<longrightarrow> visit tr r restrs = Some a) \<and> ((nn = l \<longrightarrow> \<not> cond a) \<and> (nn = r \<longrightarrow> cond a) \<longrightarrow> visit tr nn restrs = None) proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; trace_addr tr i = Some nn; restrs_condition tr restrs i; \<exists>i' nn'. i = Suc i' \<and> nn' \<in> {NextNode n} \<and> trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> (nn = l \<and> cond a \<longrightarrow> visit tr l restrs = Some a) \<and> (nn = r \<and> \<not> cond a \<longrightarrow> visit tr r restrs = Some a) \<and> ((nn = l \<longrightarrow> \<not> cond a) \<and> (nn = r \<longrightarrow> cond a) \<longrightarrow> visit tr nn restrs = None) proof (prove)
goal (2 subgoals):
 1. \<And>i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; trace_addr tr (Suc i') = Some nn; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> (nn = l \<and> cond a \<longrightarrow> visit tr l restrs = Some a) \<and> (nn = r \<and> \<not> cond a \<longrightarrow> visit tr r restrs = Some a) \<and> ((nn = l \<longrightarrow> \<not> cond a) \<and> (nn = r \<longrightarrow> cond a) \<longrightarrow> visit tr nn restrs = None) proof (prove)
goal (2 subgoals):
 1. \<And>i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (pred_restrs' n restrs) i; graph = function_graph gf; trace_addr tr (Suc i') = Some nn; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> (nn = l \<and> cond a \<longrightarrow> visit tr l restrs = Some a) \<and> (nn = r \<and> \<not> cond a \<longrightarrow> visit tr r restrs = Some a) \<and> ((nn = l \<longrightarrow> \<not> cond a) \<and> (nn = r \<longrightarrow> cond a) \<longrightarrow> visit tr nn restrs = None) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; visit tr (NextNode n) (pred_restrs' n restrs) = Some a\<rbrakk> \<Longrightarrow> (nn = l \<and> cond a \<longrightarrow> visit tr l restrs = Some a) \<and> (nn = r \<and> \<not> cond a \<longrightarrow> visit tr r restrs = Some a) \<and> ((nn = l \<longrightarrow> \<not> cond a) \<and> (nn = r \<longrightarrow> cond a) \<longrightarrow> visit tr nn restrs = None) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; graph = function_graph gf; 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> (nn = l \<and> cond (fst (snd (hd (the (tr i))))) \<longrightarrow> (\<exists>ia. restrs_condition tr restrs ia \<and> trace_addr tr ia = Some l \<and> fst (snd (hd (the (tr i)))) = fst (snd (hd (the (tr ia)))) \<and> (\<forall>j<ia. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l))) \<and> (nn = r \<and> \<not> cond (fst (snd (hd (the (tr i))))) \<longrightarrow> (\<exists>ia. restrs_condition tr restrs ia \<and> trace_addr tr ia = Some r \<and> fst (snd (hd (the (tr i)))) = fst (snd (hd (the (tr ia)))) \<and> (\<forall>j<ia. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r))) \<and> ((nn = l \<longrightarrow> \<not> cond (fst (snd (hd (the (tr i)))))) \<and> (nn = r \<longrightarrow> cond (fst (snd (hd (the (tr i)))))) \<longrightarrow> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; graph = function_graph gf; 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> (nn = l \<and> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some l \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l))) \<and> (nn = r \<and> \<not> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r))) \<and> ((nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st) \<longrightarrow> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; graph = function_graph gf; 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)]; 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> (nn = l \<and> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some l \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l))) \<and> (nn = r \<and> \<not> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r))) \<and> ((nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st) \<longrightarrow> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)) proof (prove)
goal (1 subgoal):
 1. \<And>i st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; function_graph gf n = Some (node.Cond l r cond); (reachable_step' gf)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode (entry_point gf); \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step' gf \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; graph = function_graph gf; 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)]; 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; exec_graph_invariant Gamma fn [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> (nn = l \<and> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some l \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l))) \<and> (nn = r \<and> \<not> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r))) \<and> ((nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st) \<longrightarrow> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)) proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4\<rbrakk> \<Longrightarrow> (nn = l \<and> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some l \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l))) \<and> (nn = r \<and> \<not> cond st \<longrightarrow> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r))) \<and> ((nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st) \<longrightarrow> (\<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i)) proof (prove)
goal (3 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<and> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some l \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l)
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 3. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (3 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<and> cond st\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc i) \<and> trace_addr tr (Suc i) = Some l \<and> st = fst (snd (hd (the (tr (Suc i))))) \<and> (\<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l)
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 3. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (3 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {l} \<subseteq> {NextNode n}; l \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(l, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l; cond st\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = Some l \<and> (\<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l)
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 3. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (3 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {l} \<subseteq> {NextNode n}; l \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(l, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l; cond st\<rbrakk> \<Longrightarrow> \<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some l
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 3. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (3 subgoals):
 1. \<And>i st x1 x2 x4 j. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {l} \<subseteq> {NextNode n}; l \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(l, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l; cond st; j < Suc i; restrs_condition tr restrs j; trace_addr tr j = Some l\<rbrakk> \<Longrightarrow> False
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 3. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (3 subgoals):
 1. \<And>i st x1 x2 x4 j. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {l} \<subseteq> {NextNode n}; l \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(l, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l; cond st; j < Suc i; restrs_condition tr restrs j; trace_addr tr j = Some l; \<exists>i' nn'. j = Suc i' \<and> nn' \<in> {NextNode n} \<and> trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> False
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 3. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (3 subgoals):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {l} \<subseteq> {NextNode n}; l \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(l, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l; cond st; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs' n restrs) i'; trace_addr tr (Suc i') = Some l; trace_bottom_addr tr i' = Some (NextNode n); i' < i\<rbrakk> \<Longrightarrow> False
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 3. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some r \<and> st = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r \<and> \<not> cond st\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc i) \<and> trace_addr tr (Suc i) = Some r \<and> st = fst (snd (hd (the (tr (Suc i))))) \<and> (\<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {r} \<subseteq> {NextNode n}; r \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r; \<not> cond st\<rbrakk> \<Longrightarrow> trace_addr tr (Suc i) = Some r \<and> (\<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r)
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {r} \<subseteq> {NextNode n}; r \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r; \<not> cond st\<rbrakk> \<Longrightarrow> \<forall>j<Suc i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some r
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4 j. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {r} \<subseteq> {NextNode n}; r \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r; \<not> cond st; j < Suc i; restrs_condition tr restrs j; trace_addr tr j = Some r\<rbrakk> \<Longrightarrow> False
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4 j. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {r} \<subseteq> {NextNode n}; r \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r; \<not> cond st; j < Suc i; restrs_condition tr restrs j; trace_addr tr j = Some r; \<exists>i' nn'. j = Suc i' \<and> nn' \<in> {NextNode n} \<and> trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> False
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {r} \<subseteq> {NextNode n}; r \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = r; \<not> cond st; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs' n restrs) i'; trace_addr tr (Suc i') = Some r; trace_bottom_addr tr i' = Some (NextNode n); i' < i\<rbrakk> \<Longrightarrow> False
 2. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; (nn = l \<longrightarrow> \<not> cond st) \<and> (nn = r \<longrightarrow> cond st)\<rbrakk> \<Longrightarrow> \<forall>i. trace_addr tr i = Some nn \<longrightarrow> \<not> restrs_condition tr restrs i proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 ia. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr ia = Some nn; restrs_condition tr restrs ia\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 ia. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr ia = Some nn; restrs_condition tr restrs ia; \<exists>i' nn'. ia = Suc i' \<and> nn' \<in> {NextNode n} \<and> trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr (Suc i') = Some nn; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr (Suc i') = Some nn; restrs_condition tr (pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr (Suc i') = Some nn; restrs_condition tr (pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n)\<rbrakk> \<Longrightarrow> (NextNode n, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>+
 2. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr (Suc i') = Some nn; restrs_condition tr (pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n); i = i'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>i st x1 x2 x4 i' z. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr (Suc i') = Some nn; restrs_condition tr (pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n); (z, NextNode n) \<in> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; z = l \<or> z = r; NextNode n \<notin> set cuts\<rbrakk> \<Longrightarrow> False
 2. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr (Suc i') = Some nn; restrs_condition tr (pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n); i = i'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i st x1 x2 x4 i'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 graph x4); wf_graph_function (GraphFunction x1 x2 graph x4) ilen olen; graph n = Some (node.Cond l r cond); (reachable_step graph)\<inverse> `` {nn} \<subseteq> {NextNode n}; nn \<noteq> NextNode x4; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs' n restrs x \<subseteq> {y}); (l, NextNode n) \<notin> (reachable_step graph \<inter> {(x, y). x \<notin> set cuts})\<^sup>*; (r, NextNode n) \<notin> (reachable_step graph \<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)]; tr (Suc i) = Some [(if cond st then l else r, st, fn)]; gf = GraphFunction x1 x2 graph x4; nn = l \<longrightarrow> \<not> cond st; nn = r \<longrightarrow> cond st; trace_addr tr (Suc i') = Some nn; restrs_condition tr (pred_restrs' n restrs) i'; trace_bottom_addr tr i' = Some (NextNode n); trace_addr tr i' = Some (NextNode n); i = i'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!