---

Step * 2 2 of Lemma permute-to-front-permutation


1. T : Type
2. L : T List
3. idxs : ℕ List
4. Inj(ℕ||L||;ℕ||L||;λi.filter(λi.int-list-member(i;idxs);upto(||L||))
                        @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i])
5. i : ℕ||L||
⊢ i < ||filter(λi.int-list-member(i;idxs);upto(||L||))|| + ||filter(λi.(¬bint-list-member(i;idxs));upto(||L||))||
BY
{ (RWW "length-append filter-split-length length_upto" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  idxs  :  \mBbbN{}  List
4.  Inj(\mBbbN{}||L||;\mBbbN{}||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])
5.  i  :  \mBbbN{}||L||
\mvdash{}  i  <  ||filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))||
+  ||filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||))||


By

---

Latex:
(RWW  "length-append  filter-split-length  length\_upto"  0  THEN  Auto)\mcdot{}

---

Home Index