Nuprl Definition : pair-blex
pair-blex(eq;Ra;Rb) == λx,y. ((Ra (fst(x)) (fst(y))) ∨b((eq (fst(x)) (fst(y))) ∧b (Rb (snd(x)) (snd(y)))))
Definitions occuring in Statement :
bor: p ∨bq,
band: p ∧b q,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
bor: p ∨bq,
band: p ∧b q,
pi1: fst(t),
apply: f a,
pi2: snd(t)
FDL editor aliases :
pair-blex
Latex:
pair-blex(eq;Ra;Rb) ==
\mlambda{}x,y. ((Ra (fst(x)) (fst(y))) \mvee{}\msubb{}((eq (fst(x)) (fst(y))) \mwedge{}\msubb{} (Rb (snd(x)) (snd(y)))))
Date html generated:
2016_05_13-PM-03_58_16
Last ObjectModification:
2015_09_22-PM-05_45_39
Theory : bool_1
Home
Index