Nuprl Lemma : ballot-lt_wf
[Id-lt:Id 
Id 
]. (ballot-lt(Id-lt) 
Ballot_Num() Ballot_Num() )
Proof not projected
Definitions occuring in Statement :
ballot-lt: ballot-lt(Id-lt),
Ballot_Num: Ballot_Num(),
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T,
function: x:A B[x]
Definitions :
bool: 
,
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
and: P 
Q,
uiff: uiff(P;Q),
es-E-interface: E(X),
uimplies: b supposing a,
subtype_rel: A 
r B,
subtype: S T,
suptype: suptype(S; T),
unit: Unit,
lambda: 
x.A[x],
product: x:A 
B[x],
int: 
,
less_than: a < b,
lex-pair: lex-pair(S;ord1;ord2),
union: left + right,
add-bottom: add-bottom(ord),
uall: [x:A]. B[x],
isect: 
x:A. B[x],
Ballot_Num: Ballot_Num(),
ballot-lt: ballot-lt(Id-lt),
axiom: Ax,
equal: s = t,
prop: ,
universe: Type,
Id: Id,
all: x:A. B[x],
function: x:A B[x],
member: t T
Lemmas :
Ballot_Num_wf,
member_wf,
unit_wf,
Id_wf,
lex-pair_wf,
add-bottom_wf
\mforall{}[Id-lt:Id {}\mrightarrow{} Id {}\mrightarrow{} \mBbbP{}]. (ballot-lt(Id-lt) \mmember{} Ballot\_Num() {}\mrightarrow{} Ballot\_Num() {}\mrightarrow{} \mBbbP{})
Date html generated:
2011_10_20-PM-04_59_55
Last ObjectModification:
2011_05_19-AM-11_39_00
Home
Index