Require Import ModelProperties.

 (*SUBJECT, Property and TransFunc*)
Ltac OpDontChangeStPSS :=
  intros s t Sub SS TF; inversion TF;
   match goal with
   | id:(s = t) |- _ => rewrite <- id; auto
   end.
 
Ltac OpDontChangeStPSP :=
  intros s t Sub SP TF;  (* SUBJECT, Property and TransFunc *)
   inversion TF; match goal with
                 | id:(s = t) |- _ => rewrite <- id; auto
                 end. 

Ltac StartPSS := intros s t Sub SS TF; inversion TF. 

Ltac BreakSS :=
  match goal with
  | SS:(SecureState _) |- _ =>
      unfold SecureState in SS; elim SS; intros DAC MAC
  end. 

Ltac StartPSP := intros s t Sub SP TF; inversion TF. 
  
 
Lemma ReadWriteImpRead :
 forall s : SFSstate,
 DACSecureState s ->
 forall (u : SUBJECT) (o : OBJECT),
 match fsecmat (secmat s) o with
 | Some y => set_In u (ActReaders y) -> PreDACRead s u o
 | None => True
 end. 
(* Goal: forall (s : SFSstate) (_ : DACSecureState s) (u : SUBJECT) (o : OBJECT), match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u (ActWriters y), PreDACWrite s u o | None => True end *)
unfold DACSecureState in |- *. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
cut
 match fsecmat (secmat s) o with
 | Some y =>
     (set_In u (ActReaders y) -> PreDACRead s u o) /\
     (set_In u (ActWriters y) -> PreDACWrite s u o)
 | None => True
 end. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim H0; intros. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fsecmat (secmat s) o with | Some y => and (forall _ : @set_In SUBJECT u (ActReaders y), PreDACRead s u o) (forall _ : @set_In SUBJECT u (ActWriters y), PreDACWrite s u o) | None => True end *)
apply H. 
 
Qed. 
 
 
Lemma ReadWriteImpWrite :
 forall s : SFSstate,
 DACSecureState s ->
 forall (u : SUBJECT) (o : OBJECT),
 match fsecmat (secmat s) o with
 | Some y => set_In u (ActWriters y) -> PreDACWrite s u o
 | None => True
 end. 
(* Goal: forall (s : SFSstate) (_ : DACSecureState s) (u : SUBJECT) (o : OBJECT), match fsecmat (secmat s) o with | Some y => forall _ : @set_In SUBJECT u (ActWriters y), PreDACWrite s u o | None => True end *)
unfold DACSecureState in |- *. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
cut
 match fsecmat (secmat s) o with
 | Some y =>
     (set_In u (ActReaders y) -> PreDACRead s u o) /\
     (set_In u (ActWriters y) -> PreDACWrite s u o)
 | None => True
 end. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim H0; intros. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fsecmat (secmat s) o with | Some y => and (forall _ : @set_In SUBJECT u (ActReaders y), PreDACRead s u o) (forall _ : @set_In SUBJECT u (ActWriters y), PreDACWrite s u o) | None => True end *)
apply H. 
 
Qed. 
 
 
Lemma TwoImpLeft :
 forall (s : SFSstate) (u : SUBJECT),
 (forall rw : ReadersWriters,
  set_In rw (ransecmat (secmat s)) ->
  ~ set_In u (ActReaders rw) /\ ~ set_In u (ActWriters rw)) ->
 forall rw : ReadersWriters,
 set_In rw (ransecmat (secmat s)) -> ~ set_In u (ActReaders rw). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: not (@set_In SUBJECT u (ActWriters rw)) *)
cut (~ set_In u (ActReaders rw) /\ ~ set_In u (ActWriters rw)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
tauto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma TwoImpRight :
 forall (s : SFSstate) (u : SUBJECT),
 (forall rw : ReadersWriters,
  set_In rw (ransecmat (secmat s)) ->
  ~ set_In u (ActReaders rw) /\ ~ set_In u (ActWriters rw)) ->
 forall rw : ReadersWriters,
 set_In rw (ransecmat (secmat s)) -> ~ set_In u (ActWriters rw). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: not (@set_In SUBJECT u (ActWriters rw)) *)
cut (~ set_In u (ActReaders rw) /\ ~ set_In u (ActWriters rw)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
tauto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma UniqNames :
 forall (s : SFSstate) (o : OBJECT),
 FuncPre1 s ->
 ~ set_In (ObjName o, File) (domf (files s)) ->
 ~ set_In (ObjName o, Directory) (domd (directories s)) ->
 ~ set_In o (DOM OBJeq_dec (acl s)). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intro; intro; unfold FuncPre1 in |- *; elim o; simpl in |- *; intros. 
cut
 ((forall o : OBJECT,
   set_In o (DOM OBJeq_dec (directories s)) -> ObjType o = Directory) /\
  (forall o : OBJECT, set_In o (DOM OBJeq_dec (files s)) -> ObjType o = File) /\
  DOM OBJeq_dec (acl s) =
  set_union OBJeq_dec (DOM OBJeq_dec (files s))
    (DOM OBJeq_dec (directories s))). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intro CUT; elim CUT; intros. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim H3; intros. 
(* Goal: not (@set_In OBJECT (@pair OBJNAME OBJTYPE a b) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
rewrite H5; intro. 
cut
 (set_In (a, File) (domf (files s)) \/
  set_In (a, Directory) (domd (directories s))). 
(* Goal: forall _ : or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))), False *)
(* Goal: or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
intro H7; elim H7; intro. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
generalize H6; elim b; intro. 
(* Goal: or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))) *)
(* Goal: or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
left; cut (~ set_In (a, File) (DOM OBJeq_dec (directories s))). 
(* Goal: forall _ : not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s)) *)
(* Goal: not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))) *)
(* Goal: or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
intro; unfold domf in |- *. 
cut
 (set_In (a, File)
    (set_union OBJeq_dec (DOM OBJeq_dec (directories s))
       (DOM OBJeq_dec (files s)))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro; eauto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))) *)
(* Goal: or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
intro; absurd (ObjType (a, File) = Directory). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
simpl in |- *. 
(* Goal: not (@eq OBJTYPE Directory File) *)
(* Goal: @eq OBJTYPE (ObjType (@pair OBJNAME OBJTYPE a Directory)) File *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
intro H11; discriminate H11. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
(* Goal: or (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a File) (domf (files s))) (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
right. 
(* Goal: @set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (domd (directories s)) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
cut (~ set_In (a, Directory) (DOM OBJeq_dec (files s))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro; unfold domd in |- *; eauto. 
 
(* Goal: not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE a Directory) (@DOM OBJECT FILECONT OBJeq_dec (files s))) *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
intro; absurd (ObjType (a, Directory) = File). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
simpl in |- *. 
(* Goal: not (@eq OBJTYPE Directory File) *)
(* Goal: @eq OBJTYPE (ObjType (@pair OBJNAME OBJTYPE a Directory)) File *)
(* Goal: and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT DIRCONT OBJeq_dec (directories s))), @eq OBJTYPE (ObjType o) Directory) (and (forall (o : OBJECT) (_ : @set_In OBJECT o (@DOM OBJECT FILECONT OBJeq_dec (files s))), @eq OBJTYPE (ObjType o) File) (@eq (set OBJECT) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)) (@set_union OBJECT OBJeq_dec (@DOM OBJECT FILECONT OBJeq_dec (files s)) (@DOM OBJECT DIRCONT OBJeq_dec (directories s))))) *)
intro H11; discriminate H11. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Hint Resolve UniqNames. 
 
 
Lemma eq_scIMPLYle_sc : forall a b : SecClass, eq_sc a b -> le_sc a b. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
unfold eq_sc, le_sc in |- *; intros. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim H; intros. 
(* Goal: and (@eq SECLEV (level b) (level a)) (@eq (set CATEGORY) (categs b) (categs a)) *)
rewrite H0; rewrite H1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
Qed. 
 
 
Lemma NotInDOMIsUndef2 :
 forall (s : SFSstate) (o1 o2 : OBJECT),
 ~ set_In o1 (domsecmat (secmat s)) ->
 o1 = o2 -> None = fsecmat (secmat s) o2. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
