Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section delUsrGrpFromAclIsSecure. 
 
Lemma DelUsrGrpFromAclPSS :
 forall (s t : SFSstate) (u : SUBJECT),
 SecureState s -> TransFunc u s DelUsrGrpFromAcl t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : SecureState s) (_ : TransFunc u s DelUsrGrpFromAcl 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
unfold SecureState in |- *. 
(* Goal: and (DACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s))) (MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s))) *)
BreakSS. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: DACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
unfold DACSecureState in |- *. 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y0) pu then root else owner y0) (group y0) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y0)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y0)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y0)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y0)) (if SUBeq_dec (owner y0) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y0))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y1) pu then root else owner y1) (group y1) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y1)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y1)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y1)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y1)) (if SUBeq_dec (owner y1) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y1))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y0) pu then root else owner y0) (group y0) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y0)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y0)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y0)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y0)) (if SUBeq_dec (owner y0) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y0))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y1) pu then root else owner y1) (group y1) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y1)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y1)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y1)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y1)) (if SUBeq_dec (owner y1) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y1))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
simpl in |- *. 
(* Goal: forall o0 : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
elim (OBJeq_dec o o0). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
rewrite <- a. 
(* Goal: match fsecmat (secmat s) o 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o) | None => True end *)
(* Goal: forall _ : not (@eq OBJECT o o0), 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
cut (fsecmat (secmat s) o = None). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: match fsecmat (secmat s) o 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o) | None => True end *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
(* Goal: forall _ : not (@eq OBJECT o o0), 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
rewrite H7. 
(* Goal: True *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
(* Goal: forall _ : not (@eq OBJECT o o0), 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
eauto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
(* Goal: forall _ : not (@eq OBJECT o o0), 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
unfold fsecmat in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
cut
 (match fsecmat (secmat s) o0 with
  | Some y => set_In u0 (ActReaders y) -> PreDACRead s u0 o0
  | None => True
  end /\
  match fsecmat (secmat s) o0 with
  | Some y => set_In u0 (ActWriters y) -> PreDACWrite s u0 o0
  | None => True
  end). 
(* Goal: forall _ : and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end, 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
elim (fsecmat (secmat s) o0). 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), PreDACRead s u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters a), PreDACWrite s u0 o0)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters a), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0 o0) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
unfold PreDACRead, PreDACWrite, delUsrGrpFromAcl_acl in |- *. 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y0) pu then root else owner y0) (group y0) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y0)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y0)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y0)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y0)) (if SUBeq_dec (owner y0) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y0))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y1) pu then root else owner y1) (group y1) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y1)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y1)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y1)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y1)) (if SUBeq_dec (owner y1) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y1))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y0) pu then root else owner y0) (group y0) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y0)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y0)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y0)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y0)) (if SUBeq_dec (owner y0) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y0))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s))) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) match facl (acl s) o with | Some y0 => match match facl (acl s) o with | Some y1 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y1) pu then root else owner y1) (group y1) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y1)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y1)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y1)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y1)) (if SUBeq_dec (owner y1) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y1)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y1))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y0) (acl s)) | None => acl s end | None => acl s end (secmat s) (files s) (directories s)) g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
simpl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y0) pu then root else owner y0) (group y0) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y0)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y0)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y0)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y0)) (if SUBeq_dec (owner y0) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y0))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (facl (acl s) o). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
replace
 (facl
    (set_add ACLeq_dec
       (o,
       acldata
         match SUBeq_dec (owner a) pu with
         | left _ => root
         | right _ => owner a
         end (group a) (set_remove SUBeq_dec ru (UsersReaders a))
         (set_remove GRPeq_dec rg (GroupReaders a))
         (set_remove SUBeq_dec wu (UsersWriters a))
         (set_remove GRPeq_dec wg (GroupWriters a))
         match SUBeq_dec (owner a) pu with
         | left _ =>
             set_add SUBeq_dec root (set_remove SUBeq_dec pu (UsersOwners a))
         | right _ => set_remove SUBeq_dec pu (UsersOwners a)
         end (set_remove GRPeq_dec pg (GroupOwners a)))
       (set_remove ACLeq_dec (o, a) (acl s))) o0) with 
 (facl (acl s) o0). 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata (if SUBeq_dec (owner a) pu then root else owner a) (group a) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders a)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders a)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters a)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters a)) (if SUBeq_dec (owner a) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners a)))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
