Nuprl Definition : es-interface-pair
(X,Y) == eclass-compose2(λxs,ys. if (#(xs) =z 1) ∧b (#(ys) =z 1) then {<only(xs), only(ys)>} else {} fi ;X;Y)
Definitions occuring in Statement :
eclass-compose2: eclass-compose2(f;X;Y),
band: p ∧b q,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n,
bag-only: only(bs),
bag-size: #(bs),
single-bag: {x},
empty-bag: {}
FDL editor aliases :
es-interface-pair
Latex:
(X,Y) ==
eclass-compose2(\mlambda{}xs,ys. if (\#(xs) =\msubz{} 1) \mwedge{}\msubb{} (\#(ys) =\msubz{} 1) then \{<only(xs), only(ys)>\} else \{\} fi ;X;\000CY)
Date html generated:
2016_05_17-AM-07_12_28
Last ObjectModification:
2012_02_25-PM-02_44_55
Theory : event-ordering
Home
Index