---

Step * 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)||
⊢ ∃f:ℕ||firstn(||filter(λi.int-list-member(i;idxs);upto(||L||))||;permute-to-front(L;idxs))|| ⟶ {i:ℕ||L||| (i ∈ idxs)} 
   (Bij(ℕ||firstn(||filter(λi.int-list-member(i;idxs);upto(||L||))||;permute-to-front(L;idxs))||;{i:ℕ||L||| (i ∈ idxs)} \000C;f)
   ∧ (∀j:ℕ||firstn(||filter(λi.int-list-member(i;idxs);upto(||L||))||;permute-to-front(L;idxs))||
        (firstn(||filter(λi.int-list-member(i;idxs);upto(||L||))||;permute-to-front(L;idxs))[j] = L[f j] ∈ T)))
BY
{ (GenConcl ⌜filter(λi.int-list-member(i;idxs);upto(||L||)) = idxs1 ∈ ({i:ℕ||L||| (i ∈ idxs)}  List)⌝⋅
   THENA Try (Complete (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 ∈ ({i:ℕ||L||| (i ∈ idxs)}  List)
⊢ ∃f:ℕ||firstn(||idxs1||;permute-to-front(L;idxs))|| ⟶ {i:ℕ||L||| (i ∈ idxs)} 
   (Bij(ℕ||firstn(||idxs1||;permute-to-front(L;idxs))||;{i:ℕ||L||| (i ∈ idxs)} ;f)
   ∧ (∀j:ℕ||firstn(||idxs1||;permute-to-front(L;idxs))||. (firstn(||idxs1||;permute-to-front(L;idxs))[j] = L[f j] ∈ T)))

---

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)||
\mvdash{}  \mexists{}f:\mBbbN{}||firstn(||filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))||;permute-to-front(L;idxs))||
          {}\mrightarrow{}  \{i:\mBbbN{}||L|||  (i  \mmember{}  idxs)\} 
      (Bij(\mBbbN{}||firstn(||filter(\mlambda{}i.int-list-member(i;idxs);
                                                      upto(||L||))||;permute-to-front(L;idxs))||;\{i:\mBbbN{}||L|||  (i  \mmember{}  idxs)\}  ;f)
      \mwedge{}  (\mforall{}j:\mBbbN{}||firstn(||filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))||;permute-to-front(L;idxs))||
                (firstn(||filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))||;permute-to-front(L;idxs))[j]
                =  L[f  j])))


By

---

Latex:
(GenConcl  \mkleeneopen{}filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))  =  idxs1\mkleeneclose{}\mcdot{}  THENA  Try  (Complete  (Auto)))

---

Home Index