Nuprl Definition : proddeq
proddeq(a;b) == λp,q. ((a (fst(p)) (fst(q))) ∧b (b (snd(p)) (snd(q))))
Definitions occuring in Statement :
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],
band: p ∧b q,
pi1: fst(t),
apply: f a,
pi2: snd(t)
FDL editor aliases :
proddeq
Latex:
proddeq(a;b) == \mlambda{}p,q. ((a (fst(p)) (fst(q))) \mwedge{}\msubb{} (b (snd(p)) (snd(q))))
Date html generated:
2016_05_14-AM-06_07_16
Last ObjectModification:
2015_09_22-PM-05_48_14
Theory : equality!deciders
Home
Index