Nuprl Definition : ballot-lt
ballot-lt(Id-lt) == add-bottom(lex-pair(
;
i,j.(i < j);Id-lt))
Proof not projected
Definitions occuring in Statement :
add-bottom: add-bottom(ord),
lex-pair: lex-pair(S;ord1;ord2),
less_than: a < b,
lambda: x.A[x],
int:
Definitions :
add-bottom: add-bottom(ord),
lex-pair: lex-pair(S;ord1;ord2),
int: ,
lambda: x.A[x],
less_than: a < b
FDL editor aliases :
ballot-lt
ballot-lt(Id-lt) == add-bottom(lex-pair(\mBbbZ{};\mlambda{}i,j.(i < j);Id-lt))
Date html generated:
2011_10_20-PM-04_59_42
Last ObjectModification:
2011_05_19-AM-11_36_24
Home
Index