theory Peterson_Atomicity

lemma acquire_lock_refinement:
  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
    \<top>\<top> \<top>\<top>
    (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
    (acquire_lock ident) (acquire_lock ident)" apply (unfold acquire_lock_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_interference_peterson) apply (simp add: modify_modify_bind) apply (rule prefix_refinement_bind_sr) apply (rule pfx_refn_modifyT) apply (clarsimp simp add: peterson_sr_def set_label_def set_ab_def forall_ident_eq) apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_interference_peterson) apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_Await[OF env_stable_peterson_sr abs_rely_stableT]) apply (clarsimp simp add: peterson_sr_def locked_def) apply (clarsimp simp add: peterson_sr_def locked_def) apply (rule pfx_refn_modifyT) apply (clarsimp simp add: peterson_sr_def set_label_def) apply (wpsimp wp: Await_sync_twp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (acquire_lock ident) (acquire_lock ident) proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do interference;
modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od) (do interference;
modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od) proof (prove)
goal (3 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) ?P' ?Q' (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do interference;
modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od) (do interference;
modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od)
 2. \<forall>s s0. True \<longrightarrow> ?P' s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ?Q' t0 t proof (prove)
goal (6 subgoals):
 1. pfx_refn peterson_sr ?rvr4 ?P4 ?Q4 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) interference interference
 2. \<And>x y. ?rvr4 x y \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind (do modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od) x) (K_bind (do modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od) y)
 3. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''4\<rbrace>
 5. \<forall>s s0. True \<longrightarrow> (?P4 and ?P'4) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind (do modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od) x) (K_bind (do modify (set_ab ident True);
modify (t_v_update (\<lambda>_. other_ident ident));
modify (set_label ident Awaiting);
interference;
Await (locked ident);
modify (set_label ident Critical)
od) y)
 2. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''4\<rbrace>
 4. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 ()) (?Q''4 ()) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True);
