Nuprl Definition : p-union
p-union(A;B) == λp.if (A p =z 1) then 1 else B p fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
apply: f a
FDL editor aliases :
p-union
p-union(A;B) == \mlambda{}p.if (A p =\msubz{} 1) then 1 else B p fi
Date html generated:
2015_07_17-AM-08_00_15
Last ObjectModification:
2008_02_27-PM-05_49_35
Home
Index