symmetry  in |- *. 
(* Goal: @eq (option ReadersWriters) (fsecmat (secmat s) o2) (@None ReadersWriters) *)
rewrite H0 in H. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply NotInDOMIsUndef; auto. 
 
Qed. 
 
Lemma NotInDOMIsUndef3 :
 forall (s : SFSstate) (p : OBJNAME) (o : OBJECT),
 FuncPre1 s ->
 FuncPre3 s ->
 ~ set_In (p, File) (domf (files s)) ->
 ~ set_In (p, Directory) (domd (directories s)) ->
 p = ObjName o -> None = fsecmat (secmat s) o. 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
intros until o; elim o; simpl in |- *. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros until b; elim b; intros. 
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) (@pair OBJNAME OBJTYPE a Directory)) *)
rewrite <- H3. 
symmetry  in |- *; unfold fsecmat in |- *; apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT (@pair OBJNAME OBJTYPE p File) (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) (@pair OBJNAME OBJTYPE a Directory)) *)
cut (~ set_In (p, File) (DOM OBJeq_dec (acl s))). 
(* Goal: forall _ : not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))), not (@set_In OBJECT (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
(* Goal: not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
unfold FuncPre3, Included in H3. 
(* Goal: forall _ : not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))), not (@set_In OBJECT (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
(* Goal: not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
unfold FuncPre3, Included in H0. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
apply UniqNames; auto. 
 
(* Goal: @eq (option ReadersWriters) (@None ReadersWriters) (fsecmat (secmat s) (@pair OBJNAME OBJTYPE a Directory)) *)
rewrite <- H3. 
symmetry  in |- *; unfold fsecmat in |- *; apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
cut (~ set_In (p, Directory) (DOM OBJeq_dec (acl s))). 
(* Goal: forall _ : not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))), not (@set_In OBJECT (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
(* Goal: not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
unfold FuncPre3, Included in H3. 
(* Goal: forall _ : not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))), not (@set_In OBJECT (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) *)
(* Goal: not (@set_In (prod OBJNAME OBJTYPE) (@pair OBJNAME OBJTYPE p Directory) (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) *)
unfold FuncPre3, Included in H0. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
apply UniqNames; auto. 
 
Qed. 
 
 
Lemma EqfOSC6 :
 forall (s : SFSstate) (o1 o2 : OBJECT) (sc : SecClass),
 o1 <> o2 -> fOSC (objectSC s) o2 = fOSC (chobjsc_SC s o1 sc) o2. 
(* Goal: forall (s : SFSstate) (o1 o2 : OBJECT) (sc : SecClass) (_ : not (@eq OBJECT o1 o2)), @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (chobjsc_SC s o1 sc) o2) *)
intros; unfold fOSC, chobjsc_SC in |- *. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC match fOSC (objectSC s) o1 with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o1 y) (objectSC s) | None => objectSC s end o2) *)
elim (fOSC (objectSC s) o1). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro; apply AddRemEq; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma EqfOSC5 :
 forall (s : SFSstate) (o : OBJECT) (p : OBJNAME),
 FuncPre1 s ->
 FuncPre2 s ->
 ~ set_In (p, File) (domf (files s)) ->
 ~ set_In (p, Directory) (domd (directories s)) ->
 p = ObjName o -> None = fOSC (objectSC s) o. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
symmetry  in |- *; unfold fOSC in |- *; apply NotInDOMIsUndef. 
(* Goal: not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC 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))) *)
rewrite H3 in H1; rewrite H3 in H2. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma EqfOSC1 :
 forall (s : SFSstate) (o : OBJECT) (p : OBJNAME) (u : SUBJECT),
 p <> ObjName o -> fOSC (objectSC s) o = fOSC (create_oSC s u p) o. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (create_oSC s u p) o) *)
unfold create_oSC in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl match fSSC (subjectSC s) u with | Some y => match fsecmat (secmat s) (MyDir p) with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWDIR p) (acldata u (primaryGrp s u) (ChangeUserR u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (ChangeUserW u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)) (ChangeGroupO (RootGrp s) (empty_set GRPNAME)))) (acl s) | None => acl s end | None => acl s end o) *)
elim (fSSC (subjectSC s) u); elim (fsecmat (secmat s) (MyDir p)). 
(* Goal: forall (_ : ReadersWriters) (a0 : SecClass), @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (@set_add (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass (NEWDIR p) a0) (objectSC s)) o) *)
(* Goal: forall _ : SecClass, @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (objectSC s) o) *)
(* Goal: forall _ : ReadersWriters, @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (objectSC s) o) *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (objectSC s) o) *)
intros; unfold fOSC in |- *; apply AddEq. 
(* Goal: match fsecmat (secmat s) o with | Some y => and (forall _ : @set_In SUBJECT u (ActReaders y), PreDACRead s u o) (forall _ : @set_In SUBJECT u (ActWriters y), PreDACWrite s u o) | None => True end *)
intro; apply H. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
rewrite H0; simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma EqfOSC2 :
 forall (s : SFSstate) (o : OBJECT) (p : OBJNAME) (u : SUBJECT),
 p <> ObjName o -> fOSC (objectSC s) o = fOSC (mkdir_oSC s u p) o. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (mkdir_oSC s u p) o) *)
unfold mkdir_oSC in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl match fSSC (subjectSC s) u with | Some y => match fsecmat (secmat s) (MyDir p) with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWDIR p) (acldata u (primaryGrp s u) (ChangeUserR u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (ChangeUserW u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)) (ChangeGroupO (RootGrp s) (empty_set GRPNAME)))) (acl s) | None => acl s end | None => acl s end o) *)
elim (fSSC (subjectSC s) u); elim (fsecmat (secmat s) (MyDir p)). 
(* Goal: forall (_ : ReadersWriters) (a0 : SecClass), @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (@set_add (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass (NEWDIR p) a0) (objectSC s)) o) *)
(* Goal: forall _ : SecClass, @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (objectSC s) o) *)
(* Goal: forall _ : ReadersWriters, @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (objectSC s) o) *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o) (fOSC (objectSC s) o) *)
intros; unfold fOSC in |- *; apply AddEq. 
(* Goal: match fsecmat (secmat s) o with | Some y => and (forall _ : @set_In SUBJECT u (ActReaders y), PreDACRead s u o) (forall _ : @set_In SUBJECT u (ActWriters y), PreDACWrite s u o) | None => True end *)
intro; apply H. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
rewrite H0; simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma EqfOSC3 :
 forall (s : SFSstate) (o1 o2 : OBJECT),
 o1 <> o2 -> fOSC (objectSC s) o2 = fOSC (unlink_oSC s o1) o2. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (unlink_oSC s o) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold unlink_oSC in |- *. 
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC match fOSC (objectSC s) o1 with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o1 y) (objectSC s) | None => objectSC s end o2) *)
elim (fOSC (objectSC s) o1). 
(* Goal: forall a : SecClass, @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o1 a) (objectSC s)) o2) *)
(* Goal: @eq (Exc SecClass) (fOSC (objectSC s) o2) (fOSC (objectSC s) o2) *)
intro; unfold fOSC in |- *; apply RemEq. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma Eqfacl1 :
 forall (s : SFSstate) (o : OBJECT) (p : OBJNAME) (u : SUBJECT)
   (perms : PERMS),
 p <> ObjName o -> facl (acl s) o = facl (create_acl s u p perms) o. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (create_acl s u p perms) o) *)