y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od) (do y <- modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True);
y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od)
 2. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''4\<rbrace>
 4. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal (8 subgoals):
 1. pfx_refn peterson_sr ?rvr10 (?P18 ()) (?Q16 ()) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True)) (modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True))
 2. \<And>x y. ?rvr10 x y \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''10 x) (?Q''10 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od) (do y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od)
 3. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>?P''10\<rbrace>
 4. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>?Q''10\<rbrace>
 5. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. ?P18 a and ?P'17 a\<rbrace>
 6. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. ?Q16 a and ?Q'15 a\<rbrace>
 7. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal (8 subgoals):
 1. \<forall>s t. peterson_sr s t \<longrightarrow> True \<longrightarrow> True \<longrightarrow> peterson_sr ((set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) s) ((set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) t)
 2. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''10 x) (?Q''10 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od) (do y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od)
 3. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>?P''10\<rbrace>
 4. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>?Q''10\<rbrace>
 5. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 6. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
 7. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''10 x) (?Q''10 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od) (do y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od)
 2. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>?P''10\<rbrace>
 3. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>?Q''10\<rbrace>
 4. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 5. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
 6. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal (10 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (?rvr25 x y) (?P26 x) (?Q28 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) interference interference
 2. \<And>x y xa ya. \<lbrakk>True; ?rvr25 x y xa ya\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''25 x y xa) (?Q''25 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- Await (locked ident);
modify (set_label ident Critical)
od) (do y <- Await (locked ident);
modify (set_label ident Critical)
od)
 3. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''25 x y\<rbrace>
 4. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''25 x y\<rbrace>
 5. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. ?P26 x and ?P'27 x\<rbrace>
 6. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. ?Q28 y and ?Q'29 y\<rbrace>
 7. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 8. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
 9. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 10. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal (9 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''25 x y xa) (?Q''25 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- Await (locked ident);
modify (set_label ident Critical)
od) (do y <- Await (locked ident);
modify (set_label ident Critical)
od)
 2. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?P''25 x y\<rbrace>
 3. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>?Q''25 x y\<rbrace>
 4. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'27 x\<rbrace>
 5. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. (\<lambda>t0 t. True) and ?Q'29 y\<rbrace>
 6. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 7. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
 8. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 9. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal (12 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (?rvr35 x y xa ya) (?P36 x y xa) (?Q38 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (Await (locked ident)) (Await (locked ident))
 2. \<And>x y xa ya xb yb. \<lbrakk>True; True; ?rvr35 x y xa ya xb yb\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''35 x y xa ya xb) (?Q''35 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (modify (set_label ident Critical)) (modify (set_label ident Critical))
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'37 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?P''35 x y xa ya\<rbrace>
 4. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'39 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?Q''35 x y xa ya\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. ?P36 x y xa and ?P'37 x y xa\<rbrace>
 6. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. ?Q38 x y ya and ?Q'39 x y ya\<rbrace>
 7. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'27 x\<rbrace>
 8. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. (\<lambda>t0 t. True) and ?Q'29 y\<rbrace>
 9. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 10. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<forall>s t. True \<longrightarrow> True \<longrightarrow> peterson_sr s t \<longrightarrow> locked ident t \<longrightarrow> locked ident s
 2. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> (\<exists>s. locked ident s) \<longrightarrow> (\<exists>s. locked ident s)
 3. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''35 x y xa ya xb) (?Q''35 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (modify (set_label ident Critical)) (modify (set_label ident Critical))
 4. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'37 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?P''35 x y xa ya\<rbrace>
 5. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'39 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?Q''35 x y xa ya\<rbrace>
 6. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>s0 s. s0 = s \<and> True) and ?P'37 x y xa\<rbrace>
 7. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>t0 t. t0 = t \<and> True) and ?Q'39 x y ya\<rbrace>
 8. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'27 x\<rbrace>
 9. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. (\<lambda>t0 t. True) and ?Q'29 y\<rbrace>
 10. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> (\<exists>s. locked ident s) \<longrightarrow> (\<exists>s. locked ident s)
 2. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''35 x y xa ya xb) (?Q''35 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (modify (set_label ident Critical)) (modify (set_label ident Critical))
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'37 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?P''35 x y xa ya\<rbrace>
 4. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'39 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?Q''35 x y xa ya\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>s0 s. s0 = s \<and> True) and ?P'37 x y xa\<rbrace>
 6. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>t0 t. t0 = t \<and> True) and ?Q'39 x y ya\<rbrace>
 7. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'27 x\<rbrace>
 8. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. (\<lambda>t0 t. True) and ?Q'29 y\<rbrace>
 9. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 10. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''35 x y xa ya xb) (?Q''35 x y xa ya yb) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (modify (set_label ident Critical)) (modify (set_label ident Critical))
 2. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'37 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?P''35 x y xa ya\<rbrace>
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'39 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>?Q''35 x y xa ya\<rbrace>
 4. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>s0 s. s0 = s \<and> True) and ?P'37 x y xa\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>t0 t. t0 = t \<and> True) and ?Q'39 x y ya\<rbrace>
 6. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'27 x\<rbrace>
 7. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. (\<lambda>t0 t. True) and ?Q'29 y\<rbrace>
 8. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 9. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
 10. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x y xa ya xb yb. \<lbrakk>True; True; True\<rbrakk> \<Longrightarrow> \<forall>s t. peterson_sr s t \<longrightarrow> True \<longrightarrow> True \<longrightarrow> peterson_sr (set_label ident Critical s) (set_label ident Critical t)
 2. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'37 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>\<lambda>xb _ _. True\<rbrace>
 3. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'39 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>\<lambda>yb _ _. True\<rbrace>
 4. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>s0 s. s0 = s \<and> True) and ?P'37 x y xa\<rbrace>
 5. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>t0 t. t0 = t \<and> True) and ?Q'39 x y ya\<rbrace>
 6. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'27 x\<rbrace>
 7. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. (\<lambda>t0 t. True) and ?Q'29 y\<rbrace>
 8. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 9. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
 10. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?P'37 x y xa\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>\<lambda>xb _ _. True\<rbrace>
 2. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> \<lbrace>?Q'39 x y ya\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> Await (locked ident) -, \<lbrace>\<lambda>yb _ _. True\<rbrace>
 3. \<And>x y. True \<Longrightarrow> \<lbrace>?P'27 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>xa. (\<lambda>s0 s. s0 = s \<and> True) and ?P'37 x y xa\<rbrace>
 4. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'29 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>ya. (\<lambda>t0 t. t0 = t \<and> True) and ?Q'39 x y ya\<rbrace>
 5. \<lbrace>?P'17 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>x. (\<lambda>_ _. True) and ?P'27 x\<rbrace>
 6. \<lbrace>?Q'15 ()\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Awaiting \<circ> t_v_update (\<lambda>_. other_ident ident) \<circ> set_ab ident True) -, \<lbrace>\<lambda>y. (\<lambda>t0 t. True) and ?Q'29 y\<rbrace>
 7. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?P'17 a\<rbrace>
 8. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> interference -, \<lbrace>\<lambda>a. (\<lambda>a b. True) and ?Q'15 a\<rbrace>
 9. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 10. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>t0 t. True) and ?Q'4) t0 t proof (prove)
goal:
No subgoals!