theory GraphProof

theorem restr_trace_refine_Restr2:
  "j \<noteq> 0
    \<Longrightarrow> distinct (map fst rs2)
    \<Longrightarrow> wf_graph_function f2 ilen olen \<Longrightarrow> Gamma2 fn2 = Some f2
    \<Longrightarrow> i \<noteq> 0 \<longrightarrow> pc' n (restrs_list ((n, [i - 1]) # (restrs_visit rs2 (NextNode n) f2))) tr'
    \<Longrightarrow> \<not> pc' n (restrs_list ((n, [j - 1]) # (restrs_visit rs2 (NextNode n) f2))) tr'
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list ((n, [i ..< j]) # rs2)) orel tr tr'
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list 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 dest!: exec_trace_init) apply simp apply (clarsimp simp: visit_eqs 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; i \<noteq> 0 \<longrightarrow> pc' n (restrs_list ((n, [i - 1]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - 1]) # restrs_visit rs2 (NextNode n) f2)) tr'; restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list ((n, [i..<j]) # rs2)) orel tr tr'\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf xs ys. \<lbrakk>0 < j; distinct (map fst rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); (\<forall>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<longrightarrow> length xsa \<noteq> length (function_inputs gf)) \<or> (\<forall>ysa. init_state fn2 f2 ys = init_state fn2 f2 ysa \<longrightarrow> length ysa \<noteq> length (function_inputs f2)) \<or> \<not> restrs_eventually_condition tr' (restrs_list ((n, [i..<j]) # rs2))\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, f2) orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf xs ys. \<lbrakk>0 < j; distinct (map fst rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<rbrakk> \<Longrightarrow> restrs_eventually_condition tr' ((\<lambda>y. UNIV)(n := {i..<j}))
 2. \<And>gf xs ys. \<lbrakk>0 < j; distinct (map fst rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); (\<forall>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<longrightarrow> length xsa \<noteq> length (function_inputs gf)) \<or> (\<forall>ysa. init_state fn2 f2 ys = init_state fn2 f2 ysa \<longrightarrow> length ysa \<noteq> length (function_inputs f2))\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, f2) orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf xs ys. \<lbrakk>0 < j; distinct (map fst rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); (\<forall>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<longrightarrow> length xsa \<noteq> length (function_inputs gf)) \<or> (\<forall>ysa. init_state fn2 f2 ys = init_state fn2 f2 ysa \<longrightarrow> length ysa \<noteq> length (function_inputs f2))\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, f2) orel tr tr'
 2. \<And>gf xs ys. \<lbrakk>0 < j; distinct (map fst rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> (\<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = Some y); visit tr' (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> (\<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = Some y); visit tr' (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> (\<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = Some y); visit tr' (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> (\<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = Some y); visit tr' (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> (\<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = Some y); visit tr' (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> (\<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = Some y); visit tr' (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; \<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = Some y; visit tr' (NextNode n) (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; \<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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) m)); tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) n else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) 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 rs2 (NextNode n) f2) m else restrs_list (restrs_visit rs2 (NextNode n) f2) 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> pc' n (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; \<not> pc' n (restrs_list ((n, [j - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2)\<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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; 0 < i \<longrightarrow> (\<exists>y. visit tr' (NextNode n) (restrs_list ((n, [i - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = 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 rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; visit tr' (NextNode n) (restrs_list ((n, [card {i. i < m \<and> trace_addr tr' i = Some (NextNode n)} - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) = None; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; \<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 rs2 (NextNode n) f2)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; \<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 rs2 (NextNode n) f2)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; \<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 rs2 (NextNode n) f2)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; \<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 rs2 (NextNode n) f2)) i; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2 (NextNode n) f2)) 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 rs2); wf_graph_function f2 ilen olen; Gamma2 fn2 = Some f2; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; the (tr' 0) = [init_state fn2 f2 ys]; length ys = length (function_inputs f2); 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 rs2 (NextNode n) f2)) m'; \<not> restrs_condition tr' (restrs_list ((n, [card {i. i < m \<and> trace_addr tr' i = Some (NextNode n)} - Suc 0]) # restrs_visit rs2 (NextNode n) f2)) m'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!