Nuprl Definition : eq

Nuprl Definition : eq_ballot

eq_ballot(b1;b2) ==
  case b1
  of inl(p1) =>
   case b2 of inl(p2) => let n1,l1 = p1 in let n2,l2 = p2 in (n1 =

n2)

(l1 =

l2) | inr(x) => ff
| inr(x) =>

isl(b2)

Proof not projected

Definitions occuring in Statement : isl: isl(x), eq_int: (i =

j), band: p

q, bnot:

b, bfalse: ff, spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions : decide: case b of inl(x) => s[x] | inr(y) => t[y], spread: spread def, band: p

q, eq_int: (i =

j), bfalse: ff, bnot:

b, isl: isl(x)
FDL editor aliases : eq_ballot

eq\_ballot(b1;b2) == case b1 of inl(p1) => case b2 of inl(p2) => let n1,l1 = p1 in let n2,l2 = p2 in (n1 =\msubz{} n2) \mwedge{}\msubb{} (l1 =\msubz{} l2) | inr(x) => ff | inr(x) => \mneg{}\msubb{}isl(b2) Date html generated: 2011_10_20-PM-04_12_31 Last ObjectModification: 2011_01_26-PM-03_30_06 Home Index