---

Step * of Lemma permute-to-front-permutation

∀[T:Type]. ∀L:T List. ∀idxs:ℕ List.  permutation(T;L;permute-to-front(L;idxs))
BY
{ (Auto
   THEN Unfold `permute-to-front` 0
   THEN With ⌜λi.filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i]⌝
    (D 0)⋅) }

1
.....wf..... 
1. T : Type
2. L : T List
3. idxs : ℕ List
⊢ λi.filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i] ∈ ℕ||L||
  ⟶ ℕ||L||

2
1. [T] : Type
2. L : T List
3. idxs : ℕ List
⊢ Inj(ℕ||L||;ℕ||L||;λi.filter(λi.int-list-member(i;idxs);upto(||L||))
                       @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i])
∧ ((L o λi.filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i])
  = (L o λi.filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i])
  ∈ (T List))

3
.....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)) ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}idxs:\mBbbN{}  List.    permutation(T;L;permute-to-front(L;idxs))


By

---

Latex:
(Auto
  THEN  Unfold  `permute-to-front`  0
  THEN  With  \mkleeneopen{}\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]\mkleeneclose{}  (D  0)\mcdot{})

---

Home Index