---

Step * 1 of Lemma index-split-permutation

.....wf..... 
1. [T] : Type
2. L : T List
3. ids : ℕ List
4. permutation(T;L;permute-to-front(L;ids))
⊢ ||filter(λi.int-list-member(i;ids);upto(||L||))|| ∈ ℕ||L|| + 1
BY
{ xxx((InstLemma `length-filter` [⌜ℤ⌝;⌜λi.int-list-member(i;ids)⌝;⌜upto(||L||)⌝]⋅ THENA Auto)
      THEN RWO "length_upto" (-1)
      THEN Auto
      THEN Auto')xxx }

---

Latex:

---

Latex:
.....wf..... 
1.  [T]  :  Type
2.  L  :  T  List
3.  ids  :  \mBbbN{}  List
4.  permutation(T;L;permute-to-front(L;ids))
\mvdash{}  ||filter(\mlambda{}i.int-list-member(i;ids);upto(||L||))||  \mmember{}  \mBbbN{}||L||  +  1


By

---

Latex:
xxx((InstLemma  `length-filter`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}i.int-list-member(i;ids)\mkleeneclose{};\mkleeneopen{}upto(||L||)\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  RWO  "length\_upto"  (-1)
        THEN  Auto
        THEN  Auto')xxx

---

Home Index