{ 
[T:Type]. [eq:EqDecider(T)]. [L:T List]. [i:
||L||].
index(L;L[i]) ~ i supposing no_repeats(T;L) }
{ Proof }
Definitions occuring in Statement :
l_index: index(L;x),
select: l[i],
length: ||as||,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
list: type List,
natural_number: $n,
universe: Type,
sqequal: s ~ t,
no_repeats: no_repeats(T;l),
deq: EqDecider(T)
Definitions :
l_index: index(L;x),
member: t 
T,
uall: [x:A]. B[x],
uimplies: b supposing a,
sq_type: SQType(T),
all: x:A. B[x],
implies: P 
Q,
guard: {T}
Lemmas :
no_repeats_mu_index,
subtype_base_sq,
int_subtype_base,
no_repeats_wf,
int_seg_wf,
length_wf1,
deq_wf
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[L:T List]. \mforall{}[i:\mBbbN{}||L||].
index(L;L[i]) \msim{} i supposing no\_repeats(T;L)
Date html generated:
2011_08_10-AM-07_52_33
Last ObjectModification:
2011_06_18-AM-08_14_40
Home
Index