---

Step * of Lemma index-split-permutation

∀[T:Type]. ∀L:T List. ∀ids:ℕ List.  let L1,L2 = index-split(L;ids) in permutation(T;L;L1 @ L2)
BY
{ xxx(Auto
      THEN (InstLemma `permute-to-front-permutation` [⌜T⌝;⌜L⌝;⌜ids⌝]⋅ THENA Auto)
      THEN RepUR ``index-split let`` 0
      THEN ((GenConcl ⌜||filter(λi.int-list-member(i;ids);upto(||L||))|| = n ∈ ℕ||L|| + 1⌝⋅ THENM Thin (-1))
            THENA Auto'
            ))xxx }

1
.....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

2
1. [T] : Type
2. L : T List
3. ids : ℕ List
4. permutation(T;L;permute-to-front(L;ids))
5. n : ℕ||L|| + 1
⊢ permutation(T;L;firstn(n;permute-to-front(L;ids)) @ nth_tl(n;permute-to-front(L;ids)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}ids:\mBbbN{}  List.    let  L1,L2  =  index-split(L;ids)  in  permutation(T;L;L1  @  L2)


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `permute-to-front-permutation`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}ids\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  RepUR  ``index-split  let``  0
        THEN  ((GenConcl  \mkleeneopen{}||filter(\mlambda{}i.int-list-member(i;ids);upto(||L||))||  =  n\mkleeneclose{}\mcdot{}  THENM  Thin  (-1))
                    THENA  Auto'
                    ))xxx

---

Home Index