---

Step * of Lemma index-split_property

∀[T:Type]
  ∀L:T List. ∀idxs:ℕ List.
    let L1 = fst(index-split(L;idxs)) in
        ∃f:ℕ||L1|| ⟶ {i:ℕ||L||| (i ∈ idxs)} . (Bij(ℕ||L1||;{i:ℕ||L||| (i ∈ idxs)} ;f) ∧ (∀j:ℕ||L1||. (L1[j] = L[f j] ∈ \000CT)))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `permute-to-front-permutation` [⌜T⌝;⌜L⌝;⌜idxs⌝]⋅ THENA Auto)
   THEN (FLemma `permutation-length` [-1] THENA Auto)
   THEN (Assert ||filter(λi.int-list-member(i;idxs);upto(||L||))|| ≤ ||permute-to-front(L;idxs)|| BY
               (Subst' ||permute-to-front(L;idxs)|| ~ ||upto(||L||)|| 0
                THEN Try ((BLemma `length-filter` THEN Auto))
                THEN RevHypSubst' (-1) 0
                THEN RWO "length_upto" 0
                THEN Auto))
   THEN RepUR ``index-split let`` 0
   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)||
⊢ ∃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)))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}idxs:\mBbbN{}  List.
        let  L1  =  fst(index-split(L;idxs))  in
                \mexists{}f:\mBbbN{}||L1||  {}\mrightarrow{}  \{i:\mBbbN{}||L|||  (i  \mmember{}  idxs)\}  .  (Bij(\mBbbN{}||L1||;\{i:\mBbbN{}||L|||  (i  \mmember{}  idxs)\}  ;f)  \mwedge{}  (\mforall{}j:\mBbbN{}||L1||\000C.  (L1[j]  =  L[f  j])))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `permute-to-front-permutation`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}idxs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `permutation-length`  [-1]  THENA  Auto)
  THEN  (Assert  ||filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))||  \mleq{}  ||permute-to-front(L;idxs)||  BY
                          (Subst'  ||permute-to-front(L;idxs)||  \msim{}  ||upto(||L||)||  0
                            THEN  Try  ((BLemma  `length-filter`  THEN  Auto))
                            THEN  RevHypSubst'  (-1)  0
                            THEN  RWO  "length\_upto"  0
                            THEN  Auto))
  THEN  RepUR  ``index-split  let``  0
  THEN  Auto)

---

Home Index