theory GraphProof

lemma reachable_trace_induct:
  "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f
    \<Longrightarrow> wf_graph_function f ilen olen
    \<Longrightarrow> trace_addr tr i = Some nn
    \<Longrightarrow> i + k \<le> j
    \<Longrightarrow> (\<forall>nn'. trace_bottom_addr tr (i + k) = Some nn'
        \<longrightarrow> (Some nn' \<in> trace_addr tr ` {i .. i + k})
        \<and> (nn, nn') \<in> rtrancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}})
        \<and> (k \<noteq> 0 \<and> trace_addr tr (i + k) \<noteq> None
        \<longrightarrow> (nn, nn') \<in> trancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}})))" apply (induct k) apply (clarsimp simp: trace_bottom_addr_def dest!: trace_addr_SomeD) apply clarsimp apply (frule(3) exec_trace_step_reachable_induct2) apply clarsimp apply (subgoal_tac "i + k \<in> {i ..< j} \<and> Suc (i + k) \<in> {i .. Suc (i + k)}") apply (rule conjI) apply (elim disjE conjE) apply simp apply (blast intro: sym) apply (rule conjI) apply (elim disjE conjE) apply simp apply (erule rtrancl_into_rtrancl) apply simp apply clarify apply (elim disjE conjE) apply simp apply (erule rtrancl_into_trancl1) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; i + k \<le> j\<rbrakk> \<Longrightarrow> \<forall>nn'. trace_bottom_addr tr (i + k) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + k} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (k \<noteq> 0 \<and> trace_addr tr (i + k) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; i + 0 \<le> j\<rbrakk> \<Longrightarrow> \<forall>nn'. trace_bottom_addr tr (i + 0) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + 0} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (0 \<noteq> 0 \<and> trace_addr tr (i + 0) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)
 2. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; i + k \<le> j\<rbrakk> \<Longrightarrow> \<forall>nn'. trace_bottom_addr tr (i + k) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + k} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (k \<noteq> 0 \<and> trace_addr tr (i + k) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+); tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; i + Suc k \<le> j\<rbrakk> \<Longrightarrow> \<forall>nn'. trace_bottom_addr tr (i + Suc k) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + Suc k} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (Suc k \<noteq> 0 \<and> trace_addr tr (i + Suc k) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; i + k \<le> j\<rbrakk> \<Longrightarrow> \<forall>nn'. trace_bottom_addr tr (i + k) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + k} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (k \<noteq> 0 \<and> trace_addr tr (i + k) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+); tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; i + Suc k \<le> j\<rbrakk> \<Longrightarrow> \<forall>nn'. trace_bottom_addr tr (i + Suc k) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + Suc k} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (Suc k \<noteq> 0 \<and> trace_addr tr (i + Suc k) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+) proof (prove)
goal (1 subgoal):
 1. \<And>k nn'. \<lbrakk>\<forall>nn'. trace_bottom_addr tr (i + k) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + k} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+); tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+) proof (prove)
goal (1 subgoal):
 1. \<And>k nn'. \<lbrakk>\<forall>nn'. trace_bottom_addr tr (i + k) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + k} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+); tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; (\<forall>n. trace_bottom_addr tr (i + k) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph f)) \<and> trace_bottom_addr tr (i + k) \<noteq> None \<and> (trace_bottom_addr tr (i + k) = Some nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (the (trace_bottom_addr tr (i + k)), nn') \<in> reachable_step' f)\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+) proof (prove)
goal (1 subgoal):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+) proof (prove)
goal (2 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (3 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)}
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (4 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; y = nn'; trace_addr tr (Suc (i + k)) = None\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)}
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)}
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)
 4. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (3 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> Some nn' \<in> trace_addr tr ` {i..Suc (i + k)}
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (2 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> ((\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (3 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (4 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; y = nn'; trace_addr tr (Suc (i + k)) = None\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 4. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (3 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (3 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> (y, nn') \<in> reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}}
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (2 subgoals):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)}\<rbrakk> \<Longrightarrow> (\<exists>y. trace_addr tr (Suc (i + k)) = Some y) \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (2 subgoals):
 1. \<And>k nn' y x ya. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some ya\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (3 subgoals):
 1. \<And>k nn' y x ya. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some ya; y = nn'; trace_addr tr (Suc (i + k)) = None\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 2. \<And>k nn' y x ya. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some ya; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 3. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (2 subgoals):
 1. \<And>k nn' y x ya. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some ya; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (2 subgoals):
 1. \<And>k nn' y x ya. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k; i + k \<in> {i..<j}; Suc (i + k) \<in> {i..Suc (i + k)}; trace_addr tr (Suc (i + k)) = Some ya; trace_addr tr (Suc (i + k)) = Some nn'; (y, nn') \<in> reachable_step' f\<rbrakk> \<Longrightarrow> (y, nn') \<in> reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}}
 2. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal (1 subgoal):
 1. \<And>k nn' y x. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; Suc (i + k) \<le> j; trace_bottom_addr tr (Suc (i + k)) = Some nn'; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph f); y = nn' \<and> trace_addr tr (Suc (i + k)) = None \<or> trace_addr tr (Suc (i + k)) = Some nn' \<and> (y, nn') \<in> reachable_step' f; trace_bottom_addr tr (i + k) = trace_addr tr x; Some y = trace_addr tr x; (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>*; 0 < k \<and> (\<exists>y. trace_addr tr (i + k) = Some y) \<longrightarrow> (nn, y) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+; i \<le> x; x \<le> i + k\<rbrakk> \<Longrightarrow> i + k \<in> {i..<j} \<and> Suc (i + k) \<in> {i..Suc (i + k)} proof (prove)
goal:
No subgoals!