---

Step * 1 1 1 1 1 2 1 2 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)||
10. Bij(ℕ||idxs1||;{i:ℕ||L||| (i ∈ idxs)} ;λi.idxs1[i])
11. j : ℕ||idxs1||
⊢ L[(λi.filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i]) j]
= L[idxs1[j]]
∈ T
BY
{ (Reduce 0
   THEN Subst' filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[j] 
        ~ idxs1[j] 0
   )⋅ }

1
.....equality..... 
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. Bij(ℕ||idxs1||;{i:ℕ||L||| (i ∈ idxs)} ;λi.idxs1[i])
11. j : ℕ||idxs1||
⊢ filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[j] ~ idxs1[j]

2
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. Bij(ℕ||idxs1||;{i:ℕ||L||| (i ∈ idxs)} ;λi.idxs1[i])
11. j : ℕ||idxs1||
⊢ L[idxs1[j]] = L[idxs1[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)||
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)||
10.  Bij(\mBbbN{}||idxs1||;\{i:\mBbbN{}||L|||  (i  \mmember{}  idxs)\}  ;\mlambda{}i.idxs1[i])
11.  j  :  \mBbbN{}||idxs1||
\mvdash{}  L[(\mlambda{}i.filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))
                @  filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||))[i]) 
        j]
=  L[idxs1[j]]


By

---

Latex:
(Reduce  0
  THEN  Subst'  filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))
            @  filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||))[j]  \msim{}  idxs1[j]  0
  )\mcdot{}

---

Home Index