Require Import ModelProperties.
Require Import AuxiliaryLemmas.

Section rmdirIsSecure. 
 
Lemma RmdirPSS :
 forall (s t : SFSstate) (u : SUBJECT),
 SecureState s -> TransFunc u s Rmdir t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : SecureState s) (_ : TransFunc u s Rmdir t), SecureState t *)
StartPSS. 
(* Goal: and (forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s t o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s t o, @set_In SUBJECT Sub (groups s (SecAdmGrp s)))) (forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s t u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
inversion H. 
(* Goal: SecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
unfold SecureState in |- *; BreakSS; split. 
(* Goal: DACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
unfold DACSecureState in |- *; simpl in |- *; intros. 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
elim (OBJeq_dec o o0); intros. 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
rewrite <- a. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (rmdir_oSC s o) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some x => match fOSC (rmdir_oSC s o) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o) with (None (A:=ReadersWriters)). 
(* Goal: True *)
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) o) *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
unfold PreDACRead, PreDACWrite in |- *; simpl in |- *. 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), match facl (rmdir_acl s o) o0 with | Some y0 => or (@set_In SUBJECT u0 (UsersReaders y0)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y0)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters y), match facl (rmdir_acl s o) o0 with | Some y0 => or (@set_In SUBJECT u0 (UsersWriters y0)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y0)))) | None => False end) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
replace (facl (rmdir_acl s o) o0) with (facl (acl s) o0). 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), match facl (acl s) o0 with | Some y0 => or (@set_In SUBJECT u0 (UsersReaders y0)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y0)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters y), match facl (acl s) o0 with | Some y0 => or (@set_In SUBJECT u0 (UsersWriters y0)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y0)))) | None => False end) | None => True end *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (rmdir_acl s o) o0) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
unfold DACSecureState, PreDACRead, PreDACWrite in DAC; apply DAC. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
auto. 
 
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
unfold MACSecureState in |- *; simpl in |- *. 
(* Goal: forall o0 : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (rmdir_oSC s o) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
elim (OBJeq_dec o o0). 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
intro; rewrite <- a. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (rmdir_oSC s o) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some x => match fOSC (rmdir_oSC s o) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o) with (None (A:=ReadersWriters)). 
(* Goal: True *)
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) o) *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
elim (fOSC (rmdir_oSC s o) o); elim (fSSC (subjectSC s) u0); trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: forall _ : not (@eq OBJECT o o0), match fsecmat (secmat s) o0 with | Some x => match fOSC (rmdir_oSC s o) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
intro EQ. 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (rmdir_oSC s o) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fOSC (rmdir_oSC s o) o0) with (fOSC (objectSC s) o0). 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o0) (fOSC (rmdir_oSC s o) o0) *)
unfold MACSecureState in MAC; apply MAC. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
auto. 
 
Qed. 
 
 
Lemma RmdirPSP :
 forall (s t : SFSstate) (u : SUBJECT),
 StarProperty s -> TransFunc u s Rmdir t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : StarProperty s) (_ : TransFunc u s Rmdir t), StarProperty t *)
StartPSP. 
(* Goal: and (forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s t o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s t o, @set_In SUBJECT Sub (groups s (SecAdmGrp s)))) (forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s t u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
inversion H. 
(* Goal: forall o0 : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold StarProperty in |- *; simpl in |- *; intros. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
elim (OBJeq_dec o o1); elim (OBJeq_dec o o2); intros EQ2 EQ1. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o1) with (None (A:=ReadersWriters)). 
elim (fOSC (objectSC s) o2); elim (fOSC (objectSC s) o1);
 elim (fOSC (rmdir_oSC s o) o2); elim (fOSC (rmdir_oSC s o) o1);
(* Goal: True *)
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) o) *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
 elim (fsecmat (secmat s) o2); trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
rewrite <- EQ1; symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o1) with (None (A:=ReadersWriters)). 
elim (fsecmat (secmat s) o2); elim (fOSC (objectSC s) o2);
 elim (fOSC (objectSC s) o1); elim (fOSC (rmdir_oSC s o) o2);
(* Goal: True *)
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) o) *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
 elim (fOSC (rmdir_oSC s o) o1); trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
rewrite <- EQ1; symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o2) with (None (A:=ReadersWriters)). 
elim (fsecmat (secmat s) o1); elim (fOSC (objectSC s) o2);
 elim (fOSC (objectSC s) o1); elim (fOSC (rmdir_oSC s o) o2);
(* Goal: True *)
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) o) *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) *)
 elim (fOSC (rmdir_oSC s o) o1); trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
rewrite <- EQ2; symmetry  in |- *; unfold fsecmat in |- *; auto. 
 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (rmdir_oSC s o) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fOSC (rmdir_oSC s o) o2) with (fOSC (objectSC s) o2). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (objectSC s) o2 with | Some y => match fOSC (rmdir_oSC s o) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
replace (fOSC (rmdir_oSC s o) o1) with (fOSC (objectSC s) o1). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (objectSC s) o2 with | Some y => match fOSC (objectSC s) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o1) (fOSC (rmdir_oSC s o) o1) *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
unfold StarProperty in SP; apply SP. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
auto. 
 
Qed. 
 
 
Lemma RmdirPCP :
 forall s t : SFSstate,
 FuncPre4 s -> FuncPre6 s -> PreservesControlProp s Rmdir t. 
intros s t FP4 FP6; unfold PreservesControlProp in |- *; intros Sub TF;
 inversion TF; unfold ControlProperty in |- *. 
(* Goal: and (forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s t o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s t o, @set_In SUBJECT Sub (groups s (SecAdmGrp s)))) (forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s t u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
inversion H. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall o0 : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H8. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJeq_dec o o0); simpl in H10; intro y0. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
tauto. 
 
(* Goal: False *)
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite y0 in H10. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
eauto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro; rewrite H12 in H11; cut False; [ tauto | inversion H11; auto ]. 
 
cut (facl (acl s) o0 = facl (rmdir_acl s o) o0);
 [ rewrite H9; rewrite H10; intro; injection H12; auto | auto ]. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJeq_dec o o0); simpl in H10; intro y0. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
tauto. 
 
(* Goal: False *)
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite y0 in H10. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
eauto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro; rewrite H12 in H11; cut False; [ tauto | inversion H11; auto ]. 
 
cut (facl (acl s) o0 = facl (rmdir_acl s o) o0);
 [ rewrite H10; rewrite H9; intro; injection H12; auto | auto ]. 
 
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H8. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJeq_dec o o0); simpl in H10; intros y0. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
tauto. 
 
(* Goal: False *)
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite y0 in H10. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
eauto. 
 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (x = y). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro; rewrite H12 in H11; cut False; [ tauto | inversion H11; auto ]. 
 
cut (fOSC (objectSC s) o0 = fOSC (rmdir_oSC s o) o0);
 [ rewrite H10; rewrite H9; intro; injection H12; auto | auto ]. 
 
intros;
 absurd
  (MACSubCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) 
        (rmdir_acl s o) (secmat s) (files s) (rmdir_directories o)) u0); 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (rmdir_oSC s o) o2) *)
 auto. 
 
Qed. 
 
 
End rmdirIsSecure. 
 
Hint Resolve RmdirPSS RmdirPSP RmdirPCP. 
 