Nuprl Definition : ses-V
PropertyV ==
∀es:EO+(Info). ∀e:E(Verify). ∃e':E(Sign). ((e' < e) ∧ (Verify(e) = Sign(e') ∈ (SecurityData × Id × Atom1)))
Definitions occuring in Statement :
ses-verify: Verify,
ses-sign: Sign,
ses-info: Info,
sdata: SecurityData,
es-E-interface: E(X),
eclass-val: X(e),
event-ordering+: EO+(Info),
es-causl: (e < e'),
Id: Id,
atom: Atom$n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
ses-V
Latex:
PropertyV == \mforall{}es:EO+(Info). \mforall{}e:E(Verify). \mexists{}e':E(Sign). ((e' < e) \mwedge{} (Verify(e) = Sign(e')))
Date html generated:
2016_05_17-PM-00_24_40
Last ObjectModification:
2012_08_30-PM-04_24_13
Theory : event-logic-applications
Home
Index