Nuprl Definition : latest-pair
(X&Y) ==
eclass-compose4(λx,y,x',y'. if (#(x) =z 1)
then if (#(y) =z 1) then {<only(x), only(y)>}
if (#(y') =z 1) then {<only(x), only(y')>}
else {}
fi
if (#(y) =z 1) then if (#(x') =z 1) then {<only(x'), only(y)>} else {} fi
else {}
fi ;X;Y;Prior(X);Prior(Y))
Definitions occuring in Statement :
primed-class: Prior(X),
eclass-compose4: eclass-compose4(f;X;Y;Z;V),
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 :
latest-pair
Latex:
(X\&Y) ==
eclass-compose4(\mlambda{}x,y,x',y'. if (\#(x) =\msubz{} 1)
then if (\#(y) =\msubz{} 1) then \{<only(x), only(y)>\}
if (\#(y') =\msubz{} 1) then \{<only(x), only(y')>\}
else \{\}
fi
if (\#(y) =\msubz{} 1)
then if (\#(x') =\msubz{} 1) then \{<only(x'), only(y)>\} else \{\} fi
else \{\}
fi ;X;Y;Prior(X);Prior(Y))
Date html generated:
2015_07_21-PM-03_45_22
Last ObjectModification:
2012_02_25-PM-02_45_33
Home
Index