Nuprl Definition : add-bottom

add-bottom(ord) ==  x,y.(((isl(x))  (isl(y)))  (((isl(x))  (isl(y)))  (ord outl(x) outl(y))))


Proof not projected



Definitions occuring in Statement :  outl: outl(x),  isl: isl(x),  assert: b,  not: A,  or: P  Q,  and: P  Q,  apply: f a,  lambda: x.A[x]
Definitions :  lambda: x.A[x],  or: P  Q,  not: A,  and: P  Q,  assert: b,  isl: isl(x),  apply: f a,  outl: outl(x)
FDL editor aliases :  add-bottom
add-bottom(ord)  ==
    \mlambda{}x,y.(((\mneg{}\muparrow{}isl(x))  \mwedge{}  (\muparrow{}isl(y)))  \mvee{}  (((\muparrow{}isl(x))  \mwedge{}  (\muparrow{}isl(y)))  \mwedge{}  (ord  outl(x)  outl(y))))


Date html generated: 2011_10_20-PM-04_51_04
Last ObjectModification: 2011_05_19-AM-11_15_47

Home Index