unfold create_acl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl match fSSC (subjectSC s) u with | Some y => match fsecmat (secmat s) (MyDir p) with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWDIR p) (acldata u (primaryGrp s u) (ChangeUserR u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (ChangeUserW u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)) (ChangeGroupO (RootGrp s) (empty_set GRPNAME)))) (acl s) | None => acl s end | None => acl s end o) *)
elim (fSSC (subjectSC s) u); elim (fsecmat (secmat s) (MyDir p)). 
(* Goal: forall (_ : ReadersWriters) (_ : SecClass), @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWDIR p) (acldata u (primaryGrp s u) (ChangeUserR u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (ChangeUserW u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)) (ChangeGroupO (RootGrp s) (empty_set GRPNAME)))) (acl s)) o) *)
(* Goal: forall _ : SecClass, @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (acl s) o) *)
(* Goal: forall _ : ReadersWriters, @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (acl s) o) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (acl s) o) *)
intros; unfold facl in |- *; apply AddEq. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro y1; apply H; rewrite y1; simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma Eqfacl2 :
 forall (s : SFSstate) (o : OBJECT) (p : OBJNAME) (u : SUBJECT)
   (perms : PERMS),
 p <> ObjName o -> facl (acl s) o = facl (mkdir_acl s u p perms) o. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (mkdir_acl s u p perms) o) *)
unfold mkdir_acl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl match fSSC (subjectSC s) u with | Some y => match fsecmat (secmat s) (MyDir p) with | Some z => @set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWDIR p) (acldata u (primaryGrp s u) (ChangeUserR u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (ChangeUserW u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)) (ChangeGroupO (RootGrp s) (empty_set GRPNAME)))) (acl s) | None => acl s end | None => acl s end o) *)
elim (fSSC (subjectSC s) u); elim (fsecmat (secmat s) (MyDir p)). 
(* Goal: forall (_ : ReadersWriters) (_ : SecClass), @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (@set_add (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData (NEWDIR p) (acldata u (primaryGrp s u) (ChangeUserR u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupR (AllGrp s) (groupp perms) (ChangeGroupR (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (ChangeUserW u (empty_set SUBJECT) (ownerp perms)) (ChangeGroupW (AllGrp s) (groupp perms) (ChangeGroupW (primaryGrp s u) (groupp perms) (empty_set GRPNAME))) (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)) (ChangeGroupO (RootGrp s) (empty_set GRPNAME)))) (acl s)) o) *)
(* Goal: forall _ : SecClass, @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (acl s) o) *)
(* Goal: forall _ : ReadersWriters, @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (acl s) o) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o) (facl (acl s) o) *)
intros; unfold facl in |- *; apply AddEq. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro y1; apply H; rewrite y1; simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma Eqfacl3 :
 forall (s : SFSstate) (o1 o2 : OBJECT),
 o1 <> o2 -> facl (acl s) o2 = facl (unlink_acl s o1) o2. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (unlink_acl s o) o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
unfold unlink_acl in |- *. 
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o2) (facl match facl (acl s) o1 with | Some y => @set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o1 y) (acl s) | None => acl s end o2) *)
elim (facl (acl s) o1). 
(* Goal: forall a : AccessCtrlListData, @eq (Exc AccessCtrlListData) (facl (acl s) o2) (facl (@set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o1 a) (acl s)) o2) *)
(* Goal: @eq (Exc AccessCtrlListData) (facl (acl s) o2) (facl (acl s) o2) *)
intros; unfold facl in |- *; apply RemEq. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 (*Seguir aqui*)
Lemma Eqfacl4 :
 forall (s : SFSstate) (o : OBJECT) (y z : AccessCtrlListData),
 FuncPre4 s ->
 facl (acl s) o = Some y -> facl (rmdir_acl s o) o = Some z -> False. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec match facl (acl s) o with | Some y => @set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s) | None => acl s end o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
unfold facl in |- *. 
(* Goal: forall (s : SFSstate) (o : OBJECT) (y z : SecClass) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (unlink_oSC s o) o) (@Some SecClass z)), False *)
intros until z. 
cut
 match PARTFUNC OBJeq_dec (acl s) o with
 | Some y => set_In (o, y) (acl s)
 | None => ~ set_In o (DOM OBJeq_dec (acl s))
 end. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (rmdir_acl s o) o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
unfold rmdir_acl in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec match facl (acl s) o with | Some y => @set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s) | None => acl s end o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
unfold facl in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s) | None => acl s end o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
elim (PARTFUNC OBJeq_dec (acl s) o). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)))) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@None AccessCtrlListData) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
cut (PARTFUNC OBJeq_dec (set_remove ACLeq_dec (o, a) (acl s)) o = None). 
(* Goal: forall _ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass), False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
rewrite H2. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intro. 
(* Goal: False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H3. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H1. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
apply DOMFuncRel4. 
Qed. 
 
 
Lemma Eqfacl5 :
 forall (s : SFSstate) (o : OBJECT) (y z : AccessCtrlListData),
 FuncPre4 s ->
 facl (acl s) o = Some y -> facl (unlink_acl s o) o = Some z -> False. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec match facl (acl s) o with | Some y => @set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s) | None => acl s end o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
unfold facl in |- *. 
(* Goal: forall (s : SFSstate) (o : OBJECT) (y z : SecClass) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (unlink_oSC s o) o) (@Some SecClass z)), False *)
intros until z. 
cut
 match PARTFUNC OBJeq_dec (acl s) o with
 | Some y => set_In (o, y) (acl s)
 | None => ~ set_In o (DOM OBJeq_dec (acl s))
 end. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (unlink_acl s o) o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
unfold unlink_acl in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec match facl (acl s) o with | Some y => @set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s) | None => acl s end o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
unfold facl in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_remove (prod OBJECT AccessCtrlListData) ACLeq_dec (@pair OBJECT AccessCtrlListData o y) (acl s) | None => acl s end o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
elim (PARTFUNC OBJeq_dec (acl s) o). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s)))) (_ : FuncPre4 s) (_ : @eq (Exc AccessCtrlListData) (@None AccessCtrlListData) (@Some AccessCtrlListData y)) (_ : @eq (Exc AccessCtrlListData) (@PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o) (@Some AccessCtrlListData z)), False *)
(* Goal: match @PARTFUNC OBJECT AccessCtrlListData OBJeq_dec (acl s) o with | Some y => @set_In (prod OBJECT AccessCtrlListData) (@pair OBJECT AccessCtrlListData o y) (acl s) | None => not (@set_In OBJECT o (@DOM OBJECT AccessCtrlListData OBJeq_dec (acl s))) end *)
cut (PARTFUNC OBJeq_dec (set_remove ACLeq_dec (o, a) (acl s)) o = None). 
(* Goal: forall _ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass), False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
rewrite H2. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intro. 
(* Goal: False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H3. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H1. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
apply DOMFuncRel4. 
Qed. 
 
 
Lemma EqfOSC4 :
 forall (s : SFSstate) (o : OBJECT) (y z : SecClass),
 FuncPre6 s ->
 fOSC (objectSC s) o = Some y -> fOSC (rmdir_oSC s o) o = Some z -> False. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec match fOSC (objectSC s) o with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o y) (objectSC s) | None => objectSC s end o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fOSC in |- *. 
