Nuprl Lemma : mk-ballot_wf
[n,ldr:
]. (mk-ballot(n;ldr) 
ballot-id())
Proof not projected
Definitions occuring in Statement :
mk-ballot: mk-ballot(n;ldr),
ballot-id: ballot-id(),
nat: ,
uall: [x:A]. B[x],
member: t T
Definitions :
pair: <a, b>,
inl: inl x ,
ballot-id: ballot-id(),
union: left + right,
product: x:A 
B[x],
unit: Unit,
mk-ballot: mk-ballot(n;ldr),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
member: t T,
equal: s = t,
nat: ,
CollapseTHEN: Error :CollapseTHEN
Lemmas :
nat_wf,
unit_wf
\mforall{}[n,ldr:\mBbbN{}]. (mk-ballot(n;ldr) \mmember{} ballot-id())
Date html generated:
2011_10_20-PM-04_12_17
Last ObjectModification:
2011_01_29-AM-00_43_15
Home
Index