elim (facl (acl s) o0). 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata (if SUBeq_dec (owner a) pu then root else owner a) (group a) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders a)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders a)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters a)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters a)) (if SUBeq_dec (owner a) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners a)))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersReaders y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters a), match facl (acl s) o0 with | Some y => or (@set_In SUBJECT u0 (UsersWriters y)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y)))) | None => False end) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
unfold facl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o0 | None => True end *)
(* Goal: match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
apply ReadWriteImpRead. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: match fsecmat (secmat s) o0 with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o0 | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) *)
apply ReadWriteImpWrite. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma DelUsrGrpFromAclPSP :
 forall (s t : SFSstate) (u : SUBJECT),
 StarProperty s -> TransFunc u s DelUsrGrpFromAcl t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : StarProperty s) (_ : TransFunc u s DelUsrGrpFromAcl t), StarProperty t *)
StartPSP. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H; auto. 
Qed. 
 
 
Lemma DelUsrGrpFromAclPCP :
 forall s t : SFSstate, PreservesControlProp s DelUsrGrpFromAcl t. 
intros; 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H7. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H9. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJeq_dec o o0); intro y0. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite <- y0; auto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H11 in H10; inversion H10; auto. 
 
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) o0 = facl (acl s) o0). 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro H12; rewrite H12 in H9; rewrite H8 in H9; injection H9; auto. 
 
symmetry  in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold delUsrGrpFromAcl_acl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y0) pu then root else owner y0) (group y0) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y0)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y0)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y0)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y0)) (if SUBeq_dec (owner y0) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y0))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (facl (acl s) o). 
(* Goal: forall a : AccessCtrlListData, @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata (if SUBeq_dec (owner a) pu then root else owner a) (group a) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders a)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders a)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters a)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters a)) (if SUBeq_dec (owner a) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners a)))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro; unfold facl in |- *; apply AddRemEq. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H9. 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJeq_dec o o0); intro. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite <- a; auto. 
 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq AccessCtrlListData y z, ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H11 in H10; inversion H10; auto. 
 
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) o0 = facl (acl s) o0). 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro H11; rewrite H11 in H9; rewrite H8 in H9; injection H9; auto. 
 
symmetry  in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold delUsrGrpFromAcl_acl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl match facl (acl s) o with | Some y => match match facl (acl s) o with | Some y0 => @Some AccessCtrlListData (acldata (if SUBeq_dec (owner y0) pu then root else owner y0) (group y0) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders y0)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders y0)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters y0)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters y0)) (if SUBeq_dec (owner y0) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners y0)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners y0))) | None => @None AccessCtrlListData end with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o z) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s)) | None => acl s end | None => acl s end o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (facl (acl s) o). 
(* Goal: forall a : AccessCtrlListData, @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o (acldata (if SUBeq_dec (owner a) pu then root else owner a) (group a) (@set_remove SUBJECT SUBeq_dec ru (UsersReaders a)) (@set_remove GRPNAME GRPeq_dec rg (GroupReaders a)) (@set_remove SUBJECT SUBeq_dec wu (UsersWriters a)) (@set_remove GRPNAME GRPeq_dec wg (GroupWriters a)) (if SUBeq_dec (owner a) pu then @set_add SUBJECT SUBeq_dec root (@set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) else @set_remove SUBJECT SUBeq_dec pu (UsersOwners a)) (@set_remove GRPNAME GRPeq_dec pg (GroupOwners a)))) (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o a) (acl s))) o0) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro; unfold facl in |- *; apply AddRemEq. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
intro;
 absurd
  (MACObjCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s)
        (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) 
        (secmat s) (files s) (directories s)) o0); 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 auto. 
 
intros;
 absurd
  (MACSubCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s)
        (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) 
        (secmat s) (files s) (directories s)) u0); 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (acl s) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) 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) (objectSC s) (delUsrGrpFromAcl_acl s o ru wu pu rg wg pg) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 auto. 
 
Qed. 
 
 
End delUsrGrpFromAclIsSecure. 
 
Hint Resolve DelUsrGrpFromAclPSS DelUsrGrpFromAclPSP DelUsrGrpFromAclPCP. 
 