(* Goal: forall (s : SFSstate) (o : OBJECT) (y z : SecClass) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (unlink_oSC s o) o) (@Some SecClass z)), False *)
intros until z. 
cut
 match PARTFUNC OBJeq_dec (objectSC s) o with
 | Some y => set_In (o, y) (objectSC s)
 | None => ~ set_In o (DOM OBJeq_dec (objectSC s))
 end. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (rmdir_oSC s o) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold rmdir_oSC in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec match fOSC (objectSC s) o with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o y) (objectSC s) | None => objectSC s end o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fOSC in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o y) (objectSC s) | None => objectSC s end o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
elim (PARTFUNC OBJeq_dec (objectSC s) o). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
cut (PARTFUNC OBJeq_dec (set_remove OSCeq_dec (o, a) (objectSC s)) o = None). 
(* Goal: forall _ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass), False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
rewrite H2. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intro. 
(* Goal: False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H3. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H1. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
apply DOMFuncRel4. 
Qed. 
 
 
Lemma EqfOSC7 :
 forall (s : SFSstate) (o : OBJECT) (y z : SecClass),
 FuncPre6 s ->
 fOSC (objectSC s) o = Some y -> fOSC (unlink_oSC s o) o = Some z -> False. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec match fOSC (objectSC s) o with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o y) (objectSC s) | None => objectSC s end o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fOSC in |- *. 
(* Goal: forall (s : SFSstate) (o : OBJECT) (y z : SecClass) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (unlink_oSC s o) o) (@Some SecClass z)), False *)
intros until z. 
cut
 match PARTFUNC OBJeq_dec (objectSC s) o with
 | Some y => set_In (o, y) (objectSC s)
 | None => ~ set_In o (DOM OBJeq_dec (objectSC s))
 end. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (unlink_oSC s o) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold unlink_oSC in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec match fOSC (objectSC s) o with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o y) (objectSC s) | None => objectSC s end o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fOSC in |- *. 
(* Goal: forall (_ : match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o y) (objectSC s) | None => objectSC s end o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
elim (PARTFUNC OBJeq_dec (objectSC s) o). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
cut (PARTFUNC OBJeq_dec (set_remove OSCeq_dec (o, a) (objectSC s)) o = None). 
(* Goal: forall _ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass), False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
rewrite H2. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intro. 
(* Goal: False *)
(* Goal: @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s)) o) (@None SecClass) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : FuncPre6 s) (_ : @eq (Exc SecClass) (@None SecClass) (@Some SecClass y)) (_ : @eq (Exc SecClass) (@PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o) (@Some SecClass z)), False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H3. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: False *)
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
discriminate H1. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
apply DOMFuncRel4. 
Qed. 
 
 
Lemma NoDACChange :
 forall (s : SFSstate) (o : OBJECT) (SSC : set (SUBJECT * SecClass))
   (OSC : set (OBJECT * SecClass)) (FILES : set (OBJECT * FILECONT))
   (DIRECTS : set (OBJECT * DIRCONT)) (SM : set (OBJECT * ReadersWriters)),
 ~
 DACCtrlAttrHaveChanged s
   (mkSFS (groups s) (primaryGrp s) SSC (AllGrp s) 
      (RootGrp s) (SecAdmGrp s) OSC (acl s) SM FILES DIRECTS) o. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intro. 
(* Goal: False *)
inversion H; simpl in H1; cut (y = z). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro EQ; rewrite EQ in H2; inversion H2; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
rewrite H0 in H1; injection H1; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro EQ; rewrite EQ in H2; inversion H2; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
rewrite H0 in H1; injection H1; auto. 
 
Qed. 
 
 
Lemma NoDACChange2 :
 forall (s : SFSstate) (o : OBJECT), ~ DACCtrlAttrHaveChanged s s o. 
intros; intro;
 eapply
  (NoDACChange s o (subjectSC s) (objectSC s) (files s) 
     (directories s) (secmat s)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
generalize H; elim s; simpl in |- *; auto. 
 
Qed. 
 
 
Lemma NoMACObjChange :
 forall (s : SFSstate) (o : OBJECT) (FILES : set (OBJECT * FILECONT))
   (DIRECTS : set (OBJECT * DIRCONT))
   (ACL : set (OBJECT * AccessCtrlListData)) (SSC : set (SUBJECT * SecClass))
   (SM : set (OBJECT * ReadersWriters)),
 ~
 MACObjCtrlAttrHaveChanged s
   (mkSFS (groups s) (primaryGrp s) SSC (AllGrp s) 
      (RootGrp s) (SecAdmGrp s) (objectSC s) ACL SM FILES DIRECTS) o. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intros; intro. 
(* Goal: False *)
inversion H; simpl in H1. 
(* Goal: False *)
cut (x = y). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro EQ; rewrite EQ in H2; inversion H2; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
rewrite H0 in H1; injection H1; auto. 
 
Qed. 
 
 
Lemma NoMACObjChange2 :
 forall (s : SFSstate) (o : OBJECT), ~ MACObjCtrlAttrHaveChanged s s o. 
intros; intro;
 eapply
  (NoMACObjChange s o (files s) (directories s) (acl s) 
     (subjectSC s) (secmat s)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
generalize H; elim s; simpl in |- *; auto. 
 
Qed. 
 
 
Lemma NoMACSubChange :
 forall (s : SFSstate) (u : SUBJECT)
   (ACL : set (OBJECT * AccessCtrlListData)) (OSC : set (OBJECT * SecClass))
   (FILES : set (OBJECT * FILECONT)) (DIRECTS : set (OBJECT * DIRCONT))
   (SM : set (OBJECT * ReadersWriters)),
 ~
 MACSubCtrlAttrHaveChanged s
   (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) 
      (RootGrp s) (SecAdmGrp s) OSC ACL SM FILES DIRECTS) u. 
(* Goal: forall (s : SFSstate) (u : SUBJECT) (ACL : set (prod OBJECT AccessCtrlListData)) (OSC : set (prod OBJECT SecClass)) (FILES : set (prod OBJECT FILECONT)) (DIRECTS : set (prod OBJECT DIRCONT)) (SM : set (prod OBJECT ReadersWriters)), not (MACSubCtrlAttrHaveChanged s (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s) (RootGrp s) (SecAdmGrp s) OSC ACL SM FILES DIRECTS) u) *)
intros; intro; inversion H. 
(* Goal: False *)
simpl in H1. 
(* Goal: False *)
cut (x = y). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro EQ; rewrite EQ in H2; inversion H2; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
rewrite H0 in H1; injection H1; auto. 
 
Qed. 
 
 
Lemma NoMACSubChange2 :
 forall (s : SFSstate) (u : SUBJECT), ~ MACSubCtrlAttrHaveChanged s s u. 
