Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section createIsSecure. 
 
Lemma CreatePSS :
 forall (s t : SFSstate) (u : SUBJECT),
 FuncPre1 s ->
 FuncPre2 s ->
 FuncPre3 s -> SecureState s -> TransFunc u s Create t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : FuncPre1 s) (_ : FuncPre2 s) (_ : FuncPre3 s) (_ : SecureState s) (_ : TransFunc u s Create t), SecureState t *)
intros s t Sub FP1 FP2 FP3 SS TF; inversion TF. 
(* 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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
BreakSS. 
(* Goal: SecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold SecureState in |- *. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) 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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold DACSecureState in |- *; simpl in |- *. 
(* Goal: forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
cut
 (match fsecmat (secmat s) o with
  | Some y => set_In u0 (ActReaders y) -> PreDACRead s u0 o
  | None => True
  end /\
  match fsecmat (secmat s) o with
  | Some y => set_In u0 (ActWriters y) -> PreDACWrite s u0 o
  | None => True
  end). 
(* Goal: forall _ : and match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end, 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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0 o) | None => True end *)
(* Goal: and match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
elim (fsecmat (secmat s) o). 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), PreDACRead s u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters a), PreDACWrite s u0 o)), and (forall _ : @set_In SUBJECT u0 (ActReaders a), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters a), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0 o) *)
(* Goal: forall _ : and True True, True *)
(* Goal: and match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold PreDACRead, PreDACWrite, create_acl in |- *; simpl in |- *. 
(* Goal: forall (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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 match fSSC (subjectSC s) Sub with | Some y => match fsecmat (secmat s) (MyDir p) with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s) | None => acl s end | None => acl s end o 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 match fSSC (subjectSC s) Sub with | Some y => match fsecmat (secmat s) (MyDir p) with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s) | None => acl s end | None => acl s end o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
elim (fsecmat (secmat s) (MyDir p)); elim (fSSC (subjectSC s) Sub). 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJNAMEeq_dec p (ObjName o)). 
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
intro y. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
rewrite y. 
(* Goal: forall (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE (ObjName o)) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE (ObjName o)) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
replace (facl (acl s) o) with (None (A:=AccessCtrlListData)). 
(* Goal: forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
(* Goal: forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim H8; intros. 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE (ObjName o)) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE (ObjName o)) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (option AccessCtrlListData) (@None AccessCtrlListData) (facl (acl s) o) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
split; intro. 
(* Goal: forall _ : False, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: False *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: forall _ : False, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: False *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
symmetry  in |- *. 
(* Goal: @eq (option AccessCtrlListData) (facl (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold facl in |- *. 
(* Goal: @eq (option AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
rewrite y in H4. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
rewrite y in H2. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
apply UniqNames; assumption.

(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
intro y. 
replace
 (facl
    (set_add ACLeq_dec
       (NEWFILE p,
       acldata Sub (primaryGrp s Sub)
         (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms))
         (ChangeGroupR (AllGrp s) (groupp perms)
            (ChangeGroupR (primaryGrp s Sub) (groupp perms)
               (empty_set GRPNAME)))
         (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms))
         (ChangeGroupW (AllGrp s) (groupp perms)
            (ChangeGroupW (primaryGrp s Sub) (groupp perms)
               (empty_set GRPNAME))) (Sub :: nil) (RootGrp s :: nil)) 
       (acl s)) o) with (facl (acl s) o). 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o) *)
(* Goal: forall (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold facl in |- *; apply AddEq. 
(* Goal: not (@eq OBJECT o (NEWFILE p)) *)
(* Goal: forall (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold NEWFILE in |- *. 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: False *)
(* Goal: forall (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
apply y. 
(* Goal: @eq OBJNAME p (ObjName o) *)
(* Goal: forall (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
rewrite H8. 
(* Goal: @eq OBJNAME p (ObjName (@pair OBJNAME OBJTYPE p File)) *)
(* Goal: forall (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
simpl in |- *. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : False, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: False *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: and match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold DACSecureState in DAC. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
apply ReadWriteImpRead; auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
apply ReadWriteImpWrite; auto. 
 
(* Goal: forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
unfold MACSecureState in |- *; simpl in |- *; intros. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJNAMEeq_dec p (ObjName o)). 
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
intro y. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
rewrite y. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub (ObjName o)) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o) with (None (A:=ReadersWriters)). 
(* Goal: True *)
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) o) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fOSC (objectSC s) o) with (None (A:=SecClass)). 
elim (fSSC (subjectSC s) u0); elim (fOSC (create_oSC s Sub (ObjName o)) o);
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
 contradiction || auto. 
 
symmetry  in |- *. 
(* Goal: @eq (option AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold fOSC in |- *; apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
replace (DOM OBJeq_dec (objectSC s)) with (DOM OBJeq_dec (acl s)). 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
rewrite y in H4; rewrite y in H2; apply UniqNames; assumption. 
 
(* Goal: @eq (option AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
symmetry  in |- *; unfold fsecmat in |- *; apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
cut (~ set_In o (DOM OBJeq_dec (acl s))). 
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))), not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
unfold not in |- *. 
(* Goal: forall (_ : forall _ : @set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)), False) (_ : @set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), False *)
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
intros SI1 SI2; apply SI1. 
(* Goal: @set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) *)
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
unfold FuncPre3 in FP3. 
(* Goal: @set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) *)
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
unfold Included in FP3. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
rewrite y in H4; rewrite y in H2; apply UniqNames; assumption. 
 
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
intro y. 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (create_oSC s Sub p) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fOSC (create_oSC s Sub p) o) with (fOSC (objectSC s) o). 
(* Goal: match fsecmat (secmat s) o with | Some x => match fOSC (objectSC s) o with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
unfold MACSecureState in MAC; apply MAC. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
 
Lemma CreatePSP :
 forall (s t : SFSstate) (u : SUBJECT),
 FuncPre1 s ->
 FuncPre2 s ->
 FuncPre3 s -> StarProperty s -> TransFunc u s Create t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : FuncPre1 s) (_ : FuncPre2 s) (_ : FuncPre3 s) (_ : StarProperty s) (_ : TransFunc u s Create t), StarProperty t *)
intros s t Sub FP1 FP2 FP3 SP TF; inversion TF. 
(* 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: StarProperty (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold StarProperty in |- *; simpl in |- *; intros u0 o1 o2. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
elim (OBJNAMEeq_dec p (ObjName o1)); elim (OBJNAMEeq_dec p (ObjName o2)). 
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o2))) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
intros y y0. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: forall (_ : @eq OBJNAME p (ObjName o2)) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o2))) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o1) with (None (A:=ReadersWriters)). 
elim (fsecmat (secmat s) o2); elim (fsecmat (secmat s) o1);
 elim (fOSC (create_oSC s Sub p) o2); elim (fOSC (create_oSC s Sub p) o1);
 trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
