theory Peterson_Atomicity

lemma peterson_proc_mutual_excl_helper':
  "\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
            \<and> ab_label s ident = Exited \<rbrace>,
   \<lbrace> peterson_rel (other_ident ident) \<rbrace>
     peterson_proc ident
   \<lbrace> peterson_rel2 ident \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. peterson_rel2 ident s0 s \<and> invs s
               \<and> ab_label s ident = Exited \<rbrace>" apply (simp add: peterson_proc_def acquire_lock_def release_lock_def
                   critical_section_def) apply (wp Await_sync_twp | simp add: split_def
         | rule rg_strengthen_guar[OF _ peterson_rel_peterson_rel2])+ apply (clarsimp simp: imp_conjL) apply (strengthen peterson_rel_imp_assume_invs | simp)+ apply (cases ident) apply (safe, simp_all) by ((clarsimp simp: peterson_rel_def peterson_rel2_def forall_ident_eq
                      set_label_def set_ab_def locked_def invs_defs cs_closed
    | rule invs_def[THEN iffD2] conjI
    | rev_drule invs_def[THEN iffD1])+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident \<lbrace>peterson_rel2 ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel2 ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> do y <- do y <- interference;
y <- modify (set_ab ident True);
y <- modify (t_v_update (\<lambda>_. other_ident ident));
y <- modify (set_label ident Awaiting);
y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od;
y <- do y <- interference;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- interference;
y <- cs2;
interference
od;
y <- modify (set_ab ident False);
y <- modify (set_label ident Exited);
interference
od \<lbrace>peterson_rel2 ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel2 ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<Longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) s s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) s'a \<longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s'a x \<and> locked ident x \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (set_label ident Critical x) s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (s'\<lparr>cs1_v := cs1 (cs2_v s')\<rparr>) s'a \<longrightarrow> csI (cs2_v s'a) \<and> invs s'a \<and> ab_label s'a ident = Critical \<and> cs1_v s'a = cs1 (cs2_v s'a) \<and> (\<forall>s0' c. csI c \<longrightarrow> (s0' = s'a \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (s'a\<lparr>cs2_v := c\<rparr>) s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False s')) s'a \<longrightarrow> peterson_rel2 ident s'a s'a \<and> invs s'a \<and> ab_label s'a ident = Exited) \<and> peterson_rel2 ident s' (set_label ident Exited (set_ab ident False s'))) \<and> peterson_rel2 ident s'a (s'a\<lparr>cs2_v := c\<rparr>)) \<and> ((\<exists>c'. s0' = s'a\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (s'a\<lparr>cs2_v := c\<rparr>) s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False s')) s'a \<longrightarrow> peterson_rel2 ident s'a s'a \<and> invs s'a \<and> ab_label s'a ident = Exited) \<and> peterson_rel2 ident s' (set_label ident Exited (set_ab ident False s'))) \<and> peterson_rel2 ident s0' (s'a\<lparr>cs2_v := c\<rparr>)))) \<and> peterson_rel2 ident s' (s'\<lparr>cs1_v := cs1 (cs2_v s')\<rparr>)) \<and> peterson_rel2 ident x (set_label ident Critical x))) \<and> peterson_rel2 ident s' (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>))) \<and> peterson_rel2 ident s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited\<rbrakk> \<Longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) s s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) s'a \<longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s'a x \<longrightarrow> locked ident x \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (set_label ident Critical x) s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (s'\<lparr>cs1_v := cs1 (cs2_v s')\<rparr>) s'a \<longrightarrow> csI (cs2_v s'a) \<and> invs s'a \<and> ab_label s'a ident = Critical \<and> cs1_v s'a = cs1 (cs2_v s'a) \<and> (\<forall>s0' c. csI c \<longrightarrow> (s0' = s'a \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (s'a\<lparr>cs2_v := c\<rparr>) s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False s')) s'a \<longrightarrow> peterson_rel2 ident s'a s'a \<and> invs s'a \<and> ab_label s'a ident = Exited) \<and> peterson_rel2 ident s' (set_label ident Exited (set_ab ident False s'))) \<and> peterson_rel2 ident s'a (s'a\<lparr>cs2_v := c\<rparr>)) \<and> ((\<exists>c'. s0' = s'a\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (s'a\<lparr>cs2_v := c\<rparr>) s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False s')) s'a \<longrightarrow> peterson_rel2 ident s'a s'a \<and> invs s'a \<and> ab_label s'a ident = Exited) \<and> peterson_rel2 ident s' (set_label ident Exited (set_ab ident False s'))) \<and> peterson_rel2 ident s0' (s'a\<lparr>cs2_v := c\<rparr>)))) \<and> peterson_rel2 ident s' (s'\<lparr>cs1_v := cs1 (cs2_v s')\<rparr>)) \<and> peterson_rel2 ident x (set_label ident Critical x))) \<and> peterson_rel2 ident s' (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>))) \<and> peterson_rel2 ident s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited\<rbrakk> \<Longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s x \<and> invs x \<longrightarrow> invs (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) \<and> (\<forall>xa. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) xa \<and> invs (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) \<and> invs xa \<longrightarrow> (\<forall>x. peterson_rel (other_ident ident) xa x \<and> invs x \<longrightarrow> locked ident x \<longrightarrow> invs (set_label ident Critical x) \<and> (\<forall>xa. peterson_rel (other_ident ident) (set_label ident Critical x) xa \<and> invs (set_label ident Critical x) \<and> invs xa \<longrightarrow> invs (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) x \<and> invs (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) \<and> invs x \<longrightarrow> csI (cs2_v x) \<and> ab_label x ident = Critical \<and> cs1_v x = cs1 (cs2_v x) \<and> (\<forall>xa xb. csI xb \<longrightarrow> (xa = x \<longrightarrow> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> invs (set_label ident Exited (set_ab ident False xa)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False xa)) x \<and> invs (set_label ident Exited (set_ab ident False xa)) \<and> invs x \<longrightarrow> peterson_rel2 ident x x \<and> ab_label x ident = Exited) \<and> peterson_rel2 ident xa (set_label ident Exited (set_ab ident False xa))) \<and> peterson_rel2 ident x (x\<lparr>cs2_v := xb\<rparr>)) \<and> ((\<exists>c'. xa = x\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> invs (set_label ident Exited (set_ab ident False xa)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False xa)) x \<and> invs (set_label ident Exited (set_ab ident False xa)) \<and> invs x \<longrightarrow> peterson_rel2 ident x x \<and> ab_label x ident = Exited) \<and> peterson_rel2 ident xa (set_label ident Exited (set_ab ident False xa))) \<and> peterson_rel2 ident xa (x\<lparr>cs2_v := xb\<rparr>)))) \<and> peterson_rel2 ident xa (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>)) \<and> peterson_rel2 ident x (set_label ident Critical x))) \<and> peterson_rel2 ident x (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>))) \<and> peterson_rel2 ident s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited; ident = A\<rbrakk> \<Longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s x \<and> invs x \<longrightarrow> invs (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) \<and> (\<forall>xa. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) xa \<and> invs (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) \<and> invs xa \<longrightarrow> (\<forall>x. peterson_rel (other_ident ident) xa x \<and> invs x \<longrightarrow> locked ident x \<longrightarrow> invs (set_label ident Critical x) \<and> (\<forall>xa. peterson_rel (other_ident ident) (set_label ident Critical x) xa \<and> invs (set_label ident Critical x) \<and> invs xa \<longrightarrow> invs (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) x \<and> invs (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) \<and> invs x \<longrightarrow> csI (cs2_v x) \<and> ab_label x ident = Critical \<and> cs1_v x = cs1 (cs2_v x) \<and> (\<forall>xa xb. csI xb \<longrightarrow> (xa = x \<longrightarrow> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> invs (set_label ident Exited (set_ab ident False xa)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False xa)) x \<and> invs (set_label ident Exited (set_ab ident False xa)) \<and> invs x \<longrightarrow> peterson_rel2 ident x x \<and> ab_label x ident = Exited) \<and> peterson_rel2 ident xa (set_label ident Exited (set_ab ident False xa))) \<and> peterson_rel2 ident x (x\<lparr>cs2_v := xb\<rparr>)) \<and> ((\<exists>c'. xa = x\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> invs (set_label ident Exited (set_ab ident False xa)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False xa)) x \<and> invs (set_label ident Exited (set_ab ident False xa)) \<and> invs x \<longrightarrow> peterson_rel2 ident x x \<and> ab_label x ident = Exited) \<and> peterson_rel2 ident xa (set_label ident Exited (set_ab ident False xa))) \<and> peterson_rel2 ident xa (x\<lparr>cs2_v := xb\<rparr>)))) \<and> peterson_rel2 ident xa (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>)) \<and> peterson_rel2 ident x (set_label ident Critical x))) \<and> peterson_rel2 ident x (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>))) \<and> peterson_rel2 ident s0 s
 2. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited; ident = B\<rbrakk> \<Longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s x \<and> invs x \<longrightarrow> invs (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) \<and> (\<forall>xa. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) xa \<and> invs (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>)) \<and> invs xa \<longrightarrow> (\<forall>x. peterson_rel (other_ident ident) xa x \<and> invs x \<longrightarrow> locked ident x \<longrightarrow> invs (set_label ident Critical x) \<and> (\<forall>xa. peterson_rel (other_ident ident) (set_label ident Critical x) xa \<and> invs (set_label ident Critical x) \<and> invs xa \<longrightarrow> invs (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) x \<and> invs (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>) \<and> invs x \<longrightarrow> csI (cs2_v x) \<and> ab_label x ident = Critical \<and> cs1_v x = cs1 (cs2_v x) \<and> (\<forall>xa xb. csI xb \<longrightarrow> (xa = x \<longrightarrow> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> invs (set_label ident Exited (set_ab ident False xa)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False xa)) x \<and> invs (set_label ident Exited (set_ab ident False xa)) \<and> invs x \<longrightarrow> peterson_rel2 ident x x \<and> ab_label x ident = Exited) \<and> peterson_rel2 ident xa (set_label ident Exited (set_ab ident False xa))) \<and> peterson_rel2 ident x (x\<lparr>cs2_v := xb\<rparr>)) \<and> ((\<exists>c'. xa = x\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> invs (set_label ident Exited (set_ab ident False xa)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Exited (set_ab ident False xa)) x \<and> invs (set_label ident Exited (set_ab ident False xa)) \<and> invs x \<longrightarrow> peterson_rel2 ident x x \<and> ab_label x ident = Exited) \<and> peterson_rel2 ident xa (set_label ident Exited (set_ab ident False xa))) \<and> peterson_rel2 ident xa (x\<lparr>cs2_v := xb\<rparr>)))) \<and> peterson_rel2 ident xa (xa\<lparr>cs1_v := cs1 (cs2_v xa)\<rparr>)) \<and> peterson_rel2 ident x (set_label ident Critical x))) \<and> peterson_rel2 ident x (set_label ident Awaiting (set_ab ident True x\<lparr>t_v := other_ident ident\<rparr>))) \<and> peterson_rel2 ident s0 s proof (prove)
goal (44 subgoals):
 1. \<And>s0 s x. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x\<rbrakk> \<Longrightarrow> invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>))
 2. \<And>s0 s x xa xb. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb\<rbrakk> \<Longrightarrow> invs (set_label A Critical xb)
 3. \<And>s0 s x xa xb xc. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc\<rbrakk> \<Longrightarrow> invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>)
 4. \<And>s0 s x xa xb xc xd. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc; peterson_rel B (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>) xd; invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>); invs xd\<rbrakk> \<Longrightarrow> csI (cs2_v xd)
 5. \<And>s0 s x xa xb xc xd. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc; peterson_rel B (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>) xd; invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>); invs xd\<rbrakk> \<Longrightarrow> ab_label xd A = Critical
 6. \<And>s0 s x xa xb xc xd. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc; peterson_rel B (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>) xd; invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>); invs xd\<rbrakk> \<Longrightarrow> cs1_v xd = cs1 (cs2_v xd)
 7. \<And>s0 s x xa xb xc xd xf. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc; peterson_rel B (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>) xd; invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>); invs xd; csI xf\<rbrakk> \<Longrightarrow> invs (xd\<lparr>cs2_v := xf\<rparr>)
 8. \<And>s0 s x xa xb xc xd xf xg. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc; peterson_rel B (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>) xd; invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>); invs xd; csI xf; peterson_rel B (xd\<lparr>cs2_v := xf\<rparr>) xg; invs (xd\<lparr>cs2_v := xf\<rparr>); invs xg\<rbrakk> \<Longrightarrow> invs (set_label A Exited (set_ab A False xg))
 9. \<And>s0 s x xa xb xc xd xf xg xh. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc; peterson_rel B (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>) xd; invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>); invs xd; csI xf; peterson_rel B (xd\<lparr>cs2_v := xf\<rparr>) xg; invs (xd\<lparr>cs2_v := xf\<rparr>); invs xg; peterson_rel B (set_label A Exited (set_ab A False xg)) xh; invs (set_label A Exited (set_ab A False xg)); invs xh\<rbrakk> \<Longrightarrow> peterson_rel2 A xh xh
 10. \<And>s0 s x xa xb xc xd xf xg xh. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; ident = A; peterson_rel B s x; invs x; peterson_rel B (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)) xa; invs (set_label A Awaiting (set_ab A True x\<lparr>t_v := B\<rparr>)); invs xa; peterson_rel B xa xb; invs xb; locked A xb; peterson_rel B (set_label A Critical xb) xc; invs (set_label A Critical xb); invs xc; peterson_rel B (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>) xd; invs (xc\<lparr>cs1_v := cs1 (cs2_v xc)\<rparr>); invs xd; csI xf; peterson_rel B (xd\<lparr>cs2_v := xf\<rparr>) xg; invs (xd\<lparr>cs2_v := xf\<rparr>); invs xg; peterson_rel B (set_label A Exited (set_ab A False xg)) xh; invs (set_label A Exited (set_ab A False xg)); invs xh\<rbrakk> \<Longrightarrow> ab_label xh A = Exited
A total of 44 subgoals...