theory Peterson_Atomicity

theorem peterson_proc_system_refinement:
  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
    (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited))
    (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited))
    (\<lambda>s0 s. s0 = s) (\<lambda>t0 t. t0 = t)
    abs_peterson_proc_system peterson_proc_system" apply (unfold abs_peterson_proc_system_def peterson_proc_system_def) apply (rule prefix_refinement_parallel') apply (rule prefix_refinement_weaken_rely, rule prefix_refinement_weaken_pre) apply (rule peterson_repeat_refinement) apply simp apply simp apply (rule eq_refl, rule bipred_disj_op_eq, simp) apply (rule eq_refl, rule bipred_disj_op_eq, simp) apply (rule prefix_refinement_weaken_rely, rule prefix_refinement_weaken_pre) apply (rule peterson_repeat_refinement) apply simp apply simp apply (rule eq_refl, rule bipred_disj_op_eq, simp) apply (rule eq_refl, rule bipred_disj_op_eq, simp) apply (clarsimp intro!: par_tr_fin_bind par_tr_fin_interference) apply (clarsimp intro!: par_tr_fin_bind par_tr_fin_interference) apply (rule rg_weaken_pre, rule rg_weaken_rely) apply (rule validI_repeat_interference; simp) apply (rule peterson_proc_mutual_excl) apply (simp+)[3] apply (rule rg_weaken_pre, rule rg_weaken_rely) apply (rule validI_repeat_interference; simp) apply (rule peterson_proc_mutual_excl) apply (simp+)[3] apply (rule rg_weaken_pre, rule rg_weaken_rely) apply (rule validI_repeat_interference; simp) apply (rule abs_peterson_proc_mutual_excl) apply (simp+)[3] apply (rule rg_weaken_pre, rule rg_weaken_rely) apply (rule validI_repeat_interference; simp) apply (rule abs_peterson_proc_mutual_excl) apply (simp+)[3] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) (=) (=) abs_peterson_proc_system peterson_proc_system proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) (=) (=) (Trace_Monad.parallel (do repeat (abs_peterson_proc A);
