theory GraphProof

lemma restr_trace_refine_Split_orig:
  fixes rs1 rs2 hyps Gamma1 f1 Gamma2 f2
  defines "H trs \<equiv>
          exec_double_trace Gamma1 f1 Gamma2 f2 (fst trs) (snd trs)
        \<and> restrs_eventually_condition (fst trs) (restrs_list rs1)
        \<and> restrs_eventually_condition (snd trs) (restrs_list rs2)"
  assumes Suc: "\<forall>i. double_pc (ccall (Suc i)) (tr, tr') \<longrightarrow> double_pc (ccall i) (tr, tr')"
  and init: "\<forall>i. i < k \<longrightarrow> H (tr, tr')
        \<longrightarrow> double_pc (ccall i) (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall i (tr, tr')"
  and induct: "\<forall>i. H (tr, tr')
        \<longrightarrow> double_pc (ccall (i + k)) (tr, tr')
        \<longrightarrow> (\<forall>j < k. split_visit_rel rel ccall acall (i + j) (tr, tr'))
        \<longrightarrow> split_visit_rel rel ccall acall (i + k) (tr, tr')"
  and distinct: "\<forall>tr i j k. restrs_condition tr (snd (snd (ccall i))) k
        \<longrightarrow> restrs_condition tr (snd (snd (ccall j))) k \<longrightarrow> i = j"
      "\<forall>tr i j k. restrs_condition tr (snd (snd (acall i))) k
        \<longrightarrow> restrs_condition tr (snd (snd (acall j))) k \<longrightarrow> i = j"
  and sides: "\<forall>i. \<not> fst (ccall i) \<and> fst (acall i)"
  and k: "k \<noteq> 0"
  and init_case: "\<not> double_pc (ccall k) (tr, tr')
    \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2)
        orel tr tr'"
  and induct_case: "\<And>i. induct_var (fst (snd (ccall 0))) i
    \<Longrightarrow> induct_var (fst (snd (acall 0))) i
    \<Longrightarrow> \<not> double_pc (ccall (i + k)) (tr, tr')
    \<Longrightarrow> \<forall>j < k. split_visit_rel rel ccall acall (i + j) (tr, tr')
    \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2)
            orel tr tr'"
  shows "restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr'" proof - have pc_ccall_less: "double_pc (ccall n) (tr, tr')
    \<longrightarrow> m \<le> n \<longrightarrow> double_pc (ccall m) (tr, tr')" for n m apply (induct_tac n, simp_all) apply clarsimp apply (frule Suc[rule_format]) apply (clarsimp simp: linorder_not_le Suc_le_eq[symmetric]) done { fix i assume le[simp]: "i \<ge> k" note induct[rule_format, where i="i - k", simplified] } note induct_minus = this { fix j have "double_pc (ccall j) (tr, tr') \<and> H (tr, tr')
      \<longrightarrow> split_visit_rel rel ccall acall j (tr, tr')" apply (induct j rule: nat_less_induct) apply (case_tac "n < k") apply (simp add: init) apply clarsimp apply (rule induct_minus, simp+) apply (simp add: field_simps pc_ccall_less) done } note rel_induct = this note H_intro = H_def[THEN meta_eq_to_obj_eq, THEN iffD2, OF conjI] have Suc_Max: "finite S \<Longrightarrow> Suc (Max S) \<notin> S" for S by (auto dest: Max_ge) have unreached:
    "finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}
        \<Longrightarrow> x \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}
        \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr')"
    for x apply (frule Suc_Max) apply (frule Max_in, rule notI, clarsimp) apply clarsimp apply (case_tac k, simp_all) apply (auto dest!: less_Suc_eq[THEN iffD1]) done have infinite_helper:
    "tr \<in> exec_trace G f
        \<Longrightarrow> \<forall>i j k. restrs_condition tr (snd (vis i)) k
            \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j
        \<Longrightarrow> \<not> finite {n. pc (fst (vis n)) (snd (vis n)) tr}
        \<Longrightarrow> trace_end tr = None"
    for tr G f and vis :: "'b \<Rightarrow> next_node \<times> (nat \<Rightarrow> nat set)" apply (clarsimp simp: trace_end_def) apply (drule(1) exec_trace_None_dom_subset) apply (drule_tac R="\<lambda>n i. restrs_condition tr (snd (vis n)) i"
           in pigeonhole_infinite_rel) apply (erule finite_subset, simp) apply (auto simp: pc_def visit_eqs dest!: trace_addr_SomeD)[1] apply (auto dest!: not_finite_two) done have infinite:
    "exec_double_trace Gamma1 f1 Gamma2 f2 tr tr'
        \<Longrightarrow> H (tr, tr')
        \<Longrightarrow> \<not> finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}
        \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None" apply (case_tac "\<exists>n. \<not> double_pc (ccall n) (tr, tr')") apply clarsimp apply (erule notE, rule_tac k1=n in finite_subset[OF _ finite_lessThan]) apply clarsimp apply (drule_tac x=0 in spec, simp add: k[simplified]) apply (rule ccontr, simp add: pc_ccall_less) apply clarsimp apply (rule conjI) apply (erule_tac vis="\<lambda>i. snd (ccall i)" in infinite_helper) apply (simp add: distinct) apply (simp add: double_pc_def[folded pc_def] split_def sides) apply (erule_tac vis="\<lambda>i. snd (acall i)" in infinite_helper) apply (simp add: distinct) apply clarsimp apply (drule_tac A="UNIV" in finite_subset[rotated]) apply clarsimp apply (rename_tac n, drule_tac x="n" in spec) apply (drule(1) rel_induct[rule_format, OF conjI]) apply (clarsimp simp: split_visit_rel_def) apply (simp add: double_pc_def[folded pc_def] sides split_def) apply simp done show ?thesis apply (clarsimp simp: restr_trace_refine_def) apply (case_tac "\<not> double_pc (ccall k) (tr, tr')") apply (rule init_case[unfolded restr_trace_refine_def, rule_format],
            auto)[1] apply (case_tac "finite {n. \<forall>j < k. double_pc (ccall (n + j)) (tr, tr')}") apply (frule Max_in) apply simp apply (rule_tac x="0" in exI) apply (simp add: pc_ccall_less) apply (rule_tac i="Max {n. \<forall>j < k. double_pc (ccall (n + j)) (tr, tr')}"
         in induct_case[unfolded restr_trace_refine_def, rule_format]) apply (simp add: induct_var_def)+ apply (simp add: rel_induct unreached) apply (simp add: rel_induct unreached H_intro) apply auto[1] apply clarsimp apply (drule infinite[rotated -1], simp) apply (simp add: H_def) apply (simp add: trace_refine2_def trace_refine_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. double_pc (ccall n) (tr, tr') \<longrightarrow> m \<le> n \<longrightarrow> double_pc (ccall m) (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>n. double_pc (ccall n) (tr, tr') \<longrightarrow> m \<le> n \<longrightarrow> double_pc (ccall m) (tr, tr') \<Longrightarrow> double_pc (ccall (Suc n)) (tr, tr') \<longrightarrow> m \<le> Suc n \<longrightarrow> double_pc (ccall m) (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>double_pc (ccall n) (tr, tr') \<longrightarrow> m \<le> n \<longrightarrow> double_pc (ccall m) (tr, tr'); double_pc (ccall (Suc n)) (tr, tr'); m \<le> Suc n\<rbrakk> \<Longrightarrow> double_pc (ccall m) (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>double_pc (ccall n) (tr, tr') \<longrightarrow> m \<le> n \<longrightarrow> double_pc (ccall m) (tr, tr'); double_pc (ccall (Suc n)) (tr, tr'); m \<le> Suc n; double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> double_pc (ccall m) (tr, tr') proof (prove)
goal:
No subgoals! proof (state)
this:
double_pc (ccall ?n) (tr, tr') \<longrightarrow> ?m \<le> ?n \<longrightarrow> double_pc (ccall ?m) (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
double_pc (ccall ?n) (tr, tr') \<longrightarrow> ?m \<le> ?n \<longrightarrow> double_pc (ccall ?m) (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
k \<le> i

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
\<lbrakk>H (tr, tr'); double_pc (ccall i) (tr, tr'); \<And>j. j < k \<Longrightarrow> split_visit_rel rel ccall acall (i + j - k) (tr, tr')\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall i (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
\<lbrakk>k \<le> ?i2; H (tr, tr'); double_pc (ccall ?i2) (tr, tr'); \<And>j. j < k \<Longrightarrow> split_visit_rel rel ccall acall (?i2 + j - k) (tr, tr')\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall ?i2 (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
\<lbrakk>k \<le> ?i2; H (tr, tr'); double_pc (ccall ?i2) (tr, tr'); \<And>j. j < k \<Longrightarrow> split_visit_rel rel ccall acall (?i2 + j - k) (tr, tr')\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall ?i2 (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
\<lbrakk>k \<le> ?i2; H (tr, tr'); double_pc (ccall ?i2) (tr, tr'); \<And>j. j < k \<Longrightarrow> split_visit_rel rel ccall acall (?i2 + j - k) (tr, tr')\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall ?i2 (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. double_pc (ccall j) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall j (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>m<n. double_pc (ccall m) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall m (tr, tr') \<Longrightarrow> double_pc (ccall n) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall n (tr, tr') proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>m<n. double_pc (ccall m) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall m (tr, tr'); n < k\<rbrakk> \<Longrightarrow> double_pc (ccall n) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall n (tr, tr')
 2. \<And>n. \<lbrakk>\<forall>m<n. double_pc (ccall m) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall m (tr, tr'); \<not> n < k\<rbrakk> \<Longrightarrow> double_pc (ccall n) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall n (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. double_pc (ccall m) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall m (tr, tr'); \<not> n < k\<rbrakk> \<Longrightarrow> double_pc (ccall n) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall n (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. double_pc (ccall m) (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall m (tr, tr'); \<not> n < k; double_pc (ccall n) (tr, tr'); H (tr, tr')\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall n (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>n j. \<lbrakk>\<forall>m<n. double_pc (ccall m) (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall m (tr, tr'); \<not> n < k; double_pc (ccall n) (tr, tr'); H (tr, tr'); j < k\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall (n + j - k) (tr, tr') proof (prove)
goal:
No subgoals! proof (state)
this:
double_pc (ccall j) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall j (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
double_pc (ccall ?j2) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall ?j2 (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
double_pc (ccall ?j2) (tr, tr') \<and> H (tr, tr') \<longrightarrow> split_visit_rel rel ccall acall ?j2 (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (state)
this:
\<lbrakk>fst ?trs2 \<in> exec_trace Gamma1 f1 \<and> snd ?trs2 \<in> exec_trace Gamma2 f2; restrs_eventually_condition (fst ?trs2) (restrs_list rs1) \<and> restrs_eventually_condition (snd ?trs2) (restrs_list rs2)\<rbrakk> \<Longrightarrow> H ?trs2

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> Suc (Max S) \<notin> S proof (state)
this:
finite ?S \<Longrightarrow> Suc (Max ?S) \<notin> ?S

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; x \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; x \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Suc (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}) \<notin> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; x \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Suc (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}) \<notin> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr') proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<forall>j<k. double_pc (ccall (x + j)) (tr, tr'); \<forall>j<k. double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + j)) (tr, tr'); j < k; \<not> double_pc (ccall (Suc (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + j))) (tr, tr'); double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>j nat. \<lbrakk>finite {n. \<forall>j<Suc nat. double_pc (ccall (n + j)) (tr, tr')}; \<forall>j<Suc nat. double_pc (ccall (x + j)) (tr, tr'); \<forall>j<Suc nat. double_pc (ccall (Max {n. \<forall>j<Suc nat. double_pc (ccall (n + j)) (tr, tr')} + j)) (tr, tr'); j < Suc nat; \<not> double_pc (ccall (Suc (Max {n. \<forall>j<Suc nat. double_pc (ccall (n + j)) (tr, tr')} + j))) (tr, tr'); double_pc (ccall (Suc (Max {n. \<forall>j<Suc nat. double_pc (ccall (n + j)) (tr, tr')} + nat))) (tr, tr'); k = Suc nat\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; ?x \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr')

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; infinite {n. pc (fst (vis n)) (snd (vis n)) tr}\<rbrakk> \<Longrightarrow> trace_end tr = None proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; infinite {n. pc (fst (vis n)) (snd (vis n)) tr}; tr n = None\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; infinite {n. pc (fst (vis n)) (snd (vis n)) tr}; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> finite (?B9 n)
 2. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> \<forall>a\<in>{n. pc (fst (vis n)) (snd (vis n)) tr}. \<exists>b\<in>?B9 n. restrs_condition tr (snd (vis a)) b
 3. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; dom tr \<subseteq> {..<n}; \<exists>b\<in>?B9 n. infinite {a \<in> {n. pc (fst (vis n)) (snd (vis n)) tr}. restrs_condition tr (snd (vis a)) b}\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> \<forall>a\<in>{n. pc (fst (vis n)) (snd (vis n)) tr}. \<exists>b\<in>dom tr. restrs_condition tr (snd (vis a)) b
 2. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; dom tr \<subseteq> {..<n}; \<exists>b\<in>dom tr. infinite {a \<in> {n. pc (fst (vis n)) (snd (vis n)) tr}. restrs_condition tr (snd (vis a)) b}\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace G f; \<forall>i j k. restrs_condition tr (snd (vis i)) k \<longrightarrow> restrs_condition tr (snd (vis j)) k \<longrightarrow> i = j; dom tr \<subseteq> {..<n}; \<exists>b\<in>dom tr. infinite {a \<in> {n. pc (fst (vis n)) (snd (vis n)) tr}. restrs_condition tr (snd (vis a)) b}\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?tr \<in> exec_trace ?G ?f; \<forall>i j k. restrs_condition ?tr (snd (?vis i)) k \<longrightarrow> restrs_condition ?tr (snd (?vis j)) k \<longrightarrow> i = j; infinite {n. pc (fst (?vis n)) (snd (?vis n)) ?tr}\<rbrakk> \<Longrightarrow> trace_end ?tr = None

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<exists>n. \<not> double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None
 2. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<nexists>n. \<not> double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<not> double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None
 2. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<nexists>n. \<not> double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>H (tr, tr'); \<not> double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<subseteq> {..<n}
 2. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<nexists>n. \<not> double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>H (tr, tr'); \<not> double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; \<forall>j<k. double_pc (ccall (x + j)) (tr, tr')\<rbrakk> \<Longrightarrow> x < n
 2. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<nexists>n. \<not> double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>H (tr, tr'); \<not> double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; double_pc (ccall x) (tr, tr')\<rbrakk> \<Longrightarrow> x < n
 2. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<nexists>n. \<not> double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<nexists>n. \<not> double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> trace_end tr = None
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> trace_end tr' = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> \<forall>i j k. restrs_condition tr (snd (snd (ccall i))) k \<longrightarrow> restrs_condition tr (snd (snd (ccall j))) k \<longrightarrow> i = j
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> infinite {n. pc (fst (snd (ccall n))) (snd (snd (ccall n))) tr}
 3. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> infinite {n. pc (fst (snd (ccall n))) (snd (snd (ccall n))) tr}
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> trace_end tr' = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> trace_end tr' = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1\<rbrakk> \<Longrightarrow> \<forall>i j k. restrs_condition tr' (snd (snd (acall i))) k \<longrightarrow> restrs_condition tr' (snd (snd (acall j))) k \<longrightarrow> i = j
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1\<rbrakk> \<Longrightarrow> infinite {n. pc (fst (snd (acall n))) (snd (snd (acall n))) tr'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1\<rbrakk> \<Longrightarrow> infinite {n. pc (fst (snd (acall n))) (snd (snd (acall n))) tr'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; finite {n. pc (fst (snd (acall n))) (snd (snd (acall n))) tr'}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1\<rbrakk> \<Longrightarrow> UNIV \<subseteq> {n. pc (fst (snd (acall n))) (snd (snd (acall n))) tr'}
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; finite UNIV\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1\<rbrakk> \<Longrightarrow> pc (fst (snd (acall x))) (snd (snd (acall x))) tr'
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; finite UNIV\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>H (tr, tr'); tr \<in> exec_trace Gamma1 f1; double_pc (ccall n) (tr, tr')\<rbrakk> \<Longrightarrow> pc (fst (snd (acall n))) (snd (snd (acall n))) tr'
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; finite UNIV\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>H (tr, tr'); tr \<in> exec_trace Gamma1 f1; split_visit_rel rel ccall acall n (tr, tr')\<rbrakk> \<Longrightarrow> pc (fst (snd (acall n))) (snd (snd (acall n))) tr'
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; finite UNIV\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>H (tr, tr'); tr \<in> exec_trace Gamma1 f1; double_pc (ccall n) (tr, tr'); double_pc (acall n) (tr, tr'); rel n (\<lambda>(x, y). the (double_visit (tuple_switch (ccall, acall) x (tuple_switch (0, n) y)) (tr, tr')))\<rbrakk> \<Longrightarrow> pc (fst (snd (acall n))) (snd (snd (acall n))) tr'
 2. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; finite UNIV\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H (tr, tr'); \<forall>n. double_pc (ccall n) (tr, tr'); tr \<in> exec_trace Gamma1 f1; finite UNIV\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2; H (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> trace_end tr' = None

goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> double_pc (ccall k) (tr, tr')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (3 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<noteq> {}
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 3. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (3 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> \<exists>x. \<forall>j<k. double_pc (ccall (x + j)) (tr, tr')
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 3. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (3 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> \<forall>j<k. double_pc (ccall (0 + j)) (tr, tr')
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 3. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (6 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> induct_var (fst (snd (ccall 0))) (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')})
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> induct_var (fst (snd (acall 0))) (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')})
 3. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr')
 4. \<And>gf gf' xs ys j. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; j < k\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + j) (tr, tr')
 5. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> (tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2) \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf)) \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf')) \<and> restrs_eventually_condition tr (restrs_list rs1) \<and> restrs_eventually_condition tr' (restrs_list rs2)
 6. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (4 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; \<forall>j<k. double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + j)) (tr, tr')\<rbrakk> \<Longrightarrow> \<not> double_pc (ccall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + k)) (tr, tr')
 2. \<And>gf gf' xs ys j. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; j < k\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + j) (tr, tr')
 3. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> (tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2) \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf)) \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf')) \<and> restrs_eventually_condition tr (restrs_list rs1) \<and> restrs_eventually_condition tr' (restrs_list rs2)
 4. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (3 subgoals):
 1. \<And>gf gf' xs ys j. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; j < k\<rbrakk> \<Longrightarrow> split_visit_rel rel ccall acall (Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} + j) (tr, tr')
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> (tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2) \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf)) \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf')) \<and> restrs_eventually_condition tr (restrs_list rs1) \<and> restrs_eventually_condition tr' (restrs_list rs2)
 3. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); finite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}; Max {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')} \<in> {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> (tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2) \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf)) \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf')) \<and> restrs_eventually_condition tr (restrs_list rs1) \<and> restrs_eventually_condition tr' (restrs_list rs2)
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc (ccall k) (tr, tr'); infinite {n. \<forall>j<k. double_pc (ccall (n + j)) (tr, tr')}\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc (ccall k) (tr, tr')\<rbrakk> \<Longrightarrow> H (tr, tr')
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc (ccall k) (tr, tr'); trace_end tr = None \<and> trace_end tr' = None\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2; Gamma1 f1 = Some gf; Gamma2 f2 = Some gf'; the (tr 0) = [init_state f1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr (restrs_list rs1); restrs_eventually_condition tr' (restrs_list rs2); the (tr' 0) = [init_state f2 gf' ys]; length ys = length (function_inputs gf'); double_pc (ccall k) (tr, tr'); trace_end tr = None \<and> trace_end tr' = None\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal:
No subgoals! proof (state)
this:
restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr'

goal:
No subgoals!