Nuprl Lemma : ballot-less_wf
[b1,b2:ballot-id()]. (ballot-less(b1;b2) 
)
Proof not projected
Definitions occuring in Statement :
ballot-less: ballot-less(b1;b2),
ballot-id: ballot-id(),
bool: ,
uall: [x:A]. B[x],
member: t T
Definitions :
isl: isl(x),
bfalse: ff,
eq_int: (i =
j),
band: p 
q,
set: {x:A| B[x]} ,
real: 
,
grp_car: |g|,
subtype: S 
T,
function: x:A 
B[x],
all: x:A. B[x],
int: 
,
lt_int: i <z j,
bor: p 
q,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ballot-id: ballot-id(),
bool: ,
ballot-less: ballot-less(b1;b2),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
union: left + right,
product: x:A 
B[x],
nat: 
,
unit: Unit,
equal: s = t,
member: t T,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic
Lemmas :
bor_wf,
band_wf,
eq_int_wf,
lt_int_wf,
bfalse_wf,
unit_wf,
nat_wf,
isl_wf
\mforall{}[b1,b2:ballot-id()]. (ballot-less(b1;b2) \mmember{} \mBbbB{})
Date html generated:
2011_10_20-PM-04_15_40
Last ObjectModification:
2011_01_29-AM-00_44_30
Home
Index