Nuprl Definition : sumdeq

sumdeq(a;b) ==
  λp,q. case p
        of inl(pa) =>
        case q of inl(qa) => a pa qa | inr(qb) => ff
        | inr(pb) =>
        case q of inl(qa) => ff | inr(qb) => b pb qb

Definitions occuring in Statement : bfalse: ff, apply: f a, lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], bfalse: ff, apply: f a
FDL editor aliases : sumdeq

Latex:
sumdeq(a;b) == \mlambda{}p,q. case p of inl(pa) => case q of inl(qa) => a pa qa | inr(qb) => ff | inr(pb) => case q of inl(qa) => ff | inr(qb) => b pb qb Date html generated: 2016_05_14-AM-06_07_29 Last ObjectModification: 2015_09_22-PM-05_48_15 Theory : equality!deciders Home Index