theory Peterson_Atomicity

lemma critical_section_refinement:
  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
    (\<lambda>_ s. invs s \<and> ab_label s ident = Critical) \<top>\<top>
    (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
    abs_critical_section critical_section" apply (simp add: abs_critical_section_def critical_section_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_interferences_split) apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_interference_peterson) 

      (* reorder the interference and modify*)
       apply (rule pfx_refinement_use_rel_tr_refinement_equivp
                  [where Q="\<lambda>s. invs s \<and> ab_label s (ident) = Critical"]) apply (rule rel_tr_refinement_bind_left_general_2left_2right) apply simp apply (rule disjI1,
                     clarsimp simp: not_env_steps_first_all
                                    cs_not_env_steps_first release_lock_def) apply (rule rshuttle_modify_interference) apply (simp add: peterson_sr_def peterson_rel_def) apply (clarsimp simp: peterson_rel_def) apply (clarsimp simp: p_state.splits) apply (clarsimp simp: peterson_rel_def invs_def invs_defs) apply simp apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_interference_peterson) apply (rule prefix_refinement_bind[where intsr=peterson_sr_cs1]) apply (rule pfx_refn_modifyT) apply (clarsimp simp add: peterson_sr_def peterson_sr_cs1_def) apply (rule prefix_refinement_bind_sr) apply (rule cs_refine) apply (rule prefix_refinement_interference_peterson) apply (wpsimp wp: validI_triv[OF cs_closed])+ apply (subst peterson_rel_imp_label[symmetric], assumption, simp) apply (drule peterson_rel_imp_invs, simp) apply (simp add: peterson_sr_ab_label) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ s. invs s \<and> ab_label s ident = Critical) (\<lambda>_ _. True) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) abs_critical_section critical_section proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ s. invs s \<and> ab_label s ident = Critical) (\<lambda>_ _. True) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interferences;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od) proof (prove)
goal (3 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) ?P'1 ?Q'1 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interferences;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od)
 2. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ?P'1 s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ?Q'1 t0 t proof (prove)
goal (3 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) ?P'1 ?Q'1 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do x <- interference;
y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od)
 2. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ?P'1 s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ?Q'1 t0 t proof (prove)
