Nuprl Lemma : eq_ballot_wf
[b1,b2:ballot-id()]. (eq_ballot(b1;b2) 
)
Proof not projected
Definitions occuring in Statement :
eq_ballot: eq_ballot(b1;b2),
ballot-id: ballot-id(),
bool: ,
uall: [x:A]. B[x],
member: t T
Definitions :
strong-subtype: strong-subtype(A;B),
not: 
A,
less_than: a < b,
and: P 
Q,
uiff: uiff(P;Q),
natural_number: $n,
fpf: a:A fp-> B[a],
subtype: S 
T,
uimplies: b supposing a,
subtype_rel: A r B,
eclass: EClass(A[eo; e]),
isl: isl(x),
inr: inr x ,
le: A 
B,
ge: i 
j ,
int: 
,
pair: <a, b>,
set: {x:A| B[x]} ,
guard: {T},
implies: P 
Q,
sq_type: SQType(T),
eq_int: (i =
j),
band: p 
q,
spread: spread def,
nat: 
,
unit: Unit,
inl: inl x ,
product: x:A 
B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
universe: Type,
bnot: b,
bfalse: ff,
btrue: tt,
function: x:A 
B[x],
all: x:A. B[x],
union: left + right,
bool: ,
eq_ballot: eq_ballot(b1;b2),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
member: t T,
equal: s = t,
ballot-id: ballot-id()
Lemmas :
isl_wf,
bool_wf,
member_wf,
bnot_wf,
bfalse_wf,
nat_properties,
eq_int_wf,
band_wf,
unit_wf,
nat_wf,
ballot-id_wf,
btrue_wf,
subtype_rel_wf
\mforall{}[b1,b2:ballot-id()]. (eq\_ballot(b1;b2) \mmember{} \mBbbB{})
Date html generated:
2011_10_20-PM-04_12_44
Last ObjectModification:
2011_01_29-AM-00_43_43
Home
Index