---

Step * 1 1 1 1 1 1 1 1 of Lemma index-split_property


1. T : Type
2. L : T List
3. idxs : ℕ List
4. permutation(T;L;permute-to-front(L;idxs))
5. ||L|| = ||permute-to-front(L;idxs)|| ∈ ℤ
6. ||filter(λi.int-list-member(i;idxs);upto(||L||))|| ≤ ||permute-to-front(L;idxs)||
7. idxs1 : {i:ℕ||L||| (i ∈ idxs)}  List
8. filter(λi.int-list-member(i;idxs);upto(||L||)) = idxs1 ∈ (ℤ List)
9. ||idxs1|| ≤ ||permute-to-front(L;idxs)||
⊢ no_repeats({i:ℕ||L||| (i ∈ idxs)} ;idxs1)
BY
{ ((RevHypSubst' (-2) 0 THEN Auto)
   THEN (Assert no_repeats(ℕ||L||;filter(λi.int-list-member(i;idxs);upto(||L||))) BY
               ((BLemma `no_repeats_filter` THEN Auto) THEN BLemma `no_repeats_upto` THEN Auto))
   ) }

1
1. T : Type
2. L : T List
3. idxs : ℕ List
4. permutation(T;L;permute-to-front(L;idxs))
5. ||L|| = ||permute-to-front(L;idxs)|| ∈ ℤ
6. ||filter(λi.int-list-member(i;idxs);upto(||L||))|| ≤ ||permute-to-front(L;idxs)||
7. idxs1 : {i:ℕ||L||| (i ∈ idxs)}  List
8. filter(λi.int-list-member(i;idxs);upto(||L||)) = idxs1 ∈ (ℤ List)
9. ||idxs1|| ≤ ||permute-to-front(L;idxs)||
10. no_repeats(ℕ||L||;filter(λi.int-list-member(i;idxs);upto(||L||)))
⊢ no_repeats({i:ℕ||L||| (i ∈ idxs)} ;filter(λi.int-list-member(i;idxs);upto(||L||)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  idxs  :  \mBbbN{}  List
4.  permutation(T;L;permute-to-front(L;idxs))
5.  ||L||  =  ||permute-to-front(L;idxs)||
6.  ||filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))||  \mleq{}  ||permute-to-front(L;idxs)||
7.  idxs1  :  \{i:\mBbbN{}||L|||  (i  \mmember{}  idxs)\}    List
8.  filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))  =  idxs1
9.  ||idxs1||  \mleq{}  ||permute-to-front(L;idxs)||
\mvdash{}  no\_repeats(\{i:\mBbbN{}||L|||  (i  \mmember{}  idxs)\}  ;idxs1)


By

---

Latex:
((RevHypSubst'  (-2)  0  THEN  Auto)
  THEN  (Assert  no\_repeats(\mBbbN{}||L||;filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||)))  BY
                          ((BLemma  `no\_repeats\_filter`  THEN  Auto)  THEN  BLemma  `no\_repeats\_upto`  THEN  Auto))
  )

---

Home Index