Nuprl Definition : basic-seq-1-3
A ─→ B: pas[A; B; m; n; x] == λA,B,es,thr. ∃m,n,x:Atom1. pas[A; B; m; n; x](thr)
Definitions occuring in Statement :
ses-is-protocol-actions: pas(thr),
atom: Atom$n,
exists: ∃x:A. B[x],
lambda: λx.A[x]
FDL editor aliases :
b-s-1-3
Latex:
A {}\mrightarrow{} B: pas[A; B; m; n; x] == \mlambda{}A,B,es,thr. \mexists{}m,n,x:Atom1. pas[A; B; m; n; x](thr)
Date html generated:
2015_07_23-PM-00_16_15
Last ObjectModification:
2012_08_30-PM-04_32_54
Home
Index