goal (6 subgoals):
 1. pfx_refn peterson_sr ?rvr7 ?P7 ?Q7 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) interference interference
 2. \<And>x y. ?rvr7 x y \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q''7 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od)
 3. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''7\<rbrace>
 5. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> (?P7 and ?P'7) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> (?Q7 and ?Q'7) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q''7 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od)
 2. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''7\<rbrace>
 4. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q''7 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od)
 2. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''7\<rbrace>
 4. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>x y. True \<Longrightarrow> rel_tr_refinement peterson_sr (\<lambda>s. invs s \<and> ab_label s ident = Critical) (peterson_rel (other_ident ident)) False (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od) (?g'13 x y)
 2. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 3. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (?g'13 x y)
 4. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 6. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (9 subgoals):
 1. \<And>x y. True \<Longrightarrow> reflp peterson_sr
 2. \<And>x y. True \<Longrightarrow> (\<forall>y. not_env_steps_first (do y <- cs2;
interference
od)) \<or> (\<forall>s s' t. peterson_sr s s' \<longrightarrow> peterson_rel (other_ident ident) s t = peterson_rel (other_ident ident) s' t)
 3. \<And>x y. True \<Longrightarrow> rel_tr_refinement peterson_sr (\<lambda>s. invs s \<and> ab_label s ident = Critical) (peterson_rel (other_ident ident)) False (do x <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
interference
od) (?g18 x y >>= ?g'18 x y)
 4. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 5. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do xa <- ?g18 x y;
y <- ?g'18 x y xa;
y <- cs2;
interference
od)
 6. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 7. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 8. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 9. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (8 subgoals):
 1. \<And>x y. True \<Longrightarrow> (\<forall>y. not_env_steps_first (do y <- cs2;
interference
od)) \<or> (\<forall>s s' t. peterson_sr s s' \<longrightarrow> peterson_rel (other_ident ident) s t = peterson_rel (other_ident ident) s' t)
 2. \<And>x y. True \<Longrightarrow> rel_tr_refinement peterson_sr (\<lambda>s. invs s \<and> ab_label s ident = Critical) (peterson_rel (other_ident ident)) False (do x <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
interference
od) (?g18 x y >>= ?g'18 x y)
 3. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 4. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do xa <- ?g18 x y;
y <- ?g'18 x y xa;
y <- cs2;
interference
od)
 5. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 6. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 7. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>x y. True \<Longrightarrow> rel_tr_refinement peterson_sr (\<lambda>s. invs s \<and> ab_label s ident = Critical) (peterson_rel (other_ident ident)) False (do x <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
interference
od) (?g18 x y >>= ?g'18 x y)
 2. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 3. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do xa <- ?g18 x y;
y <- ?g'18 x y xa;
y <- cs2;
interference
od)
 4. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 6. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (9 subgoals):
 1. \<And>x y. True \<Longrightarrow> \<forall>s. invs s \<and> ab_label s ident = Critical \<longrightarrow> peterson_sr (s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) s
 2. \<And>x y. True \<Longrightarrow> \<forall>s t. invs s \<and> ab_label s ident = Critical \<longrightarrow> peterson_rel (other_ident ident) s t \<longrightarrow> invs t \<and> ab_label t ident = Critical
 3. \<And>x y. True \<Longrightarrow> \<forall>s0 s. peterson_rel (other_ident ident) (s0\<lparr>cs1_v := cs1 (cs2_v s0)\<rparr>) s \<longrightarrow> invs s0 \<and> ab_label s0 ident = Critical \<longrightarrow> (\<exists>s_pre. s = s_pre\<lparr>cs1_v := cs1 (cs2_v s_pre)\<rparr> \<and> peterson_rel (other_ident ident) s0 s_pre)
 4. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 5. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do x <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 6. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 7. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 8. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 9. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (8 subgoals):
 1. \<And>x y. True \<Longrightarrow> \<forall>s t. invs s \<and> ab_label s ident = Critical \<longrightarrow> peterson_rel (other_ident ident) s t \<longrightarrow> invs t \<and> ab_label t ident = Critical
 2. \<And>x y. True \<Longrightarrow> \<forall>s0 s. peterson_rel (other_ident ident) (s0\<lparr>cs1_v := cs1 (cs2_v s0)\<rparr>) s \<longrightarrow> invs s0 \<and> ab_label s0 ident = Critical \<longrightarrow> (\<exists>s_pre. s = s_pre\<lparr>cs1_v := cs1 (cs2_v s_pre)\<rparr> \<and> peterson_rel (other_ident ident) s0 s_pre)
 3. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 4. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do x <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 5. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 6. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 7. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>x y. True \<Longrightarrow> \<forall>s0 s. peterson_rel (other_ident ident) (s0\<lparr>cs1_v := cs1 (cs2_v s0)\<rparr>) s \<longrightarrow> invs s0 \<and> ab_label s0 ident = Critical \<longrightarrow> (\<exists>s_pre. s = s_pre\<lparr>cs1_v := cs1 (cs2_v s_pre)\<rparr> \<and> peterson_rel (other_ident ident) s0 s_pre)
 2. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 3. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do x <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 4. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 6. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>ab_v ab_label t_v cs1_v cs2_v ab_va ab_labela t_va cs1_va cs2_va. \<lbrakk>peterson_rel (other_ident ident) \<lparr>ab_v = ab_v, ab_label = ab_label, t_v = t_v, cs1_v = cs1 cs2_v, cs2_v = cs2_v\<rparr> \<lparr>ab_v = ab_va, ab_label = ab_labela, t_v = t_va, cs1_v = cs1_va, cs2_v = cs2_va\<rparr>; invs \<lparr>ab_v = ab_v, ab_label = ab_label, t_v = t_v, cs1_v = cs1_v, cs2_v = cs2_v\<rparr>; ab_label ident = Critical\<rbrakk> \<Longrightarrow> cs1_va = cs1 cs2_va \<and> (\<exists>cs1_va. peterson_rel (other_ident ident) \<lparr>ab_v = ab_v, ab_label = ab_label, t_v = t_v, cs1_v = cs1_v, cs2_v = cs2_v\<rparr> \<lparr>ab_v = ab_va, ab_label = ab_labela, t_v = t_va, cs1_v = cs1_va, cs2_v = cs2_va\<rparr>)
 2. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 3. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do x <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 4. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 6. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (6 subgoals):
 1. \<And>x y. True \<Longrightarrow> equivp peterson_sr
 2. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do x <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 3. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 5. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''7 x) (?Q'14 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do x <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 2. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ?Q'14 y s0\<rbrace>
 4. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (8 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (?rvr43 x y) (?P44 x) (?Q46 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) interference interference
 2. \<And>x y xa ya. \<lbrakk>True; ?rvr43 x y xa ya\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''43 x y xa) (?Q''43 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 3. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''43 x y\<rbrace>
 4. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''43 x y\<rbrace>
 5. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. ?P44 x and ?P'45 x\<rbrace>
 6. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and (?Q46 y and ?Q'47 y) s0\<rbrace>
 7. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''43 x y xa) (?Q''43 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od) (do y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od)
 2. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''43 x y\<rbrace>
 3. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''43 x y\<rbrace>
 4. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'45 x\<rbrace>
 5. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ((\<lambda>t0 t. True) and ?Q'47 y) s0\<rbrace>
 6. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (10 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> prefix_refinement peterson_sr peterson_sr peterson_sr_cs1 (?rvr53 x y xa ya) (?P54 x y xa) (?Q56 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>)) (modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>))
 2. \<And>x y xa ya xb yb. \<lbrakk>True; True; ?rvr53 x y xa ya xb yb\<rbrakk> \<Longrightarrow> prefix_refinement peterson_sr peterson_sr_cs1 peterson_sr (\<lambda>_ _. True) (?P''53 x y xa ya xb) (?Q''53 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- cs2;
interference
od) (do y <- cs2;
interference
od)
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'55 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>?P''53 x y xa ya\<rbrace>
 4. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>?Q''53 x y xa ya\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. ?P54 x y xa and ?P'55 x y xa\<rbrace>
 6. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. ?Q56 x y ya and ?Q'57 x y ya\<rbrace>
 7. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'45 x\<rbrace>
 8. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ((\<lambda>t0 t. True) and ?Q'47 y) s0\<rbrace>
 9. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 10. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (10 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<forall>s t. peterson_sr s t \<longrightarrow> True \<longrightarrow> True \<longrightarrow> peterson_sr_cs1 (s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) (t\<lparr>cs1_v := cs1 (cs2_v t)\<rparr>)
 2. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> prefix_refinement peterson_sr peterson_sr_cs1 peterson_sr (\<lambda>_ _. True) (?P''53 x y xa ya xb) (?Q''53 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- cs2;
interference
od) (do y <- cs2;
interference
od)
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'55 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>?P''53 x y xa ya\<rbrace>
 4. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>?Q''53 x y xa ya\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>_ _. True) and ?P'55 x y xa\<rbrace>
 6. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>_ _. True) and ?Q'57 x y ya\<rbrace>
 7. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'45 x\<rbrace>
 8. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ((\<lambda>t0 t. True) and ?Q'47 y) s0\<rbrace>
 9. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 10. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (9 subgoals):
 1. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> prefix_refinement peterson_sr peterson_sr_cs1 peterson_sr (\<lambda>_ _. True) (?P''53 x y xa ya xb) (?Q''53 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- cs2;
interference
od) (do y <- cs2;
interference
od)
 2. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'55 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>?P''53 x y xa ya\<rbrace>
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>?Q''53 x y xa ya\<rbrace>
 4. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>_ _. True) and ?P'55 x y xa\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>_ _. True) and ?Q'57 x y ya\<rbrace>
 6. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'45 x\<rbrace>
 7. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ((\<lambda>t0 t. True) and ?Q'47 y) s0\<rbrace>
 8. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 9. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (12 subgoals):
 1. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> prefix_refinement peterson_sr peterson_sr_cs1 peterson_sr (?rvr64 x y xa ya xb yb) (?P65 x y xa ya xb) (?Q67 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) cs2 cs2
 2. \<And>x y xa ya xb yb xc yc. \<lbrakk>True; True; True; ?rvr64 x y xa ya xb yb xc yc\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''64 x y xa ya xb yb xc) (?Q''64 x y xa ya xb yb yc) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) interference interference
 3. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'66 x y xa ya xb\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 -, \<lbrace>?P''64 x y xa ya xb yb\<rbrace>
 4. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 x y xa ya yb\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 -, \<lbrace>?Q''64 x y xa ya xb yb\<rbrace>
 5. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'55 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>\<lambda>xb. ?P65 x y xa ya xb and ?P'66 x y xa ya xb\<rbrace>
 6. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>\<lambda>yb. ?Q67 x y xa ya yb and ?Q'68 x y xa ya yb\<rbrace>
 7. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>_ _. True) and ?P'55 x y xa\<rbrace>
 8. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>_ _. True) and ?Q'57 x y ya\<rbrace>
 9. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'45 x\<rbrace>
 10. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ((\<lambda>t0 t. True) and ?Q'47 y) s0\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x y xa ya xb yb xc yc. \<lbrakk>True; True; True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''64 x y xa ya xb yb xc) (?Q''64 x y xa ya xb yb yc) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) interference interference
 2. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'66 x y xa ya xb\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 -, \<lbrace>?P''64 x y xa ya xb yb\<rbrace>
 3. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 x y xa ya yb\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 -, \<lbrace>?Q''64 x y xa ya xb yb\<rbrace>
 4. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'55 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>\<lambda>xb. (\<lambda>_ s. cs1_v s = cs1 (cs2_v s)) and ?P'66 x y xa ya xb\<rbrace>
 5. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>\<lambda>yb. (\<lambda>_ _. True) and ?Q'68 x y xa ya yb\<rbrace>
 6. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>_ _. True) and ?P'55 x y xa\<rbrace>
 7. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>_ _. True) and ?Q'57 x y ya\<rbrace>
 8. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'45 x\<rbrace>
 9. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ((\<lambda>t0 t. True) and ?Q'47 y) s0\<rbrace>
 10. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'66 x y xa ya xb\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 -, \<lbrace>\<lambda>xc _ _. True\<rbrace>
 2. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 x y xa ya yb\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 -, \<lbrace>\<lambda>yc t0 t. True\<rbrace>
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'55 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>\<lambda>xb. (\<lambda>_ s. cs1_v s = cs1 (cs2_v s)) and ?P'66 x y xa ya xb\<rbrace>
 4. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) -, \<lbrace>\<lambda>yb. (\<lambda>_ _. True) and ?Q'68 x y xa ya yb\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?P'45 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>_ _. True) and ?P'55 x y xa\<rbrace>
 6. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'47 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>_ _. True) and ?Q'57 x y ya\<rbrace>
 7. \<lbrace>?P'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'45 x\<rbrace>
 8. \<lbrace>?Q'7\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>y s0. (\<lambda>s. invs s \<and> ab_label s ident = Critical) and ((\<lambda>t0 t. True) and ?Q'47 y) s0\<rbrace>
 9. \<forall>s s0. invs s \<and> ab_label s ident = Critical \<longrightarrow> ((\<lambda>_ _. True) and ?P'7) s0 s
 10. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Critical \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'7) t0 t proof (prove)
goal (1 subgoal):
 1. \<And>s t s0 x s'. \<lbrakk>peterson_sr s t; peterson_sr s0 x; invs s; ab_label s ident = Critical; peterson_rel (other_ident ident) t s'\<rbrakk> \<Longrightarrow> invs s' \<and> ab_label s' ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s t s0 x s'. \<lbrakk>peterson_sr s t; peterson_sr s0 x; invs s; ab_label s ident = Critical; peterson_rel (other_ident ident) t s'\<rbrakk> \<Longrightarrow> invs s' \<and> ab_label t ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s t s0 x s'. \<lbrakk>peterson_sr s t; peterson_sr s0 x; invs s; ab_label s ident = Critical; invs s'\<rbrakk> \<Longrightarrow> invs s' \<and> ab_label t ident = Critical proof (prove)
goal:
No subgoals!