---

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

.....wf..... 
1. T : Type
2. L : T List
3. idxs : ℕ List
4. f : ℕ||L|| ⟶ ℕ||L||
⊢ Inj(ℕ||L||;ℕ||L||;f)
  ∧ ((L o λi.filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i])
    = (L o f)
    ∈ (T List)) ∈ ℙ
BY
{ Auto }

1
1. T : Type
2. L : T List
3. idxs : ℕ List
4. f : ℕ||L|| ⟶ ℕ||L||
5. Inj(ℕ||L||;ℕ||L||;f)
6. i : ℕ||L||
⊢ i < ||filter(λi.int-list-member(i;idxs);upto(||L||))|| + ||filter(λi.(¬bint-list-member(i;idxs));upto(||L||))||

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  L  :  T  List
3.  idxs  :  \mBbbN{}  List
4.  f  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||
\mvdash{}  Inj(\mBbbN{}||L||;\mBbbN{}||L||;f)
    \mwedge{}  ((L  o  \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])
        =  (L  o  f))  \mmember{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index