eauto. 
 
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o2))) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
intros y y0. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: forall (_ : @eq OBJNAME p (ObjName o2)) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o2))) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o1) with (None (A:=ReadersWriters)). 
elim (fsecmat (secmat s) o2); elim (fOSC (create_oSC s Sub p) o2);
 elim (fOSC (create_oSC s Sub p) o1); trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
eauto. 
 
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o2))) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
intros y y0. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o2))) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fsecmat (secmat s) o2) with (None (A:=ReadersWriters)). 
elim (fsecmat (secmat s) o1); elim (fOSC (create_oSC s Sub p) o2);
 elim (fOSC (create_oSC s Sub p) o1); trivial. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
eauto. 
 
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o2))) (_ : not (@eq OBJNAME p (ObjName o1))), match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
intros y y0. 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (create_oSC s Sub p) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
replace (fOSC (create_oSC s Sub p) o1) with (fOSC (objectSC s) o1). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (create_oSC s Sub p) o2 with | Some y => match fOSC (objectSC s) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o1) (fOSC (create_oSC s Sub p) o1) *)
replace (fOSC (create_oSC s Sub p) o2) with (fOSC (objectSC s) o2). 
(* Goal: match fsecmat (secmat s) o1 with | Some w => match fsecmat (secmat s) o2 with | Some x => match fOSC (objectSC s) o2 with | Some y => match fOSC (objectSC s) o1 with | Some z => forall (_ : @set_In SUBJECT u0 (ActWriters w)) (_ : @set_In SUBJECT u0 (ActReaders x)), le_sc y z | None => True end | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (create_oSC s Sub p) o2) *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o1) (fOSC (create_oSC s Sub p) o1) *)
unfold StarProperty in SP; apply SP. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
Qed. 
 
 
Lemma CreatePCP :
 forall s t : SFSstate,
 FuncPre1 s -> FuncPre2 s -> PreservesControlProp s Create t. 
