Nuprl Definition : ballot-less

ballot-less(b1;b2) ==
  case b1
  of inl(p1) =>
   case b2 of inl(p2) => let n1,l1 = p1 in let n2,l2 = p2 in n1 <z n2

((n1 =

n2)

l1 <z l2) | inr(x) => ff
| inr(x) =>
isl(b2)

Proof not projected

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

j), bor: p

q, band: p

q, lt_int: i <z j, 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, bor: p

q, band: p

q, eq_int: (i =

j), lt_int: i <z j, bfalse: ff, isl: isl(x)
FDL editor aliases : ballot-less

ballot-less(b1;b2) == case b1 of inl(p1) => case b2 of inl(p2) => let n1,l1 = p1 in let n2,l2 = p2 in n1 <z n2 \mvee{}\msubb{}((n1 =\msubz{} n2) \mwedge{}\msubb{} l1 <z l2) | inr(x) => ff | inr(x) => isl(b2) Date html generated: 2011_10_20-PM-04_15_21 Last ObjectModification: 2011_01_26-PM-03_30_56 Home Index