| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (617 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (65 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (50 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (90 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (153 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |
Global Index
A
AccessCtrlListData [record, in FSSecModel.SFSstate]ACL [constructor, in FSSecModel.ModelProperties]
acl [projection, in FSSecModel.SFSstate]
AclChanged [inductive, in FSSecModel.ModelProperties]
acldata [constructor, in FSSecModel.SFSstate]
ACLeq_dec [axiom, in FSSecModel.SFSstate]
ACLGrp [constructor, in FSSecModel.DACandMAC]
ACLOwner [constructor, in FSSecModel.DACandMAC]
aclstat [inductive, in FSSecModel.aclstat]
Aclstat [section, in FSSecModel.aclstat]
Aclstat [constructor, in FSSecModel.SFSstate]
aclstat [library]
aclstatIsSecure [section, in FSSecModel.aclstatIsSecure]
aclstatIsSecure [library]
AclstatOK [constructor, in FSSecModel.aclstat]
AclstatPCP [lemma, in FSSecModel.aclstatIsSecure]
AclstatPSP [lemma, in FSSecModel.aclstatIsSecure]
AclstatPSS [lemma, in FSSecModel.aclstatIsSecure]
Aclstat.s [variable, in FSSecModel.aclstat]
ActReaders [projection, in FSSecModel.SFSstate]
ActWriters [projection, in FSSecModel.SFSstate]
AddEq [lemma, in FSSecModel.SFSstate]
AddEq1 [lemma, in FSSecModel.SFSstate]
AddRemEq [lemma, in FSSecModel.SFSstate]
AddUsrGrpToAcl [constructor, in FSSecModel.SFSstate]
addUsrGrpToAcl [inductive, in FSSecModel.addUsrGrpToAcl]
AddUsrGrpToAcl [section, in FSSecModel.addUsrGrpToAcl]
addUsrGrpToAcl [library]
addUsrGrpToAclIsSecure [section, in FSSecModel.addUsrGrpToAclIsSecure]
addUsrGrpToAclIsSecure [library]
addUsrGrpToAclOK [constructor, in FSSecModel.addUsrGrpToAcl]
AddUsrGrpToAclPCP [lemma, in FSSecModel.addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSP [lemma, in FSSecModel.addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSS [lemma, in FSSecModel.addUsrGrpToAclIsSecure]
addUsrGrpToAcl_acl [definition, in FSSecModel.addUsrGrpToAcl]
AddUsrGrpToAcl.NEW [variable, in FSSecModel.addUsrGrpToAcl]
AddUsrGrpToAcl.s [variable, in FSSecModel.addUsrGrpToAcl]
AddUsrGrpToAcl.t [variable, in FSSecModel.addUsrGrpToAcl]
AllGrp [projection, in FSSecModel.SFSstate]
allowedTo [constructor, in FSSecModel.SFSstate]
allunique [definition, in FSSecModel.ListFunctions]
AllWaysIncluded [lemma, in FSSecModel.ListFunctions]
AuxiliaryLemmas [library]
Aux1 [lemma, in FSSecModel.AuxiliaryLemmas]
B
BasicSecurityTheorem [lemma, in FSSecModel.ModelLemmas]BYTE [axiom, in FSSecModel.SFSstate]
BYTEeq_dec [axiom, in FSSecModel.SFSstate]
C
Categ [constructor, in FSSecModel.ModelProperties]CATEGORY [axiom, in FSSecModel.SFSstate]
categs [projection, in FSSecModel.SFSstate]
ChangeGroupO [definition, in FSSecModel.setACLdata]
ChangeGroupR [definition, in FSSecModel.setACLdata]
ChangeGroupW [definition, in FSSecModel.setACLdata]
ChangeUserR [definition, in FSSecModel.setACLdata]
ChangeUserW [definition, in FSSecModel.setACLdata]
chmod [inductive, in FSSecModel.chmod]
Chmod [section, in FSSecModel.chmod]
Chmod [constructor, in FSSecModel.SFSstate]
chmod [library]
chmodIsSecure [section, in FSSecModel.chmodIsSecure]
chmodIsSecure [library]
ChmodOK [constructor, in FSSecModel.chmod]
ChmodPCP [lemma, in FSSecModel.chmodIsSecure]
ChmodPSP [lemma, in FSSecModel.chmodIsSecure]
ChmodPSS [lemma, in FSSecModel.chmodIsSecure]
chmod_acl [definition, in FSSecModel.chmod]
Chmod.ChangeGAR [variable, in FSSecModel.chmod]
Chmod.ChangeGAW [variable, in FSSecModel.chmod]
Chmod.NEW [variable, in FSSecModel.chmod]
Chmod.s [variable, in FSSecModel.chmod]
Chmod.t [variable, in FSSecModel.chmod]
Chobjsc [constructor, in FSSecModel.SFSstate]
chobjsc [inductive, in FSSecModel.chobjsc]
Chobjsc [section, in FSSecModel.chobjsc]
chobjsc [library]
chobjscIsSecure [section, in FSSecModel.chobjscIsSecure]
chobjscIsSecure [library]
ChobjscPCP [lemma, in FSSecModel.chobjscIsSecure]
ChobjscPSP [lemma, in FSSecModel.chobjscIsSecure]
ChobjscPSS [lemma, in FSSecModel.chobjscIsSecure]
Chobjsc_Corr [lemma, in FSSecModel.AuxiliaryLemmas]
chobjsc_SC [definition, in FSSecModel.chobjsc]
Chobjsc.s [variable, in FSSecModel.chobjsc]
Chobjsc.t [variable, in FSSecModel.chobjsc]
chown [inductive, in FSSecModel.chown]
Chown [section, in FSSecModel.chown]
Chown [constructor, in FSSecModel.SFSstate]
chown [library]
chownIsSecure [section, in FSSecModel.chownIsSecure]
chownIsSecure [library]
ChownOK [constructor, in FSSecModel.chown]
ChownPCP [lemma, in FSSecModel.chownIsSecure]
ChownPSP [lemma, in FSSecModel.chownIsSecure]
ChownPSS [lemma, in FSSecModel.chownIsSecure]
chown_acl [definition, in FSSecModel.chown]
Chown.NEW [variable, in FSSecModel.chown]
Chown.NEW_UO [variable, in FSSecModel.chown]
Chown.NEW_GRP [variable, in FSSecModel.chown]
Chown.s [variable, in FSSecModel.chown]
Chown.t [variable, in FSSecModel.chown]
chsobjscOK [constructor, in FSSecModel.chobjsc]
chsubsc [inductive, in FSSecModel.chsubsc]
Chsubsc [section, in FSSecModel.chsubsc]
Chsubsc [constructor, in FSSecModel.SFSstate]
chsubsc [library]
chsubscIsSecure [section, in FSSecModel.chsubscIsSecure]
chsubscIsSecure [library]
chsubscOK [constructor, in FSSecModel.chsubsc]
ChsubscPCP [lemma, in FSSecModel.chsubscIsSecure]
ChsubscPSP [lemma, in FSSecModel.chsubscIsSecure]
ChsubscPSS [lemma, in FSSecModel.chsubscIsSecure]
ChsubscPSS1 [lemma, in FSSecModel.AuxiliaryLemmas]
chsubsc_SC [definition, in FSSecModel.chsubsc]
Chsubsc_Corr [lemma, in FSSecModel.AuxiliaryLemmas]
Chsubsc.s [variable, in FSSecModel.chsubsc]
Chsubsc.t [variable, in FSSecModel.chsubsc]
Close [constructor, in FSSecModel.SFSstate]
close [inductive, in FSSecModel.close]
Close [section, in FSSecModel.close]
close [library]
closeIsSecure [section, in FSSecModel.closeIsSecure]
closeIsSecure [library]
CloseOK [constructor, in FSSecModel.close]
ClosePCP [lemma, in FSSecModel.closeIsSecure]
ClosePSP [lemma, in FSSecModel.closeIsSecure]
ClosePSS [lemma, in FSSecModel.closeIsSecure]
Close_smCorr3 [lemma, in FSSecModel.AuxiliaryLemmas]
Close_smCorr2 [lemma, in FSSecModel.AuxiliaryLemmas]
Close_smCorr [lemma, in FSSecModel.AuxiliaryLemmas]
close_sm [definition, in FSSecModel.close]
Close.NEWSET [variable, in FSSecModel.close]
Close.s [variable, in FSSecModel.close]
Close.t [variable, in FSSecModel.close]
comp_mode [axiom, in FSSecModel.stat]
ControlProperty [definition, in FSSecModel.ModelProperties]
create [inductive, in FSSecModel.create]
Create [section, in FSSecModel.create]
Create [constructor, in FSSecModel.SFSstate]
create [library]
createIsSecure [section, in FSSecModel.createIsSecure]
createIsSecure [library]
CreateOK [constructor, in FSSecModel.create]
CreatePCP [lemma, in FSSecModel.createIsSecure]
CreatePSP [lemma, in FSSecModel.createIsSecure]
CreatePSS [lemma, in FSSecModel.createIsSecure]
create_acl [definition, in FSSecModel.create]
create_oSC [definition, in FSSecModel.create]
create_directories [axiom, in FSSecModel.SFSstate]
create_files [axiom, in FSSecModel.SFSstate]
Create.ChangeGAR [variable, in FSSecModel.create]
Create.ChangeGAW [variable, in FSSecModel.create]
Create.NEW [variable, in FSSecModel.create]
Create.s [variable, in FSSecModel.create]
Create.t [variable, in FSSecModel.create]
D
DACandMAC [library]DACCtrlAttrHaveChanged [inductive, in FSSecModel.ModelProperties]
DACSecureState [definition, in FSSecModel.ModelProperties]
defaultState [axiom, in FSSecModel.ModelLemmas]
delUsrGrpFromAcl [inductive, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl [section, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl [constructor, in FSSecModel.SFSstate]
delUsrGrpFromAcl [library]
delUsrGrpFromAclIsSecure [section, in FSSecModel.delUsrGrpFromAclIsSecure]
delUsrGrpFromAclIsSecure [library]
delUsrGrpFromAclOK [constructor, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAclPCP [lemma, in FSSecModel.delUsrGrpFromAclIsSecure]
DelUsrGrpFromAclPSP [lemma, in FSSecModel.delUsrGrpFromAclIsSecure]
DelUsrGrpFromAclPSS [lemma, in FSSecModel.delUsrGrpFromAclIsSecure]
delUsrGrpFromAcl_acl [definition, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.NEW [variable, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.NEWOWNER [variable, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.NEW_UO [variable, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.s [variable, in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.t [variable, in FSSecModel.delUsrGrpFromAcl]
DIRCONT [definition, in FSSecModel.SFSstate]
DIRCONTeq_dec [lemma, in FSSecModel.SFSstate]
directories [projection, in FSSecModel.SFSstate]
Directory [constructor, in FSSecModel.SFSstate]
DoAclstat [constructor, in FSSecModel.TransFunc]
DoAddUsrGrpToAcl [constructor, in FSSecModel.TransFunc]
DoChmod [constructor, in FSSecModel.TransFunc]
DoChobjsc [constructor, in FSSecModel.TransFunc]
DoChown [constructor, in FSSecModel.TransFunc]
DoChsubsc [constructor, in FSSecModel.TransFunc]
DoClose [constructor, in FSSecModel.TransFunc]
DoCreate [constructor, in FSSecModel.TransFunc]
DoDelUsrGrpFromAcl [constructor, in FSSecModel.TransFunc]
DOM [definition, in FSSecModel.SFSstate]
domacl [definition, in FSSecModel.SFSstate]
domd [definition, in FSSecModel.SFSstate]
domf [definition, in FSSecModel.SFSstate]
DOMFuncRel [lemma, in FSSecModel.SFSstate]
DOMFuncRel2 [lemma, in FSSecModel.SFSstate]
DOMFuncRel3 [lemma, in FSSecModel.SFSstate]
DOMFuncRel4 [lemma, in FSSecModel.SFSstate]
DoMkdir [constructor, in FSSecModel.TransFunc]
domOSC [definition, in FSSecModel.SFSstate]
domsecmat [definition, in FSSecModel.SFSstate]
domSSC [definition, in FSSecModel.SFSstate]
DoOpen [constructor, in FSSecModel.TransFunc]
DoOscstat [constructor, in FSSecModel.TransFunc]
DoOwner_Close [constructor, in FSSecModel.TransFunc]
DoRead [constructor, in FSSecModel.TransFunc]
DoReaddir [constructor, in FSSecModel.TransFunc]
DoRmdir [constructor, in FSSecModel.TransFunc]
DoSscstat [constructor, in FSSecModel.TransFunc]
DoStat [constructor, in FSSecModel.TransFunc]
DoUnlink [constructor, in FSSecModel.TransFunc]
DoWrite [constructor, in FSSecModel.TransFunc]
E
empty_set [definition, in FSSecModel.ListSet]Eqfacl1 [lemma, in FSSecModel.AuxiliaryLemmas]
Eqfacl2 [lemma, in FSSecModel.AuxiliaryLemmas]
Eqfacl3 [lemma, in FSSecModel.AuxiliaryLemmas]
Eqfacl4 [lemma, in FSSecModel.AuxiliaryLemmas]
Eqfacl5 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfOSC1 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfOSC2 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfOSC3 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfOSC4 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfOSC5 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfOSC6 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfOSC7 [lemma, in FSSecModel.AuxiliaryLemmas]
Eqfsecmat1 [lemma, in FSSecModel.AuxiliaryLemmas]
Eqfsecmat2 [lemma, in FSSecModel.AuxiliaryLemmas]
Eqfsecmat3 [lemma, in FSSecModel.AuxiliaryLemmas]
EqfSSC1 [lemma, in FSSecModel.AuxiliaryLemmas]
eq_scSym [lemma, in FSSecModel.AuxiliaryLemmas]
eq_scIMPLYle_sc [lemma, in FSSecModel.AuxiliaryLemmas]
eq_sc [definition, in FSSecModel.SFSstate]
ExecuterIsOwner [inductive, in FSSecModel.DACandMAC]
F
facl [definition, in FSSecModel.SFSstate]fdirs [definition, in FSSecModel.SFSstate]
ffiles [definition, in FSSecModel.SFSstate]
File [constructor, in FSSecModel.SFSstate]
FILECONT [definition, in FSSecModel.SFSstate]
FILECONTeq_dec [lemma, in FSSecModel.SFSstate]
files [projection, in FSSecModel.SFSstate]
first_definitions.Aeq_dec [variable, in FSSecModel.ListSet]
first_definitions.A [variable, in FSSecModel.ListSet]
first_definitions [section, in FSSecModel.ListSet]
fOSC [definition, in FSSecModel.SFSstate]
front [definition, in FSSecModel.ListFunctions]
fsecmat [definition, in FSSecModel.SFSstate]
fSSC [definition, in FSSecModel.SFSstate]
FuncPre1 [definition, in FSSecModel.ModelProperties]
FuncPre2 [definition, in FSSecModel.ModelProperties]
FuncPre3 [definition, in FSSecModel.ModelProperties]
FuncPre4 [definition, in FSSecModel.ModelProperties]
FuncPre5 [definition, in FSSecModel.ModelProperties]
FuncPre6 [definition, in FSSecModel.ModelProperties]
FuncPre7 [definition, in FSSecModel.ModelProperties]
G
GeneralSecureState [definition, in FSSecModel.ModelLemmas]GO [constructor, in FSSecModel.ModelProperties]
GR [constructor, in FSSecModel.ModelProperties]
Group [constructor, in FSSecModel.ModelProperties]
group [projection, in FSSecModel.SFSstate]
GroupOwners [projection, in FSSecModel.SFSstate]
groupp [projection, in FSSecModel.SFSstate]
GroupReaders [projection, in FSSecModel.SFSstate]
groups [projection, in FSSecModel.SFSstate]
GroupWriters [projection, in FSSecModel.SFSstate]
GRPeq_dec [axiom, in FSSecModel.SFSstate]
GRPNAME [axiom, in FSSecModel.SFSstate]
GW [constructor, in FSSecModel.ModelProperties]
I
Included [definition, in FSSecModel.ListFunctions]InDOMIsNotUndef [lemma, in FSSecModel.SFSstate]
InDOMWhenAdd [lemma, in FSSecModel.SFSstate]
InFileSystem [definition, in FSSecModel.DACandMAC]
InitialState [section, in FSSecModel.InitialState]
InitialState [library]
InitialStateIsSecure [lemma, in FSSecModel.ModelLemmas]
InitState [definition, in FSSecModel.InitialState]
IsEmpty [definition, in FSSecModel.ListFunctions]
IsPARTFUNC [definition, in FSSecModel.SFSstate]
IsUNIXOwner [inductive, in FSSecModel.DACandMAC]
IUO [constructor, in FSSecModel.DACandMAC]
L
last [definition, in FSSecModel.ListFunctions]Level [constructor, in FSSecModel.ModelProperties]
level [projection, in FSSecModel.SFSstate]
le_sc [definition, in FSSecModel.SFSstate]
Listeq_dec [lemma, in FSSecModel.ListFunctions]
ListFunctions [library]
ListSet [library]
ListSetLemmas [section, in FSSecModel.ListFunctions]
ListSetLemmas.A [variable, in FSSecModel.ListFunctions]
ListSetLemmas.Aeq_dec [variable, in FSSecModel.ListFunctions]
M
MACObjCtrlAttrHaveChanged [inductive, in FSSecModel.ModelProperties]MACSecureState [definition, in FSSecModel.ModelProperties]
MACSubCtrlAttrHaveChanged [inductive, in FSSecModel.ModelProperties]
mkdir [inductive, in FSSecModel.mkdir]
Mkdir [section, in FSSecModel.mkdir]
Mkdir [constructor, in FSSecModel.SFSstate]
mkdir [library]
mkdirIsSecure [section, in FSSecModel.mkdirIsSecure]
mkdirIsSecure [library]
MkdirOK [constructor, in FSSecModel.mkdir]
MkdirPCP [lemma, in FSSecModel.mkdirIsSecure]
MkdirPSP [lemma, in FSSecModel.mkdirIsSecure]
MkdirPSS [lemma, in FSSecModel.mkdirIsSecure]
mkdir_acl [definition, in FSSecModel.mkdir]
mkdir_oSC [definition, in FSSecModel.mkdir]
mkdir_directories [axiom, in FSSecModel.SFSstate]
Mkdir.ChangeGAR [variable, in FSSecModel.mkdir]
Mkdir.ChangeGAW [variable, in FSSecModel.mkdir]
Mkdir.NEW [variable, in FSSecModel.mkdir]
Mkdir.s [variable, in FSSecModel.mkdir]
Mkdir.t [variable, in FSSecModel.mkdir]
mkRW [constructor, in FSSecModel.SFSstate]
mkSFS [constructor, in FSSecModel.SFSstate]
MODE [inductive, in FSSecModel.SFSstate]
ModelLemmas [library]
ModelProperties [section, in FSSecModel.ModelProperties]
ModelProperties [library]
MyDir [axiom, in FSSecModel.SFSstate]
N
NEWDIR [definition, in FSSecModel.mkdir]NEWFILE [definition, in FSSecModel.create]
NEWRW [definition, in FSSecModel.close]
NEWRWOC [definition, in FSSecModel.owner_close]
NoDACChange [lemma, in FSSecModel.AuxiliaryLemmas]
NoDACChange2 [lemma, in FSSecModel.AuxiliaryLemmas]
NoMACObjChange [lemma, in FSSecModel.AuxiliaryLemmas]
NoMACObjChange2 [lemma, in FSSecModel.AuxiliaryLemmas]
NoMACSubChange [lemma, in FSSecModel.AuxiliaryLemmas]
NoMACSubChange2 [lemma, in FSSecModel.AuxiliaryLemmas]
NotInDOMIsUndef [lemma, in FSSecModel.SFSstate]
NotInDOMIsUndef2 [lemma, in FSSecModel.AuxiliaryLemmas]
NotInDOMIsUndef3 [lemma, in FSSecModel.AuxiliaryLemmas]
O
OBJDeq_dec [axiom, in FSSecModel.SFSstate]OBJECT [definition, in FSSecModel.SFSstate]
objectSC [projection, in FSSecModel.SFSstate]
OBJeq_dec [lemma, in FSSecModel.SFSstate]
OBJFeq_dec [axiom, in FSSecModel.SFSstate]
ObjName [definition, in FSSecModel.SFSstate]
OBJNAME [axiom, in FSSecModel.SFSstate]
OBJNAMEeq_dec [axiom, in FSSecModel.SFSstate]
ObjType [definition, in FSSecModel.SFSstate]
OBJTYPE [inductive, in FSSecModel.SFSstate]
OBJTYPEeq_dec [lemma, in FSSecModel.SFSstate]
open [inductive, in FSSecModel.open]
Open [section, in FSSecModel.open]
Open [constructor, in FSSecModel.SFSstate]
open [library]
openIsSecure [section, in FSSecModel.openIsSecure]
openIsSecure [library]
OpenPCP [lemma, in FSSecModel.openIsSecure]
OpenPSP [lemma, in FSSecModel.openIsSecure]
OpenPSS [lemma, in FSSecModel.openIsSecure]
OpenRead [constructor, in FSSecModel.open]
OpenWrite [constructor, in FSSecModel.open]
Open_smCorr32 [lemma, in FSSecModel.AuxiliaryLemmas]
Open_smCorr31 [lemma, in FSSecModel.AuxiliaryLemmas]
Open_smCorr22 [lemma, in FSSecModel.AuxiliaryLemmas]
Open_smCorr21 [lemma, in FSSecModel.AuxiliaryLemmas]
Open_smCorr3 [lemma, in FSSecModel.AuxiliaryLemmas]
open_sm [definition, in FSSecModel.open]
Open.s [variable, in FSSecModel.open]
Open.t [variable, in FSSecModel.open]
Operation [inductive, in FSSecModel.SFSstate]
OSCeq_dec [axiom, in FSSecModel.SFSstate]
oscstat [inductive, in FSSecModel.oscstat]
Oscstat [section, in FSSecModel.oscstat]
Oscstat [constructor, in FSSecModel.SFSstate]
oscstat [library]
oscstatIsSecure [section, in FSSecModel.oscstatIsSecure]
oscstatIsSecure [library]
OscstatOK [constructor, in FSSecModel.oscstat]
OscstatPCP [lemma, in FSSecModel.oscstatIsSecure]
OscstatPSP [lemma, in FSSecModel.oscstatIsSecure]
OscstatPSS [lemma, in FSSecModel.oscstatIsSecure]
Oscstat.s [variable, in FSSecModel.oscstat]
otherp [projection, in FSSecModel.SFSstate]
other_definitions.B [variable, in FSSecModel.ListSet]
other_definitions.A [variable, in FSSecModel.ListSet]
other_definitions [section, in FSSecModel.ListSet]
Owner [constructor, in FSSecModel.ModelProperties]
owner [projection, in FSSecModel.SFSstate]
OwnerClose_smCorr3 [lemma, in FSSecModel.AuxiliaryLemmas]
OwnerClose_smCorr2 [lemma, in FSSecModel.AuxiliaryLemmas]
ownerclose_sm [definition, in FSSecModel.owner_close]
ownerp [projection, in FSSecModel.SFSstate]
Owner_Close [constructor, in FSSecModel.SFSstate]
Owner_ClosePCP [lemma, in FSSecModel.owner_closeIsSecure]
Owner_ClosePSP [lemma, in FSSecModel.owner_closeIsSecure]
Owner_ClosePSS [lemma, in FSSecModel.owner_closeIsSecure]
owner_closeIsSecure [section, in FSSecModel.owner_closeIsSecure]
Owner_CloseOK [constructor, in FSSecModel.owner_close]
owner_close [inductive, in FSSecModel.owner_close]
Owner_Close.t [variable, in FSSecModel.owner_close]
Owner_Close.NEWSET [variable, in FSSecModel.owner_close]
Owner_Close.s [variable, in FSSecModel.owner_close]
Owner_Close [section, in FSSecModel.owner_close]
owner_closeIsSecure [library]
owner_close [library]
P
PARTFUNC [definition, in FSSecModel.SFSstate]PartialFunctions [section, in FSSecModel.SFSstate]
PartialFunctions.X [variable, in FSSecModel.SFSstate]
PartialFunctions.Xeq_dec [variable, in FSSecModel.SFSstate]
PartialFunctions.XYeq_dec [variable, in FSSecModel.SFSstate]
PartialFunctions.Y [variable, in FSSecModel.SFSstate]
PartialFunctions.Yeq_dec [variable, in FSSecModel.SFSstate]
PERMS [record, in FSSecModel.SFSstate]
Preconditions [section, in FSSecModel.DACandMAC]
Preconditions.s [variable, in FSSecModel.DACandMAC]
PreDACRead [definition, in FSSecModel.DACandMAC]
PreDACWrite [definition, in FSSecModel.DACandMAC]
PreMAC [definition, in FSSecModel.DACandMAC]
PreservesControlProp [definition, in FSSecModel.ModelProperties]
PreStarPropRead [definition, in FSSecModel.DACandMAC]
PreStarPropWrite [definition, in FSSecModel.DACandMAC]
primaryGrp [projection, in FSSecModel.SFSstate]
Prodeq_dec [lemma, in FSSecModel.ListFunctions]
R
RAN [definition, in FSSecModel.SFSstate]ransecmat [definition, in FSSecModel.SFSstate]
read [inductive, in FSSecModel.read]
Read [section, in FSSecModel.read]
Read [constructor, in FSSecModel.SFSstate]
READ [constructor, in FSSecModel.SFSstate]
read [library]
readdir [inductive, in FSSecModel.readdir]
Readdir [section, in FSSecModel.readdir]
Readdir [constructor, in FSSecModel.SFSstate]
readdir [library]
readdirIsSecure [section, in FSSecModel.readdirIsSecure]
readdirIsSecure [library]
ReaddirOK [constructor, in FSSecModel.readdir]
ReaddirPCP [lemma, in FSSecModel.readdirIsSecure]
ReaddirPSP [lemma, in FSSecModel.readdirIsSecure]
ReaddirPSS [lemma, in FSSecModel.readdirIsSecure]
Readdir.s [variable, in FSSecModel.readdir]
ReadersWriters [record, in FSSecModel.SFSstate]
readIsSecure [section, in FSSecModel.readIsSecure]
readIsSecure [library]
ReadOK [constructor, in FSSecModel.read]
ReadPCP [lemma, in FSSecModel.readIsSecure]
ReadPSP [lemma, in FSSecModel.readIsSecure]
ReadPSS [lemma, in FSSecModel.readIsSecure]
ReadWriteImpRead [lemma, in FSSecModel.AuxiliaryLemmas]
ReadWriteImpWrite [lemma, in FSSecModel.AuxiliaryLemmas]
read_right [projection, in FSSecModel.SFSstate]
Read.s [variable, in FSSecModel.read]
RemEq [lemma, in FSSecModel.SFSstate]
RIGHTS [record, in FSSecModel.SFSstate]
Rmdir [constructor, in FSSecModel.SFSstate]
rmdir [inductive, in FSSecModel.rmdir]
Rmdir [section, in FSSecModel.rmdir]
rmdir [library]
rmdirIsSecure [section, in FSSecModel.rmdirIsSecure]
rmdirIsSecure [library]
RmdirOK [constructor, in FSSecModel.rmdir]
RmdirPCP [lemma, in FSSecModel.rmdirIsSecure]
RmdirPSP [lemma, in FSSecModel.rmdirIsSecure]
RmdirPSS [lemma, in FSSecModel.rmdirIsSecure]
rmdir_directories [axiom, in FSSecModel.SFSstate]
rmdir_acl [definition, in FSSecModel.rmdir]
rmdir_oSC [definition, in FSSecModel.rmdir]
Rmdir.s [variable, in FSSecModel.rmdir]
Rmdir.t [variable, in FSSecModel.rmdir]
root [axiom, in FSSecModel.SFSstate]
RootBelongsToAllGrp [axiom, in FSSecModel.InitialState]
RootBelongsToRootGrp [axiom, in FSSecModel.InitialState]
RootGrp [projection, in FSSecModel.SFSstate]
RWeq_dec [axiom, in FSSecModel.SFSstate]
rwx [constructor, in FSSecModel.SFSstate]
S
sclass [constructor, in FSSecModel.SFSstate]SCo [constructor, in FSSecModel.ModelProperties]
SCu [constructor, in FSSecModel.ModelProperties]
SecAdmGrp [projection, in FSSecModel.SFSstate]
SecClass [record, in FSSecModel.SFSstate]
SecClassChanged [inductive, in FSSecModel.ModelProperties]
SECLEV [definition, in FSSecModel.SFSstate]
secmat [projection, in FSSecModel.SFSstate]
SECMATeq_dec [axiom, in FSSecModel.SFSstate]
secofr [axiom, in FSSecModel.SFSstate]
SecofrBelongsToAllGrp [axiom, in FSSecModel.InitialState]
SecofrBelongsToSecAdmGrp [axiom, in FSSecModel.InitialState]
SecureState [definition, in FSSecModel.ModelProperties]
set [definition, in FSSecModel.ListSet]
setACLdata [section, in FSSecModel.setACLdata]
setACLdata [library]
setACLdata.s [variable, in FSSecModel.setACLdata]
set_fold_right [definition, in FSSecModel.ListSet]
set_fold_left [definition, in FSSecModel.ListSet]
set_map [definition, in FSSecModel.ListSet]
set_power [definition, in FSSecModel.ListSet]
set_prod [definition, in FSSecModel.ListSet]
set_diff_elim1 [lemma, in FSSecModel.ListSet]
set_diff_intro [lemma, in FSSecModel.ListSet]
set_inter_elim [lemma, in FSSecModel.ListSet]
set_inter_elim2 [lemma, in FSSecModel.ListSet]
set_inter_elim1 [lemma, in FSSecModel.ListSet]
set_inter_intro [lemma, in FSSecModel.ListSet]
set_union_elim [lemma, in FSSecModel.ListSet]
set_union_intro [lemma, in FSSecModel.ListSet]
set_union_intro2 [lemma, in FSSecModel.ListSet]
set_union_intro1 [lemma, in FSSecModel.ListSet]
set_add_not_empty [lemma, in FSSecModel.ListSet]
set_add_elim [lemma, in FSSecModel.ListSet]
set_add_intro [lemma, in FSSecModel.ListSet]
set_add_intro2 [lemma, in FSSecModel.ListSet]
set_add_intro1 [lemma, in FSSecModel.ListSet]
set_mem_complete2 [lemma, in FSSecModel.ListSet]
set_mem_complete1 [lemma, in FSSecModel.ListSet]
set_mem_correct2 [lemma, in FSSecModel.ListSet]
set_mem_correct1 [lemma, in FSSecModel.ListSet]
set_mem_ind [lemma, in FSSecModel.ListSet]
set_In_dec [lemma, in FSSecModel.ListSet]
Set_remove1 [lemma, in FSSecModel.ListSet]
set_In [definition, in FSSecModel.ListSet]
set_diff [definition, in FSSecModel.ListSet]
set_union [definition, in FSSecModel.ListSet]
set_inter [definition, in FSSecModel.ListSet]
set_remove [definition, in FSSecModel.ListSet]
set_mem [definition, in FSSecModel.ListSet]
set_add [definition, in FSSecModel.ListSet]
Set_add2 [lemma, in FSSecModel.ListFunctions]
Set_add1 [lemma, in FSSecModel.ListFunctions]
Set_remove2 [lemma, in FSSecModel.ListFunctions]
Set_union2 [lemma, in FSSecModel.ListFunctions]
Set_union1 [lemma, in FSSecModel.ListFunctions]
SFSstate [record, in FSSecModel.SFSstate]
SFSstate [library]
SSCeq_dec [axiom, in FSSecModel.SFSstate]
sscstat [inductive, in FSSecModel.sscstat]
Sscstat [section, in FSSecModel.sscstat]
Sscstat [constructor, in FSSecModel.SFSstate]
sscstat [library]
sscstatIsSecure [section, in FSSecModel.sscstatIsSecure]
sscstatIsSecure [library]
SscstatOK [constructor, in FSSecModel.sscstat]
SscstatPCP [lemma, in FSSecModel.sscstatIsSecure]
SscstatPSP [lemma, in FSSecModel.sscstatIsSecure]
SscstatPSS [lemma, in FSSecModel.sscstatIsSecure]
Sscstat.s [variable, in FSSecModel.sscstat]
StarProperty [definition, in FSSecModel.ModelProperties]
stat [inductive, in FSSecModel.stat]
Stat [section, in FSSecModel.stat]
Stat [constructor, in FSSecModel.SFSstate]
stat [library]
statIsSecure [section, in FSSecModel.statIsSecure]
statIsSecure [library]
StatOK [constructor, in FSSecModel.stat]
StatPCP [lemma, in FSSecModel.statIsSecure]
StatPSP [lemma, in FSSecModel.statIsSecure]
StatPSS [lemma, in FSSecModel.statIsSecure]
stat_struct [record, in FSSecModel.stat]
stat_fields [constructor, in FSSecModel.stat]
Stat.s [variable, in FSSecModel.stat]
st_gid [projection, in FSSecModel.stat]
st_uid [projection, in FSSecModel.stat]
st_mode [projection, in FSSecModel.stat]
SUBeq_dec [axiom, in FSSecModel.SFSstate]
SUBJECT [axiom, in FSSecModel.SFSstate]
subjectSC [projection, in FSSecModel.SFSstate]
SysAllGrp [axiom, in FSSecModel.InitialState]
SysGroups [axiom, in FSSecModel.InitialState]
SysPrimaryGrp [axiom, in FSSecModel.InitialState]
SysRootGrp [axiom, in FSSecModel.InitialState]
SysSecAdmGrp [axiom, in FSSecModel.InitialState]
SysSubjectSC [axiom, in FSSecModel.InitialState]
SysSubjectSCIsPARTFUNC [axiom, in FSSecModel.InitialState]
T
take [definition, in FSSecModel.ListFunctions]TransFunc [inductive, in FSSecModel.TransFunc]
TransFunc [library]
TransitionFunction [section, in FSSecModel.TransFunc]
TwoImpLeft [lemma, in FSSecModel.AuxiliaryLemmas]
TwoImpRight [lemma, in FSSecModel.AuxiliaryLemmas]
U
UndefWhenRem [lemma, in FSSecModel.SFSstate]UniqNames [lemma, in FSSecModel.AuxiliaryLemmas]
UNIX [constructor, in FSSecModel.ModelProperties]
UNIXAttrChanged [inductive, in FSSecModel.ModelProperties]
UNIXOwner [constructor, in FSSecModel.DACandMAC]
unlink [inductive, in FSSecModel.unlink]
Unlink [section, in FSSecModel.unlink]
Unlink [constructor, in FSSecModel.SFSstate]
unlink [library]
unlinkIsSecure [section, in FSSecModel.unlinkIsSecure]
unlinkIsSecure [library]
UnlinkOK [constructor, in FSSecModel.unlink]
UnlinkPCP [lemma, in FSSecModel.unlinkIsSecure]
UnlinkPSP [lemma, in FSSecModel.unlinkIsSecure]
UnlinkPSS [lemma, in FSSecModel.unlinkIsSecure]
unlink_acl [definition, in FSSecModel.unlink]
unlink_oSC [definition, in FSSecModel.unlink]
unlink_directories [axiom, in FSSecModel.SFSstate]
unlink_files [axiom, in FSSecModel.SFSstate]
Unlink.s [variable, in FSSecModel.unlink]
Unlink.t [variable, in FSSecModel.unlink]
UO [constructor, in FSSecModel.ModelProperties]
UR [constructor, in FSSecModel.ModelProperties]
UsersOwners [projection, in FSSecModel.SFSstate]
UsersReaders [projection, in FSSecModel.SFSstate]
UsersWriters [projection, in FSSecModel.SFSstate]
UW [constructor, in FSSecModel.ModelProperties]
W
WFSI1 [axiom, in FSSecModel.ModelProperties]WFSI2 [axiom, in FSSecModel.ModelProperties]
WFSI3 [axiom, in FSSecModel.ModelProperties]
WFSI4 [axiom, in FSSecModel.ModelProperties]
WFSI5 [axiom, in FSSecModel.ModelProperties]
WFSI6 [axiom, in FSSecModel.ModelProperties]
WFSI7 [axiom, in FSSecModel.ModelProperties]
WFSI8 [axiom, in FSSecModel.ModelProperties]
WFSI9 [axiom, in FSSecModel.ModelProperties]
write [inductive, in FSSecModel.write]
Write [section, in FSSecModel.write]
Write [constructor, in FSSecModel.SFSstate]
WRITE [constructor, in FSSecModel.SFSstate]
write [library]
writeIsSecure [section, in FSSecModel.writeIsSecure]
writeIsSecure [library]
WriteOK [constructor, in FSSecModel.write]
WritePCP [lemma, in FSSecModel.writeIsSecure]
WritePSP [lemma, in FSSecModel.writeIsSecure]
WritePSS [lemma, in FSSecModel.writeIsSecure]
write_files [axiom, in FSSecModel.SFSstate]
write_right [projection, in FSSecModel.SFSstate]
Write.s [variable, in FSSecModel.write]
Write.t [variable, in FSSecModel.write]
Variable Index
A
Aclstat.s [in FSSecModel.aclstat]AddUsrGrpToAcl.NEW [in FSSecModel.addUsrGrpToAcl]
AddUsrGrpToAcl.s [in FSSecModel.addUsrGrpToAcl]
AddUsrGrpToAcl.t [in FSSecModel.addUsrGrpToAcl]
C
Chmod.ChangeGAR [in FSSecModel.chmod]Chmod.ChangeGAW [in FSSecModel.chmod]
Chmod.NEW [in FSSecModel.chmod]
Chmod.s [in FSSecModel.chmod]
Chmod.t [in FSSecModel.chmod]
Chobjsc.s [in FSSecModel.chobjsc]
Chobjsc.t [in FSSecModel.chobjsc]
Chown.NEW [in FSSecModel.chown]
Chown.NEW_UO [in FSSecModel.chown]
Chown.NEW_GRP [in FSSecModel.chown]
Chown.s [in FSSecModel.chown]
Chown.t [in FSSecModel.chown]
Chsubsc.s [in FSSecModel.chsubsc]
Chsubsc.t [in FSSecModel.chsubsc]
Close.NEWSET [in FSSecModel.close]
Close.s [in FSSecModel.close]
Close.t [in FSSecModel.close]
Create.ChangeGAR [in FSSecModel.create]
Create.ChangeGAW [in FSSecModel.create]
Create.NEW [in FSSecModel.create]
Create.s [in FSSecModel.create]
Create.t [in FSSecModel.create]
D
DelUsrGrpFromAcl.NEW [in FSSecModel.delUsrGrpFromAcl]DelUsrGrpFromAcl.NEWOWNER [in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.NEW_UO [in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.s [in FSSecModel.delUsrGrpFromAcl]
DelUsrGrpFromAcl.t [in FSSecModel.delUsrGrpFromAcl]
F
first_definitions.Aeq_dec [in FSSecModel.ListSet]first_definitions.A [in FSSecModel.ListSet]
L
ListSetLemmas.A [in FSSecModel.ListFunctions]ListSetLemmas.Aeq_dec [in FSSecModel.ListFunctions]
M
Mkdir.ChangeGAR [in FSSecModel.mkdir]Mkdir.ChangeGAW [in FSSecModel.mkdir]
Mkdir.NEW [in FSSecModel.mkdir]
Mkdir.s [in FSSecModel.mkdir]
Mkdir.t [in FSSecModel.mkdir]
O
Open.s [in FSSecModel.open]Open.t [in FSSecModel.open]
Oscstat.s [in FSSecModel.oscstat]
other_definitions.B [in FSSecModel.ListSet]
other_definitions.A [in FSSecModel.ListSet]
Owner_Close.t [in FSSecModel.owner_close]
Owner_Close.NEWSET [in FSSecModel.owner_close]
Owner_Close.s [in FSSecModel.owner_close]
P
PartialFunctions.X [in FSSecModel.SFSstate]PartialFunctions.Xeq_dec [in FSSecModel.SFSstate]
PartialFunctions.XYeq_dec [in FSSecModel.SFSstate]
PartialFunctions.Y [in FSSecModel.SFSstate]
PartialFunctions.Yeq_dec [in FSSecModel.SFSstate]
Preconditions.s [in FSSecModel.DACandMAC]
R
Readdir.s [in FSSecModel.readdir]Read.s [in FSSecModel.read]
Rmdir.s [in FSSecModel.rmdir]
Rmdir.t [in FSSecModel.rmdir]
S
setACLdata.s [in FSSecModel.setACLdata]Sscstat.s [in FSSecModel.sscstat]
Stat.s [in FSSecModel.stat]
U
Unlink.s [in FSSecModel.unlink]Unlink.t [in FSSecModel.unlink]
W
Write.s [in FSSecModel.write]Write.t [in FSSecModel.write]
Library Index
A
aclstataclstatIsSecure
addUsrGrpToAcl
addUsrGrpToAclIsSecure
AuxiliaryLemmas
C
chmodchmodIsSecure
chobjsc
chobjscIsSecure
chown
chownIsSecure
chsubsc
chsubscIsSecure
close
closeIsSecure
create
createIsSecure
D
DACandMACdelUsrGrpFromAcl
delUsrGrpFromAclIsSecure
I
InitialStateL
ListFunctionsListSet
M
mkdirmkdirIsSecure
ModelLemmas
ModelProperties
O
openopenIsSecure
oscstat
oscstatIsSecure
owner_closeIsSecure
owner_close
R
readreaddir
readdirIsSecure
readIsSecure
rmdir
rmdirIsSecure
S
setACLdataSFSstate
sscstat
sscstatIsSecure
stat
statIsSecure
T
TransFuncU
unlinkunlinkIsSecure
W
writewriteIsSecure
Constructor Index
A
ACL [in FSSecModel.ModelProperties]acldata [in FSSecModel.SFSstate]
ACLGrp [in FSSecModel.DACandMAC]
ACLOwner [in FSSecModel.DACandMAC]
Aclstat [in FSSecModel.SFSstate]
AclstatOK [in FSSecModel.aclstat]
AddUsrGrpToAcl [in FSSecModel.SFSstate]
addUsrGrpToAclOK [in FSSecModel.addUsrGrpToAcl]
allowedTo [in FSSecModel.SFSstate]
C
Categ [in FSSecModel.ModelProperties]Chmod [in FSSecModel.SFSstate]
ChmodOK [in FSSecModel.chmod]
Chobjsc [in FSSecModel.SFSstate]
Chown [in FSSecModel.SFSstate]
ChownOK [in FSSecModel.chown]
chsobjscOK [in FSSecModel.chobjsc]
Chsubsc [in FSSecModel.SFSstate]
chsubscOK [in FSSecModel.chsubsc]
Close [in FSSecModel.SFSstate]
CloseOK [in FSSecModel.close]
Create [in FSSecModel.SFSstate]
CreateOK [in FSSecModel.create]
D
DelUsrGrpFromAcl [in FSSecModel.SFSstate]delUsrGrpFromAclOK [in FSSecModel.delUsrGrpFromAcl]
Directory [in FSSecModel.SFSstate]
DoAclstat [in FSSecModel.TransFunc]
DoAddUsrGrpToAcl [in FSSecModel.TransFunc]
DoChmod [in FSSecModel.TransFunc]
DoChobjsc [in FSSecModel.TransFunc]
DoChown [in FSSecModel.TransFunc]
DoChsubsc [in FSSecModel.TransFunc]
DoClose [in FSSecModel.TransFunc]
DoCreate [in FSSecModel.TransFunc]
DoDelUsrGrpFromAcl [in FSSecModel.TransFunc]
DoMkdir [in FSSecModel.TransFunc]
DoOpen [in FSSecModel.TransFunc]
DoOscstat [in FSSecModel.TransFunc]
DoOwner_Close [in FSSecModel.TransFunc]
DoRead [in FSSecModel.TransFunc]
DoReaddir [in FSSecModel.TransFunc]
DoRmdir [in FSSecModel.TransFunc]
DoSscstat [in FSSecModel.TransFunc]
DoStat [in FSSecModel.TransFunc]
DoUnlink [in FSSecModel.TransFunc]
DoWrite [in FSSecModel.TransFunc]
F
File [in FSSecModel.SFSstate]G
GO [in FSSecModel.ModelProperties]GR [in FSSecModel.ModelProperties]
Group [in FSSecModel.ModelProperties]
GW [in FSSecModel.ModelProperties]
I
IUO [in FSSecModel.DACandMAC]L
Level [in FSSecModel.ModelProperties]M
Mkdir [in FSSecModel.SFSstate]MkdirOK [in FSSecModel.mkdir]
mkRW [in FSSecModel.SFSstate]
mkSFS [in FSSecModel.SFSstate]
O
Open [in FSSecModel.SFSstate]OpenRead [in FSSecModel.open]
OpenWrite [in FSSecModel.open]
Oscstat [in FSSecModel.SFSstate]
OscstatOK [in FSSecModel.oscstat]
Owner [in FSSecModel.ModelProperties]
Owner_Close [in FSSecModel.SFSstate]
Owner_CloseOK [in FSSecModel.owner_close]
R
Read [in FSSecModel.SFSstate]READ [in FSSecModel.SFSstate]
Readdir [in FSSecModel.SFSstate]
ReaddirOK [in FSSecModel.readdir]
ReadOK [in FSSecModel.read]
Rmdir [in FSSecModel.SFSstate]
RmdirOK [in FSSecModel.rmdir]
rwx [in FSSecModel.SFSstate]
S
sclass [in FSSecModel.SFSstate]SCo [in FSSecModel.ModelProperties]
SCu [in FSSecModel.ModelProperties]
Sscstat [in FSSecModel.SFSstate]
SscstatOK [in FSSecModel.sscstat]
Stat [in FSSecModel.SFSstate]
StatOK [in FSSecModel.stat]
stat_fields [in FSSecModel.stat]
U
UNIX [in FSSecModel.ModelProperties]UNIXOwner [in FSSecModel.DACandMAC]
Unlink [in FSSecModel.SFSstate]
UnlinkOK [in FSSecModel.unlink]
UO [in FSSecModel.ModelProperties]
UR [in FSSecModel.ModelProperties]
UW [in FSSecModel.ModelProperties]
W
Write [in FSSecModel.SFSstate]WRITE [in FSSecModel.SFSstate]
WriteOK [in FSSecModel.write]
Lemma Index
A
AclstatPCP [in FSSecModel.aclstatIsSecure]AclstatPSP [in FSSecModel.aclstatIsSecure]
AclstatPSS [in FSSecModel.aclstatIsSecure]
AddEq [in FSSecModel.SFSstate]
AddEq1 [in FSSecModel.SFSstate]
AddRemEq [in FSSecModel.SFSstate]
AddUsrGrpToAclPCP [in FSSecModel.addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSP [in FSSecModel.addUsrGrpToAclIsSecure]
AddUsrGrpToAclPSS [in FSSecModel.addUsrGrpToAclIsSecure]
AllWaysIncluded [in FSSecModel.ListFunctions]
Aux1 [in FSSecModel.AuxiliaryLemmas]
B
BasicSecurityTheorem [in FSSecModel.ModelLemmas]C
ChmodPCP [in FSSecModel.chmodIsSecure]ChmodPSP [in FSSecModel.chmodIsSecure]
ChmodPSS [in FSSecModel.chmodIsSecure]
ChobjscPCP [in FSSecModel.chobjscIsSecure]
ChobjscPSP [in FSSecModel.chobjscIsSecure]
ChobjscPSS [in FSSecModel.chobjscIsSecure]
Chobjsc_Corr [in FSSecModel.AuxiliaryLemmas]
ChownPCP [in FSSecModel.chownIsSecure]
ChownPSP [in FSSecModel.chownIsSecure]
ChownPSS [in FSSecModel.chownIsSecure]
ChsubscPCP [in FSSecModel.chsubscIsSecure]
ChsubscPSP [in FSSecModel.chsubscIsSecure]
ChsubscPSS [in FSSecModel.chsubscIsSecure]
ChsubscPSS1 [in FSSecModel.AuxiliaryLemmas]
Chsubsc_Corr [in FSSecModel.AuxiliaryLemmas]
ClosePCP [in FSSecModel.closeIsSecure]
ClosePSP [in FSSecModel.closeIsSecure]
ClosePSS [in FSSecModel.closeIsSecure]
Close_smCorr3 [in FSSecModel.AuxiliaryLemmas]
Close_smCorr2 [in FSSecModel.AuxiliaryLemmas]
Close_smCorr [in FSSecModel.AuxiliaryLemmas]
CreatePCP [in FSSecModel.createIsSecure]
CreatePSP [in FSSecModel.createIsSecure]
CreatePSS [in FSSecModel.createIsSecure]
D
DelUsrGrpFromAclPCP [in FSSecModel.delUsrGrpFromAclIsSecure]DelUsrGrpFromAclPSP [in FSSecModel.delUsrGrpFromAclIsSecure]
DelUsrGrpFromAclPSS [in FSSecModel.delUsrGrpFromAclIsSecure]
DIRCONTeq_dec [in FSSecModel.SFSstate]
DOMFuncRel [in FSSecModel.SFSstate]
DOMFuncRel2 [in FSSecModel.SFSstate]
DOMFuncRel3 [in FSSecModel.SFSstate]
DOMFuncRel4 [in FSSecModel.SFSstate]
E
Eqfacl1 [in FSSecModel.AuxiliaryLemmas]Eqfacl2 [in FSSecModel.AuxiliaryLemmas]
Eqfacl3 [in FSSecModel.AuxiliaryLemmas]
Eqfacl4 [in FSSecModel.AuxiliaryLemmas]
Eqfacl5 [in FSSecModel.AuxiliaryLemmas]
EqfOSC1 [in FSSecModel.AuxiliaryLemmas]
EqfOSC2 [in FSSecModel.AuxiliaryLemmas]
EqfOSC3 [in FSSecModel.AuxiliaryLemmas]
EqfOSC4 [in FSSecModel.AuxiliaryLemmas]
EqfOSC5 [in FSSecModel.AuxiliaryLemmas]
EqfOSC6 [in FSSecModel.AuxiliaryLemmas]
EqfOSC7 [in FSSecModel.AuxiliaryLemmas]
Eqfsecmat1 [in FSSecModel.AuxiliaryLemmas]
Eqfsecmat2 [in FSSecModel.AuxiliaryLemmas]
Eqfsecmat3 [in FSSecModel.AuxiliaryLemmas]
EqfSSC1 [in FSSecModel.AuxiliaryLemmas]
eq_scSym [in FSSecModel.AuxiliaryLemmas]
eq_scIMPLYle_sc [in FSSecModel.AuxiliaryLemmas]
F
FILECONTeq_dec [in FSSecModel.SFSstate]I
InDOMIsNotUndef [in FSSecModel.SFSstate]InDOMWhenAdd [in FSSecModel.SFSstate]
InitialStateIsSecure [in FSSecModel.ModelLemmas]
L
Listeq_dec [in FSSecModel.ListFunctions]M
MkdirPCP [in FSSecModel.mkdirIsSecure]MkdirPSP [in FSSecModel.mkdirIsSecure]
MkdirPSS [in FSSecModel.mkdirIsSecure]
N
NoDACChange [in FSSecModel.AuxiliaryLemmas]NoDACChange2 [in FSSecModel.AuxiliaryLemmas]
NoMACObjChange [in FSSecModel.AuxiliaryLemmas]
NoMACObjChange2 [in FSSecModel.AuxiliaryLemmas]
NoMACSubChange [in FSSecModel.AuxiliaryLemmas]
NoMACSubChange2 [in FSSecModel.AuxiliaryLemmas]
NotInDOMIsUndef [in FSSecModel.SFSstate]
NotInDOMIsUndef2 [in FSSecModel.AuxiliaryLemmas]
NotInDOMIsUndef3 [in FSSecModel.AuxiliaryLemmas]
O
OBJeq_dec [in FSSecModel.SFSstate]OBJTYPEeq_dec [in FSSecModel.SFSstate]
OpenPCP [in FSSecModel.openIsSecure]
OpenPSP [in FSSecModel.openIsSecure]
OpenPSS [in FSSecModel.openIsSecure]
Open_smCorr32 [in FSSecModel.AuxiliaryLemmas]
Open_smCorr31 [in FSSecModel.AuxiliaryLemmas]
Open_smCorr22 [in FSSecModel.AuxiliaryLemmas]
Open_smCorr21 [in FSSecModel.AuxiliaryLemmas]
Open_smCorr3 [in FSSecModel.AuxiliaryLemmas]
OscstatPCP [in FSSecModel.oscstatIsSecure]
OscstatPSP [in FSSecModel.oscstatIsSecure]
OscstatPSS [in FSSecModel.oscstatIsSecure]
OwnerClose_smCorr3 [in FSSecModel.AuxiliaryLemmas]
OwnerClose_smCorr2 [in FSSecModel.AuxiliaryLemmas]
Owner_ClosePCP [in FSSecModel.owner_closeIsSecure]
Owner_ClosePSP [in FSSecModel.owner_closeIsSecure]
Owner_ClosePSS [in FSSecModel.owner_closeIsSecure]
P
Prodeq_dec [in FSSecModel.ListFunctions]R
ReaddirPCP [in FSSecModel.readdirIsSecure]ReaddirPSP [in FSSecModel.readdirIsSecure]
ReaddirPSS [in FSSecModel.readdirIsSecure]
ReadPCP [in FSSecModel.readIsSecure]
ReadPSP [in FSSecModel.readIsSecure]
ReadPSS [in FSSecModel.readIsSecure]
ReadWriteImpRead [in FSSecModel.AuxiliaryLemmas]
ReadWriteImpWrite [in FSSecModel.AuxiliaryLemmas]
RemEq [in FSSecModel.SFSstate]
RmdirPCP [in FSSecModel.rmdirIsSecure]
RmdirPSP [in FSSecModel.rmdirIsSecure]
RmdirPSS [in FSSecModel.rmdirIsSecure]
S
set_diff_elim1 [in FSSecModel.ListSet]set_diff_intro [in FSSecModel.ListSet]
set_inter_elim [in FSSecModel.ListSet]
set_inter_elim2 [in FSSecModel.ListSet]
set_inter_elim1 [in FSSecModel.ListSet]
set_inter_intro [in FSSecModel.ListSet]
set_union_elim [in FSSecModel.ListSet]
set_union_intro [in FSSecModel.ListSet]
set_union_intro2 [in FSSecModel.ListSet]
set_union_intro1 [in FSSecModel.ListSet]
set_add_not_empty [in FSSecModel.ListSet]
set_add_elim [in FSSecModel.ListSet]
set_add_intro [in FSSecModel.ListSet]
set_add_intro2 [in FSSecModel.ListSet]
set_add_intro1 [in FSSecModel.ListSet]
set_mem_complete2 [in FSSecModel.ListSet]
set_mem_complete1 [in FSSecModel.ListSet]
set_mem_correct2 [in FSSecModel.ListSet]
set_mem_correct1 [in FSSecModel.ListSet]
set_mem_ind [in FSSecModel.ListSet]
set_In_dec [in FSSecModel.ListSet]
Set_remove1 [in FSSecModel.ListSet]
Set_add2 [in FSSecModel.ListFunctions]
Set_add1 [in FSSecModel.ListFunctions]
Set_remove2 [in FSSecModel.ListFunctions]
Set_union2 [in FSSecModel.ListFunctions]
Set_union1 [in FSSecModel.ListFunctions]
SscstatPCP [in FSSecModel.sscstatIsSecure]
SscstatPSP [in FSSecModel.sscstatIsSecure]
SscstatPSS [in FSSecModel.sscstatIsSecure]
StatPCP [in FSSecModel.statIsSecure]
StatPSP [in FSSecModel.statIsSecure]
StatPSS [in FSSecModel.statIsSecure]
T
TwoImpLeft [in FSSecModel.AuxiliaryLemmas]TwoImpRight [in FSSecModel.AuxiliaryLemmas]
U
UndefWhenRem [in FSSecModel.SFSstate]UniqNames [in FSSecModel.AuxiliaryLemmas]
UnlinkPCP [in FSSecModel.unlinkIsSecure]
UnlinkPSP [in FSSecModel.unlinkIsSecure]
UnlinkPSS [in FSSecModel.unlinkIsSecure]
W
WritePCP [in FSSecModel.writeIsSecure]WritePSP [in FSSecModel.writeIsSecure]
WritePSS [in FSSecModel.writeIsSecure]
Axiom Index
A
ACLeq_dec [in FSSecModel.SFSstate]B
BYTE [in FSSecModel.SFSstate]BYTEeq_dec [in FSSecModel.SFSstate]
C
CATEGORY [in FSSecModel.SFSstate]comp_mode [in FSSecModel.stat]
create_directories [in FSSecModel.SFSstate]
create_files [in FSSecModel.SFSstate]
D
defaultState [in FSSecModel.ModelLemmas]G
GRPeq_dec [in FSSecModel.SFSstate]GRPNAME [in FSSecModel.SFSstate]
M
mkdir_directories [in FSSecModel.SFSstate]MyDir [in FSSecModel.SFSstate]
O
OBJDeq_dec [in FSSecModel.SFSstate]OBJFeq_dec [in FSSecModel.SFSstate]
OBJNAME [in FSSecModel.SFSstate]
OBJNAMEeq_dec [in FSSecModel.SFSstate]
OSCeq_dec [in FSSecModel.SFSstate]
R
rmdir_directories [in FSSecModel.SFSstate]root [in FSSecModel.SFSstate]
RootBelongsToAllGrp [in FSSecModel.InitialState]
RootBelongsToRootGrp [in FSSecModel.InitialState]
RWeq_dec [in FSSecModel.SFSstate]
S
SECMATeq_dec [in FSSecModel.SFSstate]secofr [in FSSecModel.SFSstate]
SecofrBelongsToAllGrp [in FSSecModel.InitialState]
SecofrBelongsToSecAdmGrp [in FSSecModel.InitialState]
SSCeq_dec [in FSSecModel.SFSstate]
SUBeq_dec [in FSSecModel.SFSstate]
SUBJECT [in FSSecModel.SFSstate]
SysAllGrp [in FSSecModel.InitialState]
SysGroups [in FSSecModel.InitialState]
SysPrimaryGrp [in FSSecModel.InitialState]
SysRootGrp [in FSSecModel.InitialState]
SysSecAdmGrp [in FSSecModel.InitialState]
SysSubjectSC [in FSSecModel.InitialState]
SysSubjectSCIsPARTFUNC [in FSSecModel.InitialState]
U
unlink_directories [in FSSecModel.SFSstate]unlink_files [in FSSecModel.SFSstate]
W
WFSI1 [in FSSecModel.ModelProperties]WFSI2 [in FSSecModel.ModelProperties]
WFSI3 [in FSSecModel.ModelProperties]
WFSI4 [in FSSecModel.ModelProperties]
WFSI5 [in FSSecModel.ModelProperties]
WFSI6 [in FSSecModel.ModelProperties]
WFSI7 [in FSSecModel.ModelProperties]
WFSI8 [in FSSecModel.ModelProperties]
WFSI9 [in FSSecModel.ModelProperties]
write_files [in FSSecModel.SFSstate]
Inductive Index
A
AclChanged [in FSSecModel.ModelProperties]aclstat [in FSSecModel.aclstat]
addUsrGrpToAcl [in FSSecModel.addUsrGrpToAcl]
C
chmod [in FSSecModel.chmod]chobjsc [in FSSecModel.chobjsc]
chown [in FSSecModel.chown]
chsubsc [in FSSecModel.chsubsc]
close [in FSSecModel.close]
create [in FSSecModel.create]
D
DACCtrlAttrHaveChanged [in FSSecModel.ModelProperties]delUsrGrpFromAcl [in FSSecModel.delUsrGrpFromAcl]
E
ExecuterIsOwner [in FSSecModel.DACandMAC]I
IsUNIXOwner [in FSSecModel.DACandMAC]M
MACObjCtrlAttrHaveChanged [in FSSecModel.ModelProperties]MACSubCtrlAttrHaveChanged [in FSSecModel.ModelProperties]
mkdir [in FSSecModel.mkdir]
MODE [in FSSecModel.SFSstate]
O
OBJTYPE [in FSSecModel.SFSstate]open [in FSSecModel.open]
Operation [in FSSecModel.SFSstate]
oscstat [in FSSecModel.oscstat]
owner_close [in FSSecModel.owner_close]
R
read [in FSSecModel.read]readdir [in FSSecModel.readdir]
rmdir [in FSSecModel.rmdir]
S
SecClassChanged [in FSSecModel.ModelProperties]sscstat [in FSSecModel.sscstat]
stat [in FSSecModel.stat]
T
TransFunc [in FSSecModel.TransFunc]U
UNIXAttrChanged [in FSSecModel.ModelProperties]unlink [in FSSecModel.unlink]
W
write [in FSSecModel.write]Projection Index
A
acl [in FSSecModel.SFSstate]ActReaders [in FSSecModel.SFSstate]
ActWriters [in FSSecModel.SFSstate]
AllGrp [in FSSecModel.SFSstate]
C
categs [in FSSecModel.SFSstate]D
directories [in FSSecModel.SFSstate]F
files [in FSSecModel.SFSstate]G
group [in FSSecModel.SFSstate]GroupOwners [in FSSecModel.SFSstate]
groupp [in FSSecModel.SFSstate]
GroupReaders [in FSSecModel.SFSstate]
groups [in FSSecModel.SFSstate]
GroupWriters [in FSSecModel.SFSstate]
L
level [in FSSecModel.SFSstate]O
objectSC [in FSSecModel.SFSstate]otherp [in FSSecModel.SFSstate]
owner [in FSSecModel.SFSstate]
ownerp [in FSSecModel.SFSstate]
P
primaryGrp [in FSSecModel.SFSstate]R
read_right [in FSSecModel.SFSstate]RootGrp [in FSSecModel.SFSstate]
S
SecAdmGrp [in FSSecModel.SFSstate]secmat [in FSSecModel.SFSstate]
st_gid [in FSSecModel.stat]
st_uid [in FSSecModel.stat]
st_mode [in FSSecModel.stat]
subjectSC [in FSSecModel.SFSstate]
U
UsersOwners [in FSSecModel.SFSstate]UsersReaders [in FSSecModel.SFSstate]
UsersWriters [in FSSecModel.SFSstate]
W
write_right [in FSSecModel.SFSstate]Section Index
A
Aclstat [in FSSecModel.aclstat]aclstatIsSecure [in FSSecModel.aclstatIsSecure]
AddUsrGrpToAcl [in FSSecModel.addUsrGrpToAcl]
addUsrGrpToAclIsSecure [in FSSecModel.addUsrGrpToAclIsSecure]
C
Chmod [in FSSecModel.chmod]chmodIsSecure [in FSSecModel.chmodIsSecure]
Chobjsc [in FSSecModel.chobjsc]
chobjscIsSecure [in FSSecModel.chobjscIsSecure]
Chown [in FSSecModel.chown]
chownIsSecure [in FSSecModel.chownIsSecure]
Chsubsc [in FSSecModel.chsubsc]
chsubscIsSecure [in FSSecModel.chsubscIsSecure]
Close [in FSSecModel.close]
closeIsSecure [in FSSecModel.closeIsSecure]
Create [in FSSecModel.create]
createIsSecure [in FSSecModel.createIsSecure]
D
DelUsrGrpFromAcl [in FSSecModel.delUsrGrpFromAcl]delUsrGrpFromAclIsSecure [in FSSecModel.delUsrGrpFromAclIsSecure]
F
first_definitions [in FSSecModel.ListSet]I
InitialState [in FSSecModel.InitialState]L
ListSetLemmas [in FSSecModel.ListFunctions]M
Mkdir [in FSSecModel.mkdir]mkdirIsSecure [in FSSecModel.mkdirIsSecure]
ModelProperties [in FSSecModel.ModelProperties]
O
Open [in FSSecModel.open]openIsSecure [in FSSecModel.openIsSecure]
Oscstat [in FSSecModel.oscstat]
oscstatIsSecure [in FSSecModel.oscstatIsSecure]
other_definitions [in FSSecModel.ListSet]
owner_closeIsSecure [in FSSecModel.owner_closeIsSecure]
Owner_Close [in FSSecModel.owner_close]
P
PartialFunctions [in FSSecModel.SFSstate]Preconditions [in FSSecModel.DACandMAC]
R
Read [in FSSecModel.read]Readdir [in FSSecModel.readdir]
readdirIsSecure [in FSSecModel.readdirIsSecure]
readIsSecure [in FSSecModel.readIsSecure]
Rmdir [in FSSecModel.rmdir]
rmdirIsSecure [in FSSecModel.rmdirIsSecure]
S
setACLdata [in FSSecModel.setACLdata]Sscstat [in FSSecModel.sscstat]
sscstatIsSecure [in FSSecModel.sscstatIsSecure]
Stat [in FSSecModel.stat]
statIsSecure [in FSSecModel.statIsSecure]
T
TransitionFunction [in FSSecModel.TransFunc]U
Unlink [in FSSecModel.unlink]unlinkIsSecure [in FSSecModel.unlinkIsSecure]
W
Write [in FSSecModel.write]writeIsSecure [in FSSecModel.writeIsSecure]
Record Index
A
AccessCtrlListData [in FSSecModel.SFSstate]P
PERMS [in FSSecModel.SFSstate]R
ReadersWriters [in FSSecModel.SFSstate]RIGHTS [in FSSecModel.SFSstate]
S
SecClass [in FSSecModel.SFSstate]SFSstate [in FSSecModel.SFSstate]
stat_struct [in FSSecModel.stat]
Definition Index
A
addUsrGrpToAcl_acl [in FSSecModel.addUsrGrpToAcl]allunique [in FSSecModel.ListFunctions]
C
ChangeGroupO [in FSSecModel.setACLdata]ChangeGroupR [in FSSecModel.setACLdata]
ChangeGroupW [in FSSecModel.setACLdata]
ChangeUserR [in FSSecModel.setACLdata]
ChangeUserW [in FSSecModel.setACLdata]
chmod_acl [in FSSecModel.chmod]
chobjsc_SC [in FSSecModel.chobjsc]
chown_acl [in FSSecModel.chown]
chsubsc_SC [in FSSecModel.chsubsc]
close_sm [in FSSecModel.close]
ControlProperty [in FSSecModel.ModelProperties]
create_acl [in FSSecModel.create]
create_oSC [in FSSecModel.create]
D
DACSecureState [in FSSecModel.ModelProperties]delUsrGrpFromAcl_acl [in FSSecModel.delUsrGrpFromAcl]
DIRCONT [in FSSecModel.SFSstate]
DOM [in FSSecModel.SFSstate]
domacl [in FSSecModel.SFSstate]
domd [in FSSecModel.SFSstate]
domf [in FSSecModel.SFSstate]
domOSC [in FSSecModel.SFSstate]
domsecmat [in FSSecModel.SFSstate]
domSSC [in FSSecModel.SFSstate]
E
empty_set [in FSSecModel.ListSet]eq_sc [in FSSecModel.SFSstate]
F
facl [in FSSecModel.SFSstate]fdirs [in FSSecModel.SFSstate]
ffiles [in FSSecModel.SFSstate]
FILECONT [in FSSecModel.SFSstate]
fOSC [in FSSecModel.SFSstate]
front [in FSSecModel.ListFunctions]
fsecmat [in FSSecModel.SFSstate]
fSSC [in FSSecModel.SFSstate]
FuncPre1 [in FSSecModel.ModelProperties]
FuncPre2 [in FSSecModel.ModelProperties]
FuncPre3 [in FSSecModel.ModelProperties]
FuncPre4 [in FSSecModel.ModelProperties]
FuncPre5 [in FSSecModel.ModelProperties]
FuncPre6 [in FSSecModel.ModelProperties]
FuncPre7 [in FSSecModel.ModelProperties]
G
GeneralSecureState [in FSSecModel.ModelLemmas]I
Included [in FSSecModel.ListFunctions]InFileSystem [in FSSecModel.DACandMAC]
InitState [in FSSecModel.InitialState]
IsEmpty [in FSSecModel.ListFunctions]
IsPARTFUNC [in FSSecModel.SFSstate]
L
last [in FSSecModel.ListFunctions]le_sc [in FSSecModel.SFSstate]
M
MACSecureState [in FSSecModel.ModelProperties]mkdir_acl [in FSSecModel.mkdir]
mkdir_oSC [in FSSecModel.mkdir]
N
NEWDIR [in FSSecModel.mkdir]NEWFILE [in FSSecModel.create]
NEWRW [in FSSecModel.close]
NEWRWOC [in FSSecModel.owner_close]
O
OBJECT [in FSSecModel.SFSstate]ObjName [in FSSecModel.SFSstate]
ObjType [in FSSecModel.SFSstate]
open_sm [in FSSecModel.open]
ownerclose_sm [in FSSecModel.owner_close]
P
PARTFUNC [in FSSecModel.SFSstate]PreDACRead [in FSSecModel.DACandMAC]
PreDACWrite [in FSSecModel.DACandMAC]
PreMAC [in FSSecModel.DACandMAC]
PreservesControlProp [in FSSecModel.ModelProperties]
PreStarPropRead [in FSSecModel.DACandMAC]
PreStarPropWrite [in FSSecModel.DACandMAC]
R
RAN [in FSSecModel.SFSstate]ransecmat [in FSSecModel.SFSstate]
rmdir_acl [in FSSecModel.rmdir]
rmdir_oSC [in FSSecModel.rmdir]
S
SECLEV [in FSSecModel.SFSstate]SecureState [in FSSecModel.ModelProperties]
set [in FSSecModel.ListSet]
set_fold_right [in FSSecModel.ListSet]
set_fold_left [in FSSecModel.ListSet]
set_map [in FSSecModel.ListSet]
set_power [in FSSecModel.ListSet]
set_prod [in FSSecModel.ListSet]
set_In [in FSSecModel.ListSet]
set_diff [in FSSecModel.ListSet]
set_union [in FSSecModel.ListSet]
set_inter [in FSSecModel.ListSet]
set_remove [in FSSecModel.ListSet]
set_mem [in FSSecModel.ListSet]
set_add [in FSSecModel.ListSet]
StarProperty [in FSSecModel.ModelProperties]
T
take [in FSSecModel.ListFunctions]U
unlink_acl [in FSSecModel.unlink]unlink_oSC [in FSSecModel.unlink]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (617 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (65 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (50 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (90 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (153 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (32 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |