theory GraphProof

theorem restr_trace_refine_Restr1:
  "j \<noteq> 0
    \<Longrightarrow> distinct (map fst rs1)
    \<Longrightarrow> wf_graph_function f1 ilen olen \<Longrightarrow> Gamma1 fn1 = Some f1
    \<Longrightarrow> i \<noteq> 0 \<longrightarrow>
        pc' n (restrs_list ((n, [i - 1]) # (restrs_visit rs1 (NextNode n) f1))) tr
    \<Longrightarrow> \<not> pc' n (restrs_list ((n, [j - 1]) # (restrs_visit rs1 (NextNode n) f1))) tr
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list ((n, [i ..< j]) # rs1)) rs2 orel tr tr'
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list rs1) rs2 orel tr tr'" apply (clarsimp simp: restr_trace_refine_def) apply (subst(asm) restrs_eventually_Cons, simp_all add: K_def) prefer 2 apply auto[1] apply (rule restrs_eventually_upt) apply (clarsimp simp: fold_double_trace_imp double_trace_imp_def pc_def) apply (case_tac "i = 0") apply (rule_tac x=0 in exI) apply (clarsimp simp: dest!: exec_trace_init) apply simp apply (clarsimp simp: visit_eqs) apply (simp(no_asm_use) add: restrs_list_Cons restrs_condition_def) apply (drule_tac x=n in spec)+ apply simp apply (rule_tac x="Suc ia" in exI, simp add: Collect_less_Suc) apply (rule exec_trace_addr_Suc[simplified], assumption) apply simp apply (clarsimp simp: fold_double_trace_imp double_trace_imp_def pc_def) apply (thin_tac "0 < i \<longrightarrow> q" for q) apply (clarsimp simp: visit_eqs) apply (frule num_visits_equals_j_first[OF refl, simplified neq0_conv]) apply clarsimp apply (drule(5) restrs_eventually_at_visit) apply (drule_tac x=m' in spec, clarsimp) apply (clarsimp simp: restrs_list_Cons restrs_condition_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<noteq> 0; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; i \<noteq> 0 \<longrightarrow> pc' n (restrs_list ((n, [i - 1]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - 1]) # restrs_visit rs1 (NextNode n) f1)) tr; restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list ((n, [i..<j]) # rs1)) rs2 orel tr tr'\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list rs1) rs2 orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<forall>xsa. init_state fn1 f1 xs = init_state fn1 f1 xsa \<longrightarrow> length xsa \<noteq> length (function_inputs f1)) \<or> (\<forall>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<longrightarrow> length ysa \<noteq> length (function_inputs gf')) \<or> \<not> restrs_eventually_condition tr (restrs_list ((n, [i..<j]) # rs1))\<rbrakk> \<Longrightarrow> trace_refine2 prec (f1, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> restrs_eventually_condition tr ((\<lambda>y. UNIV)(n := {i..<j}))
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<forall>xsa. init_state fn1 f1 xs = init_state fn1 f1 xsa \<longrightarrow> length xsa \<noteq> length (function_inputs f1)) \<or> (\<forall>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<longrightarrow> length ysa \<noteq> length (function_inputs gf'))\<rbrakk> \<Longrightarrow> trace_refine2 prec (f1, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<forall>xsa. init_state fn1 f1 xs = init_state fn1 f1 xsa \<longrightarrow> length xsa \<noteq> length (function_inputs f1)) \<or> (\<forall>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<longrightarrow> length ysa \<noteq> length (function_inputs gf'))\<rbrakk> \<Longrightarrow> trace_refine2 prec (f1, gf') orel tr tr'
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> restrs_eventually_condition tr ((\<lambda>y. UNIV)(n := {i..<j})) proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> restrs_eventually_condition tr ((\<lambda>y. UNIV)(n := {i..<j})) proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> tr m \<noteq> None
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> (\<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y); visit tr (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (3 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> (\<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y); visit tr (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); i = 0\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> (\<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y); visit tr (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); i \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 3. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (3 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> (\<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y); visit tr (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); i = 0\<rbrakk> \<Longrightarrow> card {i. i < 0 \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr 0 = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> (\<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y); visit tr (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); i \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 3. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> (\<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y); visit tr (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); i \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; \<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y; visit tr (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); 0 < i\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys ia. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); 0 < i; restrs_condition tr (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) ia; trace_addr tr ia = Some (NextNode n); \<forall>j<ia. restrs_condition tr (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys ia. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> (\<exists>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<notin> (if m = n then set [j - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); 0 < i; \<forall>m. card {i. i < ia \<and> trace_addr tr i = Some (NextNode m)} \<in> (if m = n then set [i - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m); trace_addr tr ia = Some (NextNode n); \<forall>j<ia. (\<forall>m. card {i. i < j \<and> trace_addr tr i = Some (NextNode m)} \<in> (if m = n then set [i - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)) \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys ia. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); 0 < i; trace_addr tr ia = Some (NextNode n); trace_addr tr n = Some (NextNode n) \<longrightarrow> (\<exists>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<notin> (if m = n then set [j - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)); card {i. i < ia \<and> trace_addr tr i = Some (NextNode n)} \<in> (if n = n then set [i - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) n else restrs_list (restrs_visit rs1 (NextNode n) f1) n); n < ia \<longrightarrow> (\<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> (if m = n then set [i - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)) \<longrightarrow> trace_addr tr n \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys ia. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); 0 < i; trace_addr tr ia = Some (NextNode n); trace_addr tr n = Some (NextNode n) \<longrightarrow> (\<exists>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<notin> (if m = n then set [j - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)); card {i. i < ia \<and> trace_addr tr i = Some (NextNode n)} = i - Suc 0 \<and> card {i. i < ia \<and> trace_addr tr i = Some (NextNode n)} \<in> restrs_list (restrs_visit rs1 (NextNode n) f1) n; n < ia \<longrightarrow> (\<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> (if m = n then set [i - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)) \<longrightarrow> trace_addr tr n \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} = i \<and> (\<exists>y. tr m = Some y)
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys ia. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); 0 < i; trace_addr tr ia = Some (NextNode n); trace_addr tr n = Some (NextNode n) \<longrightarrow> (\<exists>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<notin> (if m = n then set [j - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)); card {i. i < ia \<and> trace_addr tr i = Some (NextNode n)} = i - Suc 0 \<and> card {i. i < ia \<and> trace_addr tr i = Some (NextNode n)} \<in> restrs_list (restrs_visit rs1 (NextNode n) f1) n; n < ia \<longrightarrow> (\<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> (if m = n then set [i - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)) \<longrightarrow> trace_addr tr n \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> \<exists>y. tr (Suc ia) = Some y
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (2 subgoals):
 1. \<And>gf' xs ys ia. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); 0 < i; trace_addr tr ia = Some (NextNode n); trace_addr tr n = Some (NextNode n) \<longrightarrow> (\<exists>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<notin> (if m = n then set [j - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)); card {i. i < ia \<and> trace_addr tr i = Some (NextNode n)} = i - Suc 0 \<and> card {i. i < ia \<and> trace_addr tr i = Some (NextNode n)} \<in> restrs_list (restrs_visit rs1 (NextNode n) f1) n; n < ia \<longrightarrow> (\<forall>m. card {i. i < n \<and> trace_addr tr i = Some (NextNode m)} \<in> (if m = n then set [i - Suc 0] \<inter> restrs_list (restrs_visit rs1 (NextNode n) f1) m else restrs_list (restrs_visit rs1 (NextNode n) f1) m)) \<longrightarrow> trace_addr tr n \<noteq> Some (NextNode n)\<rbrakk> \<Longrightarrow> trace_addr tr ia = Some (NextNode (?m144 gf' xs ys ia))
 2. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys. \<lbrakk>0 < j; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) tr; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> \<forall>m. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<noteq> j proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys m. \<lbrakk>0 < card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; 0 < i \<longrightarrow> (\<exists>y. visit tr (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = Some y); visit tr (NextNode n) (restrs_list ((n, [card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); j = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys m. \<lbrakk>0 < card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; visit tr (NextNode n) (restrs_list ((n, [card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); j = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys m. \<lbrakk>0 < card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (restrs_list ((n, [card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); j = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys m. \<lbrakk>0 < card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (restrs_list ((n, [card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); j = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; \<exists>m'. trace_addr tr m' = Some (NextNode n) \<and> card {i. i < m' \<and> trace_addr tr i = Some (NextNode n)} = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys m m'. \<lbrakk>0 < card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (restrs_list ((n, [card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); j = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; trace_addr tr m' = Some (NextNode n); card {i. i < m' \<and> trace_addr tr i = Some (NextNode n)} = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys m m'. \<lbrakk>0 < card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; \<forall>i. trace_addr tr i = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr (restrs_list ((n, [card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); j = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; trace_addr tr m' = Some (NextNode n); card {i. i < m' \<and> trace_addr tr i = Some (NextNode n)} = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0; restrs_condition tr (restrs_list (restrs_visit rs1 (NextNode n) f1)) m'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>gf' xs ys m m'. \<lbrakk>0 < card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; distinct (map fst rs1); wf_graph_function f1 ilen olen; Gamma1 fn1 = Some f1; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 f1 xs]; length xs = length (function_inputs f1); restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); j = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)}; trace_addr tr m' = Some (NextNode n); card {i. i < m' \<and> trace_addr tr i = Some (NextNode n)} = card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0; restrs_condition tr (restrs_list (restrs_visit rs1 (NextNode n) f1)) m'; \<not> restrs_condition tr (restrs_list ((n, [card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} - Suc 0]) # restrs_visit rs1 (NextNode n) f1)) m'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!