Require Import ModelProperties. 
Require Import AuxiliaryLemmas. 
 
Section owner_closeIsSecure. 
 
Lemma Owner_ClosePSS :
 forall (s t : SFSstate) (u : SUBJECT),
 FuncPre5 s -> SecureState s -> TransFunc u s Owner_Close t -> SecureState t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : FuncPre5 s) (_ : SecureState s) (_ : TransFunc u s Owner_Close t), SecureState t *)
intros s t Sub FP5 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) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
unfold SecureState in |- *. 
(* Goal: and (DACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s))) (MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s))) *)
BreakSS. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: DACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
unfold DACSecureState in |- *; intros; simpl in |- *. 
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
elim (OBJeq_dec o o0); intro y0. 
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
rewrite <- y0. 
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o) | None => True end *)
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
cut (fsecmat (secmat s) o = None -> fsecmat (ownerclose_sm s u o) o = None). 
cut
 match fsecmat (ownerclose_sm s u o) o, fsecmat (secmat s) o with
 | _, None => False
 | None, Some z => True
 | Some y, Some z =>
     (set_In u0 (ActReaders y) -> set_In u0 (ActReaders z)) /\
     (set_In u0 (ActWriters y) -> set_In u0 (ActWriters z))
 end. 
cut
 match fsecmat (secmat s) o with
 | None => True
 | Some y =>
     (set_In u0 (ActReaders y) -> PreDACRead s u0 o) /\
     (set_In u0 (ActWriters y) -> PreDACWrite s u0 o)
 end. 
unfold PreDACRead, PreDACWrite in |- *; simpl in |- *;
 elim (fsecmat (secmat s) o); elim (fsecmat (ownerclose_sm s u o) o); 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 intros; contradiction || auto. 
(* Goal: le_sc a2 a1 *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o1) (fsecmat (ownerclose_sm s u o) o1) *)
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
tauto. 
 
(* Goal: match fsecmat (secmat s) o with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead s u0 o) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite s u0 o) | None => True end *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat (ownerclose_sm s u o) o) (@None ReadersWriters) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
unfold DACSecureState in DAC; apply DAC. 
 
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
apply OwnerClose_smCorr2; auto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), PreDACRead (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o0) (forall _ : @set_In SUBJECT u0 (ActWriters y), PreDACWrite (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0 o0) | None => True end *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
unfold PreDACRead, PreDACWrite in |- *; simpl in |- *. 
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fsecmat (ownerclose_sm s u o) o0) with (fsecmat (secmat s) o0). 
(* Goal: match fsecmat (secmat s) o0 with | Some y => and (forall _ : @set_In SUBJECT u0 (ActReaders y), match facl (acl s) o0 with | Some y0 => or (@set_In SUBJECT u0 (UsersReaders y0)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupReaders y0)))) | None => False end) (forall _ : @set_In SUBJECT u0 (ActWriters y), match facl (acl s) o0 with | Some y0 => or (@set_In SUBJECT u0 (UsersWriters y0)) (@ex GRPNAME (fun g : GRPNAME => and (@set_In SUBJECT u0 (groups s g)) (@set_In GRPNAME g (GroupWriters y0)))) | None => False end) | None => True end *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o0) (fsecmat (ownerclose_sm s u o) o0) *)
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
unfold DACSecureState, PreDACRead, PreDACWrite in DAC; apply DAC. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: MACSecureState (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
unfold MACSecureState in |- *; intros; simpl in |- *. 
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
elim (OBJeq_dec o o0); intro y0. 
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
rewrite <- y0. 
cut
 match fsecmat (ownerclose_sm s u o) o, fsecmat (secmat s) o with
 | _, None => False
 | None, Some z => True
 | Some y, Some z =>
     (set_In u0 (ActReaders y) -> set_In u0 (ActReaders z)) /\
     (set_In u0 (ActWriters y) -> set_In u0 (ActWriters z))
 end. 
cut
 match fsecmat (secmat s) o, fOSC (objectSC s) o, fSSC (subjectSC s) u0 with
 | None, _, _ => True
 | _, None, _ => True
 | _, _, None => True
 | Some x, Some y, Some z =>
     set_In u0 (ActReaders x) \/ set_In u0 (ActWriters x) -> le_sc y z
 end. 
elim (fsecmat (secmat s) o); elim (fsecmat (ownerclose_sm s u o) o);
 elim (fOSC (objectSC s) o); elim (fSSC (subjectSC s) u0);
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 contradiction || auto. 
(* Goal: le_sc a2 a1 *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o1) (fsecmat (ownerclose_sm s u o) o1) *)
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
tauto. 
 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o0) (fsecmat (ownerclose_sm s u o) o0) *)
unfold MACSecureState in MAC; apply MAC. 
 
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
apply OwnerClose_smCorr2; auto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: match fsecmat (ownerclose_sm s u o) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
replace (fsecmat (ownerclose_sm s u o) o0) with (fsecmat (secmat s) o0). 
(* Goal: match fsecmat (secmat s) o0 with | Some x => match fOSC (objectSC s) o0 with | Some y => match fSSC (subjectSC s) u0 with | Some z => forall _ : or (@set_In SUBJECT u0 (ActReaders x)) (@set_In SUBJECT u0 (ActWriters x)), le_sc y z | None => True end | None => True end | None => True end *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o0) (fsecmat (ownerclose_sm s u o) o0) *)
unfold MACSecureState in MAC; apply MAC. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
Qed. 
 
 
Lemma Owner_ClosePSP :
 forall (s t : SFSstate) (u : SUBJECT),
 FuncPre5 s ->
 StarProperty s -> TransFunc u s Owner_Close t -> StarProperty t. 
