Nuprl Definition : lex-pair
lex-pair(S;ord1;ord2) == 
x,y.((ord1 (fst(x)) (fst(y))) 
(((fst(x)) = (fst(y))) 
(ord2 (snd(x)) (snd(y)))))
Proof not projected
Definitions occuring in Statement :
pi1: fst(t),
pi2: snd(t),
or: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
equal: s = t
Definitions :
lambda: x.A[x],
or: P Q,
and: P Q,
equal: s = t,
pi1: fst(t),
apply: f a,
pi2: snd(t)
FDL editor aliases :
lex-pair
lex-pair(S;ord1;ord2) ==
\mlambda{}x,y.((ord1 (fst(x)) (fst(y))) \mvee{} (((fst(x)) = (fst(y))) \mwedge{} (ord2 (snd(x)) (snd(y)))))
Date html generated:
2011_10_20-PM-04_50_38
Last ObjectModification:
2011_05_19-AM-11_30_17
Home
Index