intros; intro;
 eapply
  (NoMACSubChange s u (acl s) (objectSC s) (files s) 
     (directories s) (secmat s)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
generalize H; elim s; simpl in |- *; auto. 
 
Qed. 
 
 
Lemma eq_scSym : forall a b : SecClass, eq_sc a b -> eq_sc b a. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
unfold eq_sc in |- *; intros. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim H; intros. 
(* Goal: and (@eq SECLEV (level b) (level a)) (@eq (set CATEGORY) (categs b) (categs a)) *)
rewrite H0; rewrite H1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
Qed. 
 
 
Lemma ChsubscPSS1 :
 forall (s : SFSstate) (u : SUBJECT) (y : ReadersWriters),
 (forall rw : ReadersWriters,
  ~ set_In u (ActReaders rw) /\ ~ set_In u (ActWriters rw)) ->
 ~ (set_In u (ActReaders y) \/ set_In u (ActWriters y)). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
(* Goal: not (or (@set_In SUBJECT u (ActReaders y)) (@set_In SUBJECT u (ActWriters y))) *)
cut (~ set_In u (ActReaders y) /\ ~ set_In u (ActWriters y)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
tauto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma EqfSSC1 :
 forall (s : SFSstate) (u u0 : SUBJECT) (sc : SecClass),
 u <> u0 -> fSSC (subjectSC s) u0 = fSSC (chsubsc_SC s u sc) u0. 
(* Goal: forall (s : SFSstate) (u : SUBJECT) (sc : SecClass) (_ : FuncPre7 s), iff (@eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)) (@eq (Exc SecClass) (fSSC (chsubsc_SC s u sc) u) (@None SecClass)) *)
intros; unfold chsubsc_SC in |- *. 
(* Goal: @eq (Exc SecClass) (fSSC (subjectSC s) u0) (fSSC match fSSC (subjectSC s) u with | Some y => @set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u y) (subjectSC s)) | None => subjectSC s end u0) *)
elim (fSSC (subjectSC s) u). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intros; unfold fSSC in |- *; apply AddRemEq; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma Close_smCorr :
 forall (s : SFSstate) (Sub : SUBJECT) (o : OBJECT),
 FuncPre5 s ->
 match fsecmat (secmat s) o with
 | Some y => set_In Sub (set_union SUBeq_dec (ActReaders y) (ActWriters y))
 | None => False
 end ->
 match fsecmat (close_sm s Sub o) o with
 | None => True
 | Some y => ~ set_In Sub (ActReaders y) /\ ~ set_In Sub (ActWriters y)
 end. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (ownerclose_sm s Sub 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 *)