(* Goal: forall (s t : SFSstate) (u : SUBJECT) (_ : FuncPre5 s) (_ : StarProperty s) (_ : TransFunc u s Owner_Close t), StarProperty t *)
intros s t Sub FP5 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) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) *)
unfold StarProperty in |- *; simpl in |- *; intros. 
cut
 match
   fsecmat (secmat s) o1, fsecmat (secmat s) o2, fOSC (objectSC s) o2,
   fOSC (objectSC s) o1
 with
 | None, _, _, _ => True
 | _, None, _, _ => True
 | _, _, None, _ => True
 | _, _, _, None => True
 | Some w, Some x, Some y, Some z =>
     set_In u0 (ActWriters w) -> set_In u0 (ActReaders x) -> le_sc y z
 end. 
cut
 match fsecmat (ownerclose_sm s u o) o, fsecmat (secmat s) o with
 | _, None => False
 | None, Some z => True
 | Some y, Some z =>
     (set_In u0 (ActReaders y) -> set_In u0 (ActReaders z)) /\
     (set_In u0 (ActWriters y) -> set_In u0 (ActWriters z))
 end. 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
elim (OBJeq_dec o o1); elim (OBJeq_dec o o2); intros EQ2 EQ1. 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
rewrite <- EQ1; rewrite <- EQ2. 
elim (fsecmat (secmat s) o); elim (fOSC (objectSC s) o);
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 elim (fsecmat (ownerclose_sm s u o) o); intros; auto. 
 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
replace (fsecmat (ownerclose_sm s u o) o2) with (fsecmat (secmat s) o2). 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) 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 ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
rewrite <- EQ1. 
elim (fsecmat (secmat s) o2); elim (fOSC (objectSC s) o);
 elim (fOSC (objectSC s) o2); elim (fsecmat (secmat s) o);
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 elim (fsecmat (ownerclose_sm s u o) o); intros; contradiction || auto. 
(* Goal: le_sc a2 a1 *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o1) (fsecmat (ownerclose_sm s u o) o1) *)
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
tauto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) 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 ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
replace (fsecmat (ownerclose_sm s u o) o1) with (fsecmat (secmat s) o1). 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (secmat s) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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 ReadersWriters) (fsecmat (secmat s) o1) (fsecmat (ownerclose_sm s u o) o1) *)
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
rewrite <- EQ2. 
elim (fsecmat (secmat s) o1); elim (fOSC (objectSC s) o);
 elim (fOSC (objectSC s) o1); elim (fsecmat (secmat s) o);
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 elim (fsecmat (ownerclose_sm s u o) o); intros; contradiction || auto. 
(* Goal: le_sc a2 a1 *)
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o1) (fsecmat (ownerclose_sm s u o) o1) *)
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
tauto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) o1 with | Some w => match fsecmat (ownerclose_sm s u o) 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: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
replace (fsecmat (ownerclose_sm s u o) o2) with (fsecmat (secmat s) o2). 
(* Goal: forall (_ : match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end) (_ : 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), match fsecmat (ownerclose_sm s u o) 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 ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
replace (fsecmat (ownerclose_sm s u o) o1) with (fsecmat (secmat s) o1). 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
auto. 
 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
apply Close_smCorr2; auto. 
 
(* 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 *)
unfold StarProperty in SP; apply SP. 
 
Qed. 
 
 
Lemma Owner_ClosePCP :
 forall s t : SFSstate, PreservesControlProp s Owner_Close t. 
intros; unfold PreservesControlProp in |- *; intros Sub TF; inversion TF;
 unfold ControlProperty in |- *. 
(* Goal: and (forall o : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s t o, ExecuterIsOwner s Sub o) (forall _ : MACObjCtrlAttrHaveChanged s t o, @set_In SUBJECT Sub (groups s (SecAdmGrp s)))) (forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s t u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
inversion H. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
(* Goal: forall o0 : OBJECT, and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
intros. 
(* Goal: and (forall _ : DACCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, ExecuterIsOwner s Sub o0) (forall _ : MACObjCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0, @set_In SUBJECT Sub (groups s (SecAdmGrp s))) *)
(* Goal: forall (u0 : SUBJECT) (_ : MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0), @set_In SUBJECT Sub (groups s (SecAdmGrp s)) *)
split. 
intros;
 absurd
  (DACCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) 
        (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0); 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 auto. 
 
intros;
 absurd
  (MACObjCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) 
        (acl s) (ownerclose_sm s u o) (files s) (directories s)) o0); 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 auto. 
 
intros;
 absurd
  (MACSubCtrlAttrHaveChanged s
     (mkSFS (groups s) (primaryGrp s) (subjectSC s) 
        (AllGrp s) (RootGrp s) (SecAdmGrp s) (objectSC s) 
        (acl s) (ownerclose_sm s u o) (files s) (directories s)) u0); 
(* Goal: @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (ownerclose_sm s u o) o2) *)
(* Goal: match fsecmat (ownerclose_sm s u o) o with | Some y => match fsecmat (secmat s) o with | Some z => and (forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z)) (forall _ : @set_In SUBJECT u0 (ActWriters y), @set_In SUBJECT u0 (ActWriters z)) | None => False end | None => match fsecmat (secmat s) o with | Some z => True | None => False end end *)
(* 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 *)
 auto. 
 
Qed. 
 
 
End owner_closeIsSecure. 
 
Hint Resolve Owner_ClosePSS Owner_ClosePSP Owner_ClosePCP. 
 