Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section chmodIsSecure. 
 
Lemma ChmodPSS :
 forall (s t : SFSstate) (u : SUBJECT),
 SecureState s -> TransFunc u s Chmod t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : SecureState s) (_ : TransFunc u s Chmod 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s))) (MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chmod_acl s Sub o perms) (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 => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y1) (groupp perms) (GroupReaders y1))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y1) (groupp perms) (GroupWriters y1))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y0) (group y0) (ChangeUserR Sub (UsersReaders y0) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y0) (ownerp perms)) gaw (UsersOwners y0) (GroupOwners y0)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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 => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y2) (groupp perms) (GroupReaders y2))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y2) (groupp perms) (GroupWriters y2))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y1) (group y1) (ChangeUserR Sub (UsersReaders y1) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y1) (ownerp perms)) gaw (UsersOwners y1) (GroupOwners y1)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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 => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y1) (groupp perms) (GroupReaders y1))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y1) (groupp perms) (GroupWriters y1))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y0) (group y0) (ChangeUserR Sub (UsersReaders y0) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y0) (ownerp perms)) gaw (UsersOwners y0) (GroupOwners y0)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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 => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y2) (groupp perms) (GroupReaders y2))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y2) (groupp perms) (GroupWriters y2))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y1) (group y1) (ChangeUserR Sub (UsersReaders y1) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y1) (ownerp perms)) gaw (UsersOwners y1) (GroupOwners y1)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) *)
rewrite H6. 
(* 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) *)
unfold PreDACRead, PreDACWrite, chmod_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 => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y1) (groupp perms) (GroupReaders y1))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y1) (groupp perms) (GroupWriters y1))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y0) (group y0) (ChangeUserR Sub (UsersReaders y0) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y0) (ownerp perms)) gaw (UsersOwners y0) (GroupOwners y0)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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 => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y2) (groupp perms) (GroupReaders y2))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y2) (groupp perms) (GroupWriters y2))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y1) (group y1) (ChangeUserR Sub (UsersReaders y1) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y1) (ownerp perms)) gaw (UsersOwners y1) (GroupOwners y1)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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 => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y1) (groupp perms) (GroupReaders y1))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y1) (groupp perms) (GroupWriters y1))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y0) (group y0) (ChangeUserR Sub (UsersReaders y0) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y0) (ownerp perms)) gaw (UsersOwners y0) (GroupOwners y0)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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 => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y2) (groupp perms) (GroupReaders y2))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y2 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y2) (groupp perms) (GroupWriters y2))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y1) (group y1) (ChangeUserR Sub (UsersReaders y1) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y1) (ownerp perms)) gaw (UsersOwners y1) (GroupOwners y1)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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) (chmod_acl s Sub o perms) (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 => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y1) (groupp perms) (GroupReaders y1))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y1) (groupp perms) (GroupWriters y1))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y0) (group y0) (ChangeUserR Sub (UsersReaders y0) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y0) (ownerp perms)) gaw (UsersOwners y0) (GroupOwners y0)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
replace
 (facl
    (set_add ACLeq_dec
       (o,
       acldata (owner a) (group a)
         (ChangeUserR Sub (UsersReaders a) (ownerp perms))
         (ChangeGroupR (AllGrp s) (groupp perms)
            (ChangeGroupR (group a) (groupp perms) (GroupReaders a)))
         (ChangeUserW Sub (UsersWriters a) (ownerp perms))
         (ChangeGroupW (AllGrp s) (groupp perms)
            (ChangeGroupW (group a) (groupp perms) (GroupWriters a)))
         (UsersOwners a) (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 (owner a) (group a) (ChangeUserR Sub (UsersReaders a) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group a) (groupp perms) (GroupReaders a))) (ChangeUserW Sub (UsersWriters a) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group a) (groupp perms) (GroupWriters a))) (UsersOwners a) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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 (owner a) (group a) (ChangeUserR Sub (UsersReaders a) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group a) (groupp perms) (GroupReaders a))) (ChangeUserW Sub (UsersWriters a) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group a) (groupp perms) (GroupWriters a))) (UsersOwners a) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma ChmodPSP :
 forall (s t : SFSstate) (u : SUBJECT),
 StarProperty s -> TransFunc u s Chmod t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : StarProperty s) (_ : TransFunc u s Chmod 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H; auto. 
Qed. 
 
 
Lemma ChmodPCP : forall s t : SFSstate, PreservesControlProp s Chmod 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H6. 
(* Goal: ExecuterIsOwner s Sub o0 *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H8. 
(* 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H10 in H9; inversion H9; 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (chmod_acl s Sub o perms) 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro H10; rewrite H10 in H8; rewrite H7 in H8; injection H8; auto. 
 
symmetry  in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (chmod_acl s Sub o perms) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold chmod_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 => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y1) (groupp perms) (GroupReaders y1))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y1) (groupp perms) (GroupWriters y1))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y0) (group y0) (ChangeUserR Sub (UsersReaders y0) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y0) (ownerp perms)) gaw (UsersOwners y0) (GroupOwners y0)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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 (owner a) (group a) (ChangeUserR Sub (UsersReaders a) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group a) (groupp perms) (GroupReaders a))) (ChangeUserW Sub (UsersWriters a) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group a) (groupp perms) (GroupWriters a))) (UsersOwners a) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H8. 
(* 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H10 in H9; inversion H9; 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (chmod_acl s Sub o perms) 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro H10; rewrite H10 in H8; rewrite H7 in H8; injection H8; auto. 
 
symmetry  in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o0) (facl (chmod_acl s Sub o perms) o0) *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold chmod_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 => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group y1) (groupp perms) (GroupReaders y1))) | None => @None (set GRPNAME) end with | Some gar => match match facl (acl s) o with | Some y1 => @Some (set GRPNAME) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group y1) (groupp perms) (GroupWriters y1))) | None => @None (set GRPNAME) end with | Some gaw => @Some AccessCtrlListData (acldata (owner y0) (group y0) (ChangeUserR Sub (UsersReaders y0) (ownerp perms)) gar (ChangeUserW Sub (UsersWriters y0) (ownerp perms)) gaw (UsersOwners y0) (GroupOwners y0)) | None => @None AccessCtrlListData end | None => @None AccessCtrlListData end | 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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 (owner a) (group a) (ChangeUserR Sub (UsersReaders a) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (group a) (groupp perms) (GroupReaders a))) (ChangeUserW Sub (UsersWriters a) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (group a) (groupp perms) (GroupWriters a))) (UsersOwners a) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (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)
        (chmod_acl s Sub o perms) (secmat s) (files s) 
(* 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
        (directories s)) o0); auto. 
 
intros;
 absurd
  (MACSubCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s)
        (chmod_acl s Sub o perms) (secmat s) (files s) 
(* 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) (chmod_acl s Sub o perms) (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) (chmod_acl s Sub o perms) (secmat s) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
        (directories s)) u0); auto. 
 
Qed. 
 
 
End chmodIsSecure. 
 
Hint Resolve ChmodPSS ChmodPSP ChmodPCP.