interference
od) (do repeat (abs_peterson_proc B);
interference
od)) (Trace_Monad.parallel (do repeat (peterson_proc A);
interference
od) (do repeat (peterson_proc B);
interference
od)) proof (prove)
goal (8 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Gc) ((=) or ?Gd) (do repeat (abs_peterson_proc A);
interference
od) (do repeat (peterson_proc A);
interference
od)
 2. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Ga) ((=) or ?Gb) (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 3. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 4. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 5. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gd\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>?Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gc\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 8. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>?Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (12 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) ?P'13 ?Q'13 ?AR9 ?R9 (do repeat (abs_peterson_proc A);
interference
od) (do repeat (peterson_proc A);
interference
od)
 2. \<forall>s s0. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> ?P'13 s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> ?Q'13 t0 t
 4. ((=) or ?Gd) \<le> ?R9
 5. ((=) or ?Gc) \<le> ?AR9
 6. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Ga) ((=) or ?Gb) (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 7. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 8. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 9. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gd\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 10. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>?Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<forall>s s0. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> peterson_rel A s0 s \<and> invs s \<and> ab_label s A = Exited
 2. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> peterson_rel A t0 t \<and> invs t \<and> ab_label t A = Exited
 3. ((=) or ?Gd) \<le> peterson_rel (other_ident A)
 4. ((=) or ?Gc) \<le> peterson_rel (other_ident A)
 5. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Ga) ((=) or ?Gb) (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 6. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 7. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 8. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gd\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 9. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>?Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 10. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gc\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> peterson_rel A t0 t \<and> invs t \<and> ab_label t A = Exited
 2. ((=) or ?Gd) \<le> peterson_rel (other_ident A)
 3. ((=) or ?Gc) \<le> peterson_rel (other_ident A)
 4. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Ga) ((=) or ?Gb) (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 5. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 6. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 7. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gd\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 8. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>?Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 9. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gc\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 10. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>?Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (9 subgoals):
 1. ((=) or ?Gd) \<le> peterson_rel (other_ident A)
 2. ((=) or ?Gc) \<le> peterson_rel (other_ident A)
 3. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Ga) ((=) or ?Gb) (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 4. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 5. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 6. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gd\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>?Gd\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 8. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gc\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 9. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>?Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (8 subgoals):
 1. ((=) or ?Gc) \<le> peterson_rel (other_ident A)
 2. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Ga) ((=) or ?Gb) (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 3. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 4. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 5. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gc\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 8. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>?Gc\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (7 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) ((=) or ?Ga) ((=) or ?Gb) (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 2. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 3. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 4. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (11 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) ?P'30 ?Q'30 ?AR26 ?R26 (do repeat (abs_peterson_proc B);
interference
od) (do repeat (peterson_proc B);
interference
od)
 2. \<forall>s s0. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> ?P'30 s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> ?Q'30 t0 t
 4. ((=) or ?Gb) \<le> ?R26
 5. ((=) or ?Ga) \<le> ?AR26
 6. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 7. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 8. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 9. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 10. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<forall>s s0. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> peterson_rel B s0 s \<and> invs s \<and> ab_label s B = Exited
 2. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> peterson_rel B t0 t \<and> invs t \<and> ab_label t B = Exited
 3. ((=) or ?Gb) \<le> peterson_rel (other_ident B)
 4. ((=) or ?Ga) \<le> peterson_rel (other_ident B)
 5. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 6. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 7. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 8. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 9. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 10. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<longrightarrow> t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> peterson_rel B t0 t \<and> invs t \<and> ab_label t B = Exited
 2. ((=) or ?Gb) \<le> peterson_rel (other_ident B)
 3. ((=) or ?Ga) \<le> peterson_rel (other_ident B)
 4. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 5. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 6. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 8. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 9. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (8 subgoals):
 1. ((=) or ?Gb) \<le> peterson_rel (other_ident B)
 2. ((=) or ?Ga) \<le> peterson_rel (other_ident B)
 3. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 4. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 5. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>?Gb\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Gb\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 8. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (7 subgoals):
 1. ((=) or ?Ga) \<le> peterson_rel (other_ident B)
 2. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 3. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 4. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>?Ga\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or ?Ga\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. par_tr_fin_principle (do repeat (abs_peterson_proc A);
interference
od)
 2. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 3. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 4. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. par_tr_fin_principle (do repeat (abs_peterson_proc B);
interference
od)
 2. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 3. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 4. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 3. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 4. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrace>?P'53\<rbrace>, \<lbrace>?R'56\<rbrace> do repeat (peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<And>s0 s. ((=) or peterson_rel (other_ident A)) s0 s \<Longrightarrow> ?R'56 s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'53 s0 s
 4. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrace>?P'53\<rbrace>, \<lbrace>?R'56\<rbrace> peterson_proc A \<lbrace>peterson_rel A\<rbrace>, \<lbrace>\<lambda>_. ?P'53\<rbrace>
 2. \<forall>s0 s. ?P'53 s0 s \<longrightarrow> peterson_rel A s0 s
 3. \<And>s0 s. ((=) or peterson_rel (other_ident A)) s0 s \<Longrightarrow> ?R'56 s0 s
 4. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'53 s0 s
 5. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 7. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<forall>s0 s. peterson_rel A s0 s \<and> invs s \<and> ab_label s A = Exited \<longrightarrow> peterson_rel A s0 s
 2. \<And>s0 s. ((=) or peterson_rel (other_ident A)) s0 s \<Longrightarrow> peterson_rel (other_ident A) s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> peterson_rel A s0 s \<and> invs s \<and> ab_label s A = Exited
 4. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 3. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'71\<rbrace>, \<lbrace>?R'74\<rbrace> do repeat (peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<And>s0 s. ((=) or peterson_rel (other_ident B)) s0 s \<Longrightarrow> ?R'74 s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'71 s0 s
 4. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrace>?P'71\<rbrace>, \<lbrace>?R'74\<rbrace> peterson_proc B \<lbrace>peterson_rel B\<rbrace>, \<lbrace>\<lambda>_. ?P'71\<rbrace>
 2. \<forall>s0 s. ?P'71 s0 s \<longrightarrow> peterson_rel B s0 s
 3. \<And>s0 s. ((=) or peterson_rel (other_ident B)) s0 s \<Longrightarrow> ?R'74 s0 s
 4. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'71 s0 s
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 6. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<forall>s0 s. peterson_rel B s0 s \<and> invs s \<and> ab_label s B = Exited \<longrightarrow> peterson_rel B s0 s
 2. \<And>s0 s. ((=) or peterson_rel (other_ident B)) s0 s \<Longrightarrow> peterson_rel (other_ident B) s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> peterson_rel B s0 s \<and> invs s \<and> ab_label s B = Exited
 4. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident A)\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'89\<rbrace>, \<lbrace>?R'92\<rbrace> do repeat (abs_peterson_proc A);
interference
od \<lbrace>peterson_rel (other_ident B)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<And>s0 s. ((=) or peterson_rel (other_ident A)) s0 s \<Longrightarrow> ?R'92 s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'89 s0 s
 4. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'89\<rbrace>, \<lbrace>?R'92\<rbrace> abs_peterson_proc A \<lbrace>peterson_rel A\<rbrace>, \<lbrace>\<lambda>_. ?P'89\<rbrace>
 2. \<forall>s0 s. ?P'89 s0 s \<longrightarrow> peterson_rel A s0 s
 3. \<And>s0 s. ((=) or peterson_rel (other_ident A)) s0 s \<Longrightarrow> ?R'92 s0 s
 4. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'89 s0 s
 5. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<forall>s0 s. peterson_rel A s0 s \<and> invs s \<and> ab_label s A = Exited \<longrightarrow> peterson_rel A s0 s
 2. \<And>s0 s. ((=) or peterson_rel (other_ident A)) s0 s \<Longrightarrow> peterson_rel (other_ident A) s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> peterson_rel A s0 s \<and> invs s \<and> ab_label s A = Exited
 4. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=) or peterson_rel (other_ident B)\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'107\<rbrace>, \<lbrace>?R'110\<rbrace> do repeat (abs_peterson_proc B);
interference
od \<lbrace>peterson_rel (other_ident A)\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<And>s0 s. ((=) or peterson_rel (other_ident B)) s0 s \<Longrightarrow> ?R'110 s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'107 s0 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'107\<rbrace>, \<lbrace>?R'110\<rbrace> abs_peterson_proc B \<lbrace>peterson_rel B\<rbrace>, \<lbrace>\<lambda>_. ?P'107\<rbrace>
 2. \<forall>s0 s. ?P'107 s0 s \<longrightarrow> peterson_rel B s0 s
 3. \<And>s0 s. ((=) or peterson_rel (other_ident B)) s0 s \<Longrightarrow> ?R'110 s0 s
 4. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> ?P'107 s0 s proof (prove)
goal (3 subgoals):
 1. \<forall>s0 s. peterson_rel B s0 s \<and> invs s \<and> ab_label s B = Exited \<longrightarrow> peterson_rel B s0 s
 2. \<And>s0 s. ((=) or peterson_rel (other_ident B)) s0 s \<Longrightarrow> peterson_rel (other_ident B) s0 s
 3. \<And>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<Longrightarrow> peterson_rel B s0 s \<and> invs s \<and> ab_label s B = Exited proof (prove)
goal:
No subgoals!