intros until o. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall (_ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (close_sm s Sub 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) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold close_sm in |- *. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim (fsecmat (secmat s) o); intros. 
elim (set_remove SUBeq_dec Sub (ActReaders a));
 elim (set_remove SUBeq_dec Sub (ActWriters a)). 
replace (fsecmat (set_remove SECMATeq_dec (o, a) (secmat s)) o) with
 (None (A:=ReadersWriters)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
symmetry  in |- *; unfold fsecmat in |- *; unfold FuncPre5 in H0; auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
replace
 (fsecmat
    (set_add SECMATeq_dec (o, NEWRW Sub o a)
       (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
 (Some (NEWRW Sub o a)). 
(* Goal: and (not (@set_In SUBJECT Sub (ActReaders (NEWRW Sub o a)))) (not (@set_In SUBJECT Sub (ActWriters (NEWRW Sub o a)))) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRW Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRW Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => and (not (@set_In SUBJECT Sub (ActReaders y))) (not (@set_In SUBJECT Sub (ActWriters y))) | None => True end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRW in |- *; simpl in |- *; split; apply Set_remove1. 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec (o, NEWRW Sub o a)
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (NEWRW Sub o a)). 
(* Goal: and (not (@set_In SUBJECT Sub (ActReaders (NEWRW Sub o a)))) (not (@set_In SUBJECT Sub (ActWriters (NEWRW Sub o a)))) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRW Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRW Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => and (not (@set_In SUBJECT Sub (ActReaders y))) (not (@set_In SUBJECT Sub (ActWriters y))) | None => True end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRW in |- *; simpl in |- *; split; apply Set_remove1. 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec (o, NEWRW Sub o a)
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (NEWRW Sub o a)). 
(* Goal: and (not (@set_In SUBJECT Sub (ActReaders (NEWRW Sub o a)))) (not (@set_In SUBJECT Sub (ActWriters (NEWRW Sub o a)))) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRW Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRW Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => and (not (@set_In SUBJECT Sub (ActReaders y))) (not (@set_In SUBJECT Sub (ActWriters y))) | None => True end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRW in |- *; simpl in |- *; split; apply Set_remove1. 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
tauto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Close_smCorr2 :
 forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT),
 FuncPre5 s ->
 match fsecmat (secmat s) o with
 | Some y => set_In Sub (set_union SUBeq_dec (ActReaders y) (ActWriters y))
 | None => False
 end ->
 match fsecmat (close_sm s Sub 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 (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (ownerclose_sm s Sub 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 *)
intros until o. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall (_ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (close_sm s Sub 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) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold close_sm in |- *. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim (fsecmat (secmat s) o); intros. 
elim (set_remove SUBeq_dec Sub (ActReaders a));
 elim (set_remove SUBeq_dec Sub (ActWriters a)). 
replace (fsecmat (set_remove SECMATeq_dec (o, a) (secmat s)) o) with
 (None (A:=ReadersWriters)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
symmetry  in |- *; unfold fsecmat in |- *; unfold FuncPre5 in H; auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
replace
 (fsecmat
    (set_add SECMATeq_dec (o, NEWRW Sub o a)
       (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
 (Some (NEWRW Sub o a)). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRW in |- *; simpl in |- *. 
split;
 [ intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActReaders a) (x:=u0) (y:=Sub)); auto
 | intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActWriters a) (x:=u0) (y:=Sub)); auto ]. 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
replace
 (fsecmat
    (set_add SECMATeq_dec (o, NEWRW Sub o a)
       (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
 (Some (NEWRW Sub o a)). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRW in |- *; simpl in |- *. 
split;
 [ intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActReaders a) (x:=u0) (y:=Sub)); auto
 | intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActWriters a) (x:=u0) (y:=Sub)); auto ]. 
 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
replace
 (fsecmat
    (set_add SECMATeq_dec (o, NEWRW Sub o a)
       (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
 (Some (NEWRW Sub o a)). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRW in |- *; simpl in |- *. 
split;
 [ intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActReaders a) (x:=u0) (y:=Sub)); auto
 | intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActWriters a) (x:=u0) (y:=Sub)); auto ]. 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
tauto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Eqfsecmat1 :
 forall (s : SFSstate) (o1 o2 : OBJECT) (u : SUBJECT),
 o1 <> o2 -> fsecmat (secmat s) o2 = fsecmat (close_sm s u o1) o2. 
unfold close_sm, fsecmat in |- *; intros;
 elim (PARTFUNC OBJeq_dec (secmat s) o1). 
intro; elim (set_remove SUBeq_dec u (ActReaders a));
 elim (set_remove SUBeq_dec u (ActWriters a)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma Close_smCorr3 :
 forall (s : SFSstate) (Sub : SUBJECT) (o : OBJECT),
 fsecmat (secmat s) o = None -> fsecmat (close_sm s Sub o) o = None. 
(* Goal: forall (_ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (close_sm s Sub 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) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
intros until o; unfold close_sm in |- *. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intro. 
(* Goal: @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
generalize H. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
(* Goal: forall (a : ReadersWriters) (_ : @eq (Exc ReadersWriters) (@Some ReadersWriters a) (@None ReadersWriters)), @eq (Exc ReadersWriters) (fsecmat match @set_remove SUBJECT SUBeq_dec Sub (ActReaders a) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters a) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s)) end o) (@None ReadersWriters) *)
(* Goal: forall _ : @eq (Exc ReadersWriters) (@None ReadersWriters) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
intros y H0; discriminate H0. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma OwnerClose_smCorr2 :
 forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT),
 FuncPre5 s ->
 match fsecmat (secmat s) o with
 | Some y => set_In Sub (set_union SUBeq_dec (ActReaders y) (ActWriters y))
 | None => False
 end ->
 match fsecmat (ownerclose_sm s Sub 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 (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (ownerclose_sm s Sub 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 *)
intros until o. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall (_ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (ownerclose_sm s Sub 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) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold ownerclose_sm in |- *. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
elim (fsecmat (secmat s) o); intros. 
elim (set_remove SUBeq_dec Sub (ActReaders a));
 elim (set_remove SUBeq_dec Sub (ActWriters a)). 
replace (fsecmat (set_remove SECMATeq_dec (o, a) (secmat s)) o) with
 (None (A:=ReadersWriters)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
symmetry  in |- *; unfold fsecmat in |- *; unfold FuncPre5 in H0; auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
replace
 (fsecmat
    (set_add SECMATeq_dec (o, NEWRWOC Sub o a)
       (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
 (Some (NEWRWOC Sub o a)). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRWOC in |- *; simpl in |- *. 
split;
 [ intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActReaders a) (x:=u0) (y:=Sub)); auto
 | intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActWriters a) (x:=u0) (y:=Sub)); auto ]. 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
replace
 (fsecmat
    (set_add SECMATeq_dec (o, NEWRWOC Sub o a)
       (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
 (Some (NEWRWOC Sub o a)). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRWOC in |- *; simpl in |- *. 
split;
 [ intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActReaders a) (x:=u0) (y:=Sub)); auto
 | intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActWriters a) (x:=u0) (y:=Sub)); auto ]. 
 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
replace
 (fsecmat
    (set_add SECMATeq_dec (o, NEWRWOC Sub o a)
       (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
 (Some (NEWRWOC Sub o a)). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold NEWRWOC in |- *; simpl in |- *. 
split;
 [ intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActReaders a) (x:=u0) (y:=Sub)); auto
 | intro;
    eapply
     (Set_remove2 (A:=SUBJECT) (Aeq_dec:=SUBeq_dec) (B:=
        ActWriters a) (x:=u0) (y:=Sub)); auto ]. 
 
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (NEWRWOC Sub o a)) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: match fsecmat (secmat s) o with | Some y => False | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold fsecmat in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
tauto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Eqfsecmat2 :
 forall (s : SFSstate) (o1 o2 : OBJECT) (u : SUBJECT),
 o1 <> o2 -> fsecmat (secmat s) o2 = fsecmat (ownerclose_sm s u o1) o2. 
unfold ownerclose_sm, fsecmat in |- *; intros;
 elim (PARTFUNC OBJeq_dec (secmat s) o1). 
intro; elim (set_remove SUBeq_dec u (ActReaders a));
 elim (set_remove SUBeq_dec u (ActWriters a)). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma OwnerClose_smCorr3 :
 forall (s : SFSstate) (Sub : SUBJECT) (o : OBJECT),
 fsecmat (secmat s) o = None -> fsecmat (ownerclose_sm s Sub o) o = None. 
(* Goal: forall (_ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end) (_ : FuncPre5 s) (_ : match fsecmat (secmat s) o with | Some y => @set_In SUBJECT Sub (@set_union SUBJECT SUBeq_dec (ActReaders y) (ActWriters y)) | None => False end), match fsecmat (ownerclose_sm s Sub 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) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
intros until o; unfold ownerclose_sm in |- *. 
(* Goal: forall _ : @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
intro. 
(* Goal: @eq (Exc ReadersWriters) (fsecmat match fsecmat (secmat s) o with | Some y => match @set_remove SUBJECT SUBeq_dec Sub (ActReaders y) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters y) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o y)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) end | None => secmat s end o) (@None ReadersWriters) *)
generalize H. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
(* Goal: forall (a : ReadersWriters) (_ : @eq (Exc ReadersWriters) (@Some ReadersWriters a) (@None ReadersWriters)), @eq (Exc ReadersWriters) (fsecmat match @set_remove SUBJECT SUBeq_dec Sub (ActReaders a) with | nil => match @set_remove SUBJECT SUBeq_dec Sub (ActWriters a) with | nil => @set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s) | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s)) end | cons s0 l => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (NEWRWOC Sub o a)) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s)) end o) (@None ReadersWriters) *)
(* Goal: forall _ : @eq (Exc ReadersWriters) (@None ReadersWriters) (@None ReadersWriters), @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
intros y H0; discriminate H0. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
Qed. 
 
 
Lemma Open_smCorr3 :
 forall (s : SFSstate) (Sub : SUBJECT) (o : OBJECT) (m : MODE),
 FuncPre5 s ->
 fsecmat (open_sm s Sub o m) o = None -> fsecmat (secmat s) o = None. 
(* Goal: forall (s : SFSstate) (Sub : SUBJECT) (o : OBJECT) (m : MODE) (_ : FuncPre5 s) (_ : @eq (Exc ReadersWriters) (fsecmat (open_sm s Sub o m) o) (@None ReadersWriters)), @eq (Exc ReadersWriters) (fsecmat (secmat s) o) (@None ReadersWriters) *)
intros until m; intro; unfold open_sm in |- *. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim m; elim (fsecmat (secmat s) o). 
intro; intro;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o, mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))). 
(* Goal: forall _ : @eq (Exc ReadersWriters) (@Some ReadersWriters (mkRW (@set_add SUBJECT SUBeq_dec Sub (ActReaders a)) (ActWriters a))) (@None ReadersWriters), @eq (Exc ReadersWriters) (@Some ReadersWriters a) (@None ReadersWriters) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (@set_add SUBJECT SUBeq_dec Sub (ActReaders a)) (ActWriters a))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (@set_add SUBJECT SUBeq_dec Sub (ActReaders a)) (ActWriters a))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s)))) (_ : @eq (Exc ReadersWriters) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))) (secmat s)) o) (@None ReadersWriters)), @eq (Exc ReadersWriters) (@None ReadersWriters) (@None ReadersWriters) *)
(* Goal: forall (a : ReadersWriters) (_ : @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o a) (secmat s)) (_ : @eq (Exc ReadersWriters) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) (@None ReadersWriters)), @eq (Exc ReadersWriters) (@Some ReadersWriters a) (@None ReadersWriters) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s)))) (_ : @eq (Exc ReadersWriters) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o) (@None ReadersWriters)), @eq (Exc ReadersWriters) (@None ReadersWriters) (@None ReadersWriters) *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
intros H2; discriminate H2. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
intro;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o,
        mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))
        (secmat s)) o) with
  (Some
     (mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))). 
(* Goal: forall _ : @eq (Exc SecClass) (@Some SecClass sc) (@None SecClass), @eq (Exc SecClass) (@Some SecClass a) (@None SecClass) *)
(* Goal: @eq (option SecClass) (@Some SecClass sc) (fSSC (@set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u a) (subjectSC s))) u) *)
(* Goal: forall (_ : not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s)))) (_ : @eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)), @eq (Exc SecClass) (@None SecClass) (@None SecClass) *)
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro H2; discriminate H2. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
intro; intro;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o, mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))). 
(* Goal: forall _ : @eq (Exc SecClass) (@Some SecClass sc) (@None SecClass), @eq (Exc SecClass) (@Some SecClass a) (@None SecClass) *)
(* Goal: @eq (option SecClass) (@Some SecClass sc) (fSSC (@set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u a) (subjectSC s))) u) *)
(* Goal: forall (_ : not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s)))) (_ : @eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)), @eq (Exc SecClass) (@None SecClass) (@None SecClass) *)
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro H2; discriminate H2. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
intro;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o,
        mkRW (empty_set SUBJECT) (set_add SUBeq_dec Sub (empty_set SUBJECT)))
        (secmat s)) o) with
  (Some
     (mkRW (empty_set SUBJECT) (set_add SUBeq_dec Sub (empty_set SUBJECT)))). 
