Nuprl Definition : basic-seq-1-4
A ⟶ B: pas[A;B;m;n;x;y] == λA,B,es,thr. ∃m,n,x,y:Atom1. pas[A;B;m;n;x;y](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-4
Latex:
A {}\mrightarrow{} B: pas[A;B;m;n;x;y] == \mlambda{}A,B,es,thr. \mexists{}m,n,x,y:Atom1. pas[A;B;m;n;x;y](thr)
Date html generated:
2016_05_17-PM-00_41_54
Last ObjectModification:
2012_08_30-PM-04_33_02
Theory : event-logic-applications
Home
Index