{ 
[T:Type]. [eq:EqDecider(T)]. [L:T List]. [i:
||L||].
mu(
i@0.(eqof(eq) L[i] L[i@0])) = i supposing no_repeats(T;L) }
{ Proof }
Definitions occuring in Statement :
select: l[i],
length: ||as||,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
apply: f a,
lambda: x.A[x],
list: type List,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
no_repeats: no_repeats(T;l),
eqof: eqof(d),
deq: EqDecider(T),
mu: mu(f)
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t 
T,
and: P 
Q,
assert: 
b,
all: x:A. B[x],
implies: P 
Q,
top: Top,
subtype: S 
T,
le: A 
B,
not: 
A,
false: False,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
prop: 
,
nat: ,
squash: 
T,
int_seg: {i..j},
lelt: i j < k,
iff: P 
Q,
l_member!: (x ! l),
exists: 
x:A. B[x],
cand: A c B
Lemmas :
mu-bound-unique,
length_wf_nat,
top_wf,
eqof_wf,
select_wf,
eqof_eq_btrue,
assert_wf,
no_repeats_wf,
int_seg_wf,
length_wf1,
deq_wf,
iff_weakening_uiff,
uiff_inversion,
deq_property,
no_repeats_member,
select_member,
le_wf
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[L:T List]. \mforall{}[i:\mBbbN{}||L||].
mu(\mlambda{}i@0.(eqof(eq) L[i] L[i@0])) = i supposing no\_repeats(T;L)
Date html generated:
2011_08_10-AM-07_52_29
Last ObjectModification:
2011_06_18-AM-08_14_37
Home
Index