(* Goal: forall _ : @eq (Exc SecClass) (@Some SecClass sc) (@None SecClass), @eq (Exc SecClass) (@Some SecClass a) (@None SecClass) *)
(* Goal: @eq (option SecClass) (@Some SecClass sc) (fSSC (@set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u a) (subjectSC s))) u) *)
(* Goal: forall (_ : not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s)))) (_ : @eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)), @eq (Exc SecClass) (@None SecClass) (@None SecClass) *)
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro H2; discriminate H2. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Open_smCorr21 :
 forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (m : MODE),
 Sub <> u0 ->
 FuncPre5 s ->
 match fsecmat (open_sm s Sub o READ) o, fsecmat (secmat s) o with
 | Some y, None =>
     ActReaders y = set_add SUBeq_dec Sub (empty_set SUBJECT) /\
     ActWriters y = empty_set SUBJECT
 | None, _ => False
 | 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 (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold open_sm in |- *. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o, mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
simpl in |- *. 
(* Goal: and (forall _ : @set_In SUBJECT u0 (@set_add SUBJECT SUBeq_dec Sub (ActReaders a)), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters a), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (@set_add SUBJECT SUBeq_dec Sub (ActReaders a)) (ActWriters a))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (@set_add SUBJECT SUBeq_dec Sub (ActReaders a)) (ActWriters a))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActWriters y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
split; (intros; eauto). 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o,
        mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))
        (secmat s)) o) with
  (Some
     (mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Open_smCorr22 :
 forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (m : MODE),
 Sub <> u0 ->
 FuncPre5 s ->
 match fsecmat (open_sm s Sub o WRITE) o, fsecmat (secmat s) o with
 | Some y, None =>
     ActWriters y = set_add SUBeq_dec Sub (empty_set SUBJECT) /\
     ActReaders y = empty_set SUBJECT
 | None, _ => False
 | 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 (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold open_sm in |- *. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o, mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))). 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (ActWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
simpl in |- *. 
(* Goal: and (forall _ : @set_In SUBJECT u0 (ActReaders a), @set_In SUBJECT u0 (ActReaders a)) (forall _ : @set_In SUBJECT u0 (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)), @set_In SUBJECT u0 (ActWriters a)) *)
(* Goal: @eq (option ReadersWriters) (@Some ReadersWriters (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders a) (@set_add SUBJECT SUBeq_dec Sub (ActWriters a)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o a) (secmat s))) o) *)
(* Goal: forall _ : not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))), match fsecmat (@set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s)) o with | Some y => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
split; (intro; eauto). 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o,
        mkRW (empty_set SUBJECT) (set_add SUBeq_dec Sub (empty_set SUBJECT)))
        (secmat s)) o) with
  (Some
     (mkRW (empty_set SUBJECT) (set_add SUBeq_dec Sub (empty_set SUBJECT)))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Eqfsecmat3 :
 forall (s : SFSstate) (o1 o2 : OBJECT) (u : SUBJECT) (m : MODE),
 o1 <> o2 -> fsecmat (secmat s) o2 = fsecmat (open_sm s u o1 m) o2. 
(* Goal: forall (s : SFSstate) (o1 o2 : OBJECT) (u : SUBJECT) (m : MODE) (_ : not (@eq OBJECT o1 o2)), @eq (Exc ReadersWriters) (fsecmat (secmat s) o2) (fsecmat (open_sm s u o1 m) o2) *)
intros until m; unfold fsecmat, open_sm in |- *. 
(* Goal: forall _ : not (@eq OBJECT o1 o2), @eq (Exc ReadersWriters) (@PARTFUNC OBJECT ReadersWriters OBJeq_dec (secmat s) o2) (@PARTFUNC OBJECT ReadersWriters OBJeq_dec match fsecmat (secmat s) o1 with | Some y => match m with | READ => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o1 (mkRW (@set_add SUBJECT SUBeq_dec u (ActReaders y)) (ActWriters y))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o1 y) (secmat s)) | WRITE => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o1 (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec u (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o1 y) (secmat s)) end | None => match m with | READ => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o1 (mkRW (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)) (empty_set SUBJECT))) (secmat s) | WRITE => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o1 (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec u (empty_set SUBJECT)))) (secmat s) end end o2) *)
elim m; elim (fsecmat (secmat s) o1). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intros; apply AddRemEq; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intros; apply AddEq; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intros; apply AddRemEq; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intros; apply AddEq; auto. 
 
Qed. 
 
 
Lemma Chobjsc_Corr :
 forall (s : SFSstate) (o : OBJECT) (sc : SecClass),
 FuncPre6 s ->
 (fOSC (objectSC s) o = None <-> fOSC (chobjsc_SC s o sc) o = None). 
(* Goal: forall (s : SFSstate) (o : OBJECT) (sc : SecClass) (_ : FuncPre6 s), iff (@eq (Exc SecClass) (fOSC (objectSC s) o) (@None SecClass)) (@eq (Exc SecClass) (fOSC (chobjsc_SC s o sc) o) (@None SecClass)) *)
intros; unfold chobjsc_SC in |- *. 
cut
 match fOSC (objectSC s) o with
 | Some y => set_In (o, y) (objectSC s)
 | None => ~ set_In o (DOM OBJeq_dec (objectSC s))
 end. 
(* Goal: forall _ : match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end, iff (@eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)) (@eq (Exc SecClass) (fSSC match fSSC (subjectSC s) u with | Some y => @set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u y) (subjectSC s)) | None => subjectSC s end u) (@None SecClass)) *)
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
split. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro H1; rewrite H1; auto. 
 
(* Goal: forall _ : @eq (Exc SecClass) (fOSC match fOSC (objectSC s) o with | Some y => @set_add (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o sc) (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o y) (objectSC s)) | None => objectSC s end o) (@None SecClass), @eq (Exc SecClass) (fOSC (objectSC s) o) (@None SecClass) *)
(* Goal: match fOSC (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
generalize H0; elim (fOSC (objectSC s) o). 
intro; intro;
 replace
  (fOSC
     (set_add OSCeq_dec (o, sc) (set_remove OSCeq_dec (o, a) (objectSC s))) o)
  with (Some sc). 
(* Goal: forall _ : @eq (Exc SecClass) (@Some SecClass sc) (@None SecClass), @eq (Exc SecClass) (@Some SecClass a) (@None SecClass) *)
(* Goal: @eq (option SecClass) (@Some SecClass sc) (fSSC (@set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u a) (subjectSC s))) u) *)
(* Goal: forall (_ : not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s)))) (_ : @eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)), @eq (Exc SecClass) (@None SecClass) (@None SecClass) *)
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro H2; discriminate H2. 
 
