{ SES 
' }
{ Proof }
Definitions occuring in Statement :
security-event-structure: SES,
member: t T,
universe: Type
Definitions :
equal: s = t,
member: t T,
function: x:A 
B[x],
all: 
x:A. B[x],
top: Top,
atom: Atom$n,
universe: Type,
Id: Id,
product: x:A 
B[x],
bool: 
,
encryption-key: Key,
so_lambda: 
x y.t[x; y],
eclass: EClass(A[eo; e]),
subtype: S 
T,
event_ordering: EO,
event-ordering+: EO+(Info),
es-E: E,
sdata: SecurityData,
lambda: x.A[x],
security-event-structure: SES,
Auto: Error :Auto,
Unfold: Error :Unfold,
tactic: Error :tactic,
CollapseTHEN: Error :CollapseTHEN
Lemmas :
event-ordering+_wf,
sdata_wf,
es-E_wf,
event-ordering+_inc,
eclass_wf,
encryption-key_wf,
bool_wf,
Id_wf,
top_wf
SES \mmember{} \mBbbU{}'
Date html generated:
2010_08_28-AM-01_49_47
Last ObjectModification:
2010_02_22-AM-11_58_39
Home
Index