---

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


1. T : Type
2. L : T List
3. idxs : ℕ List
⊢ l_disjoint(ℕ||L||;filter(λi.int-list-member(i;idxs);upto(||L||));filter(λi.(¬bint-list-member(i;idxs));upto(||L||)))
BY
{ (RepeatFor 2 ((D 0 THEN Auto))
   THEN ((RWO "member_filter" (-2) THENM (Reduce (-2) THEN D -2)) THENA Auto)
   THEN ((RWO "member_filter" (-1) THENM (Reduce (-1) THEN D -1)) THENA Auto)) }

1
1. T : Type
2. L : T List
3. idxs : ℕ List
4. x : ℕ||L||
5. (x ∈ upto(||L||))
6. ↑int-list-member(x;idxs)
7. (x ∈ upto(||L||))
8. ↑¬bint-list-member(x;idxs)
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  idxs  :  \mBbbN{}  List
\mvdash{}  l\_disjoint(\mBbbN{}||L||;filter(\mlambda{}i.int-list-member(i;idxs);
                                                      upto(||L||));filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||)))


By

---

Latex:
(RepeatFor  2  ((D  0  THEN  Auto))
  THEN  ((RWO  "member\_filter"  (-2)  THENM  (Reduce  (-2)  THEN  D  -2))  THENA  Auto)
  THEN  ((RWO  "member\_filter"  (-1)  THENM  (Reduce  (-1)  THEN  D  -1))  THENA  Auto))

---

Home Index