Nuprl Definition : fresh-sig-protocol1
FreshSignatures(bss) ==
∃f:SecurityData ⟶ (Atom1?)
∀es:EO+(Info). ∀thr:Thread. ∀A:Id. ((thr is one of bss at A) ⇒ ses-fresh-thread(s;es;f;A;thr))
Definitions occuring in Statement :
ses-fresh-thread: ses-fresh-thread(s;es;f;A;thr),
ses-protocol1-thread: (thr is one of bss at A),
ses-thread: Thread,
ses-info: Info,
sdata: SecurityData,
event-ordering+: EO+(Info),
Id: Id,
atom: Atom$n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
unit: Unit,
function: x:A ⟶ B[x],
union: left + right
FDL editor aliases :
fresh-sig-protocol1
Latex:
FreshSignatures(bss) ==
\mexists{}f:SecurityData {}\mrightarrow{} (Atom1?)
\mforall{}es:EO+(Info). \mforall{}thr:Thread. \mforall{}A:Id. ((thr is one of bss at A) {}\mRightarrow{} ses-fresh-thread(s;es;f;A;thr))
Date html generated:
2016_05_17-PM-00_43_27
Last ObjectModification:
2012_08_30-PM-04_33_52
Theory : event-logic-applications
Home
Index