Nuprl Definition : union-sep

union-sep(ss1;ss2;p;q) ==
  case p
   of inl(a) =>
   case q of inl(a') => a # a' | inr(b') => True
   | inr(b) =>
   case q of inl(a') => True | inr(b') => b # b'

Definitions occuring in Statement : ss-sep: x # y, true: True, decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : decide: case b of inl(x) => s[x] | inr(y) => t[y], true: True, ss-sep: x # y
FDL editor aliases : union-sep

Latex:
union-sep(ss1;ss2;p;q) == case p of inl(a) => case q of inl(a') => a \# a' | inr(b') => True | inr(b) => case q of inl(a') => True | inr(b') => b \# b' Date html generated: 2019_10_31-AM-07_26_54 Last ObjectModification: 2019_03_19-PM-03_41_39 Theory : constructive!algebra Home Index