intros s t FP1 FP2; 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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) 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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H8. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H10. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJNAMEeq_dec p (ObjName o)). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (acl s) o = None). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H12 in H9. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
discriminate H9. 
 
(* Goal: @eq (option AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold facl in |- *; apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
rewrite a in H4; rewrite a in H2; apply UniqNames; assumption. 
 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: forall _ : False, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: False *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H12 in H11; inversion H11; auto. 
 
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (acl s) o = facl (create_acl s Sub p perms) o). 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro EQ; rewrite <- EQ in H10; rewrite H10 in H9; injection H9; auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H10. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJNAMEeq_dec p (ObjName o)). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (acl s) o = None). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H12 in H9. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
discriminate H9. 
 
(* Goal: @eq (option AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold facl in |- *; apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
rewrite a in H4; rewrite a in H2; apply UniqNames; assumption. 
 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (y = z). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: forall _ : False, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: False *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H12 in H11; inversion H11; auto. 
 
(* Goal: @eq AccessCtrlListData y z *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (facl (acl s) o = facl (create_acl s Sub p perms) o). 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro EQ; rewrite <- EQ in H10; rewrite H10 in H9; injection H9; auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
inversion H8. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
simpl in H10. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
elim (OBJNAMEeq_dec p (ObjName o)). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (fOSC (objectSC s) o = None). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: ExecuterIsOwner s Sub o *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), ExecuterIsOwner s Sub o *)
(* Goal: forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) o, @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H12 in H9; discriminate H9. 
 
(* Goal: @eq (option AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@None AccessCtrlListData) *)
(* Goal: forall (_ : not (@eq OBJNAME p (ObjName o))) (_ : SecClass) (_ : ReadersWriters) (a1 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a1), match facl (acl s) o 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 a1), match facl (acl s) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 a1), match facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWFILE p) (acldata Sub (primaryGrp s Sub) (ChangeUserR Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (ChangeUserW Sub (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s Sub) (groupp perms) (empty_set GRPNAME))) (@cons SUBJECT Sub (@nil SUBJECT)) (@cons GRPNAME (RootGrp s) (@nil GRPNAME)))) (acl s)) o 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 (_ : ReadersWriters) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (_ : SecClass) (a0 : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 a0), match facl (acl s) o 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 (a : ReadersWriters) (_ : and (forall _ : @set_In SUBJECT u0 (ActReaders a), match facl (acl s) o 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) o 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) o 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) o 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) o with | Some y => forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o | None => True end match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) *)
unfold fOSC in |- *; apply NotInDOMIsUndef. 
 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) *)
(* Goal: forall _ : not (@eq OBJNAME p (ObjName o)), @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) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
replace (DOM OBJeq_dec (objectSC s)) with (DOM OBJeq_dec (acl s)). 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite a in H4; rewrite a in H2; eauto.
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
auto. 
 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (x = y). 
(* Goal: forall _ : @eq SecClass x y, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro. 
(* Goal: @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut False. 
(* Goal: forall _ : False, @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
(* Goal: False *)
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
tauto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
rewrite H12 in H11; inversion H11; auto. 
 
(* Goal: @eq SecClass x y *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
cut (fOSC (objectSC s) o = fOSC (create_oSC s Sub p) o). 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intro EQ; rewrite <- EQ in H10; rewrite H10 in H9; injection H9; auto. 
 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) 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) (create_oSC s Sub p)
        (create_acl s Sub p perms) (secmat s) (create_files Sub p)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s Sub p) o) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (create_oSC s Sub p) (create_acl s Sub p perms) (secmat s) (create_files Sub p) (create_directories Sub p)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
        (create_directories Sub p)) u0); auto. 
 
Qed. 
 
 
End createIsSecure. 
 
Hint Resolve CreatePSS CreatePSP CreatePCP. 
 