(* Goal: @eq (option SecClass) (@Some SecClass sc) (fOSC (@set_add (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o sc) (@set_remove (prod OBJECT SecClass) OSCeq_dec (@pair OBJECT SecClass o a) (objectSC s))) o) *)
(* Goal: forall (_ : not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s)))) (_ : @eq (Exc SecClass) (fOSC (objectSC s) o) (@None SecClass)), @eq (Exc SecClass) (@None SecClass) (@None SecClass) *)
(* Goal: match fOSC (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fOSC in |- *; apply AddEq1. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fOSC in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Aux1 :
 forall y : SecClass, ~ (Some y = None <-> None = None :>option SecClass). 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intro; unfold iff in |- *; intro H; elim H; intros. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
absurd (Some y = None); auto. 
(* Goal: not (@eq (option SecClass) (@Some SecClass y) (@None SecClass)) *)
intro D; discriminate D. 
 
Qed. 
 
 
Lemma Chsubsc_Corr :
 forall (s : SFSstate) (u : SUBJECT) (sc : SecClass),
 FuncPre7 s ->
 (fSSC (subjectSC s) u = None <-> fSSC (chsubsc_SC s u sc) u = None). 
(* Goal: forall (s : SFSstate) (u : SUBJECT) (sc : SecClass) (_ : FuncPre7 s), iff (@eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)) (@eq (Exc SecClass) (fSSC (chsubsc_SC s u sc) u) (@None SecClass)) *)
intros; unfold chsubsc_SC in |- *. 
cut
 match fSSC (subjectSC s) u with
 | Some y => set_In (u, y) (subjectSC s)
 | None => ~ set_In u (DOM SUBeq_dec (subjectSC s))
 end. 
(* Goal: forall _ : match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end, iff (@eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)) (@eq (Exc SecClass) (fSSC match fSSC (subjectSC s) u with | Some y => @set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u y) (subjectSC s)) | None => subjectSC s end u) (@None SecClass)) *)
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
split. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro H1; rewrite H1; auto. 
 
(* Goal: @eq (Exc SecClass) (fSSC (subjectSC s) u0) (fSSC match fSSC (subjectSC s) u with | Some y => @set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u y) (subjectSC s)) | None => subjectSC s end u0) *)
generalize H0; elim (fSSC (subjectSC s) u). 
intro; intro;
 replace
  (fSSC
     (set_add SSCeq_dec (u, sc) (set_remove SSCeq_dec (u, a) (subjectSC s)))
     u) with (Some sc). 
(* Goal: forall _ : @eq (Exc SecClass) (@Some SecClass sc) (@None SecClass), @eq (Exc SecClass) (@Some SecClass a) (@None SecClass) *)
(* Goal: @eq (option SecClass) (@Some SecClass sc) (fSSC (@set_add (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u sc) (@set_remove (prod SUBJECT SecClass) SSCeq_dec (@pair SUBJECT SecClass u a) (subjectSC s))) u) *)
(* Goal: forall (_ : not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s)))) (_ : @eq (Exc SecClass) (fSSC (subjectSC s) u) (@None SecClass)), @eq (Exc SecClass) (@None SecClass) (@None SecClass) *)
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
intro H2; discriminate H2. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fSSC in |- *; apply AddEq1; auto. 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
auto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fSSC in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Open_smCorr31 :
 forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (m : MODE),
 FuncPre5 s ->
 match fsecmat (open_sm s Sub o READ) o, fsecmat (secmat s) o with
 | Some y, None =>
     ActReaders y = set_add SUBeq_dec Sub (empty_set SUBJECT) /\
     ActWriters y = empty_set SUBJECT
 | None, _ => False
 | Some y, Some z => set_In u0 (ActWriters y) -> set_In u0 (ActWriters z)
 end. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold open_sm in |- *. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o, mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (mkRW (set_add SUBeq_dec Sub (ActReaders a)) (ActWriters a))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o,
        mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))
        (secmat s)) o) with
  (Some
     (mkRW (set_add SUBeq_dec Sub (empty_set SUBJECT)) (empty_set SUBJECT))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
 
Lemma Open_smCorr32 :
 forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (m : MODE),
 FuncPre5 s ->
 match fsecmat (open_sm s Sub o WRITE) o, fsecmat (secmat s) o with
 | Some y, None =>
     ActWriters y = set_add SUBeq_dec Sub (empty_set SUBJECT) /\
     ActReaders y = empty_set SUBJECT
 | None, _ => False
 | Some y, Some z => set_In u0 (ActReaders y) -> set_In u0 (ActReaders z)
 end. 
(* Goal: forall (s : SFSstate) (Sub u0 : SUBJECT) (o : OBJECT) (_ : MODE) (_ : FuncPre5 s), match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
intros. 
cut
 match fsecmat (secmat s) o with
 | Some y => set_In (o, y) (secmat s)
 | None => ~ set_In o (DOM OBJeq_dec (secmat s))
 end. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat (open_sm s Sub o WRITE) o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
unfold open_sm in |- *. 
(* Goal: forall _ : match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end, match fsecmat match fsecmat (secmat s) o with | Some y => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (ActReaders y) (@set_add SUBJECT SUBeq_dec Sub (ActWriters y)))) (@set_remove (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o y) (secmat s)) | None => @set_add (prod OBJECT ReadersWriters) SECMATeq_dec (@pair OBJECT ReadersWriters o (mkRW (empty_set SUBJECT) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT)))) (secmat s) end o with | Some y => match fsecmat (secmat s) o with | Some z => forall _ : @set_In SUBJECT u0 (ActReaders y), @set_In SUBJECT u0 (ActReaders z) | None => and (@eq (set SUBJECT) (ActWriters y) (@set_add SUBJECT SUBeq_dec Sub (empty_set SUBJECT))) (@eq (set SUBJECT) (ActReaders y) (empty_set SUBJECT)) end | None => False end *)
(* Goal: match fsecmat (secmat s) o with | Some y => @set_In (prod OBJECT ReadersWriters) (@pair OBJECT ReadersWriters o y) (secmat s) | None => not (@set_In OBJECT o (@DOM OBJECT ReadersWriters OBJeq_dec (secmat s))) end *)
elim (fsecmat (secmat s) o). 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o, mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))
        (set_remove SECMATeq_dec (o, a) (secmat s))) o) with
  (Some (mkRW (ActReaders a) (set_add SUBeq_dec Sub (ActWriters a)))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
intros;
 replace
  (fsecmat
     (set_add SECMATeq_dec
        (o,
        mkRW (empty_set SUBJECT) (set_add SUBeq_dec Sub (empty_set SUBJECT)))
        (secmat s)) o) with
  (Some
     (mkRW (empty_set SUBJECT) (set_add SUBeq_dec Sub (empty_set SUBJECT)))). 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
simpl in |- *; auto. 
 
(* Goal: match fSSC (subjectSC s) u with | Some y => @set_In (prod SUBJECT SecClass) (@pair SUBJECT SecClass u y) (subjectSC s) | None => not (@set_In SUBJECT u (@DOM SUBJECT SecClass SUBeq_dec (subjectSC s))) end *)
unfold fsecmat in |- *; apply AddEq1; auto. 
 
(* Goal: match @PARTFUNC OBJECT SecClass OBJeq_dec (objectSC s) o with | Some y => @set_In (prod OBJECT SecClass) (@pair OBJECT SecClass o y) (objectSC s) | None => not (@set_In OBJECT o (@DOM OBJECT SecClass OBJeq_dec (objectSC s))) end *)
unfold fsecmat in |- *; apply DOMFuncRel4. 
 
Qed. 
 
Hint Resolve eq_scIMPLYle_sc eq_scSym Eqfsecmat1 Close_smCorr3 TwoImpLeft
  TwoImpRight EqfOSC1 ChsubscPSS1 Eqfsecmat2 NoMACObjChange NoDACChange
  NoMACSubChange EqfOSC6 Eqfacl1 Eqfacl2 Eqfacl3 EqfOSC1 EqfOSC2 EqfOSC3 Aux1
  NotInDOMIsUndef2 Eqfacl4 EqfOSC4 EqfOSC5 EqfSSC1 OwnerClose_smCorr3
  Open_smCorr3 Eqfsecmat3 Chobjsc_Corr NoMACObjChange2 NoDACChange2
  NoMACSubChange2 Chsubsc_Corr NotInDOMIsUndef3 Eqfacl5 EqfOSC7. 
