Nuprl Lemma : mu_ex_v5_no_repeats_headers_no_inputs
no_repeats(Name;mu_ex_v5_headers_no_inputs())
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_headers_no_inputs: mu_ex_v5_headers_no_inputs(),
name: Name,
no_repeats: no_repeats(T;l)
Definitions :
no_repeats: no_repeats(T;l),
name: Name,
mu_ex_v5_headers_no_inputs: mu_ex_v5_headers_no_inputs(),
uall: 
[x:A]. B[x],
uimplies: b supposing a,
length: ||as||,
not: 
A,
ycomb: Y,
member: t 
T,
implies: P 
Q,
false: False,
or: P 
Q,
prop: 
,
tl: tl(l),
and: P 
Q,
ifthenelse: if b then t else f fi ,
bfalse: ff,
assert: 
b,
name_eq: name_eq(x;y),
uiff: uiff(P;Q),
name-deq: NameDeq,
list-deq: list-deq(eq),
band: p 
q,
atom-deq: AtomDeq,
eq_atom: x =a y,
nat: 
,
le: A 
B,
select: l[i],
sq_type: SQType(T),
all: x:A. B[x],
guard: {T},
le_int: i z j,
bnot: b,
lt_int: i <z j,
btrue: tt
Lemmas :
name_wf,
select_wf,
not_wf,
equal_wf,
nat_wf,
nat_properties,
less_than_wf,
subtype_base_sq,
int_subtype_base,
and_wf,
tl_wf,
assert-name_eq
no\_repeats(Name;mu\_ex\_v5\_headers\_no\_inputs())
Date html generated:
2012_02_20-PM-06_59_44
Last ObjectModification:
2012_02_02-PM-03_01_31
Home
Index