---

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


1. [T] : Type
2. L : T List
3. idxs : ℕ List
4. v : ℕ||L|| List
5. (filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||)))
= v
∈ (ℕ||L|| List)
⊢ Inj(ℕ||L||;ℕ||L||;λi.v[i])
BY
{ xxxAssert ⌜||L|| = ||v|| ∈ ℤ⌝⋅xxx }

1
.....assertion..... 
1. T : Type
2. L : T List
3. idxs : ℕ List
4. v : ℕ||L|| List
5. (filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||)))
= v
∈ (ℕ||L|| List)
⊢ ||L|| = ||v|| ∈ ℤ

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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  idxs  :  \mBbbN{}  List
4.  v  :  \mBbbN{}||L||  List
5.  (filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))
@  filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||)))
=  v
\mvdash{}  Inj(\mBbbN{}||L||;\mBbbN{}||L||;\mlambda{}i.v[i])


By

---

Latex:
xxxAssert  \mkleeneopen{}||L||  =  ||v||\mkleeneclose{}\mcdot{}xxx

---

Home Index