---

Step * of Lemma split-by-indices

∀[T:Type]
  ∀L:T List. ∀ids:ℕ List.
    ∃L1,L2:T List. (permutation(T;L;L1 @ L2) ∧ (∃f:ℕ||L1|| ⟶ {i:ℕ||L||| (i ∈ ids)} . (Bij(ℕ||L1||;{i:ℕ||L||| (i ∈ ids)}\000C ;f) ∧ (∀j:ℕ||L1||. (L1[j] = L[f j] ∈ T)))))
BY
{ xxx(Auto
      THEN (InstLemma `index-split_property` [⌜T⌝;⌜L⌝;⌜ids⌝]⋅ THENA Auto)
      THEN InstConcl [ ⌜fst(index-split(L;ids))⌝;⌜snd(index-split(L;ids))⌝]⋅
      THEN Auto
      THEN Try (((GenConclAtAddr [1] THEN Complete (Auto)) ORELSE (GenConclAtAddr [2] THEN Complete (Auto))))
      THEN Thin (-1))xxx }

1
1. [T] : Type
2. L : T List
3. ids : ℕ List
⊢ permutation(T;L;(fst(index-split(L;ids))) @ (snd(index-split(L;ids))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}ids:\mBbbN{}  List.
        \mexists{}L1,L2:T  List
          (permutation(T;L;L1  @  L2)
          \mwedge{}  (\mexists{}f:\mBbbN{}||L1||  {}\mrightarrow{}  \{i:\mBbbN{}||L|||  (i  \mmember{}  ids)\}  .  (Bij(\mBbbN{}||L1||;\{i:\mBbbN{}||L|||  (i  \mmember{}  ids)\}  ;f)  \mwedge{}  (\mforall{}j:\mBbbN{}||L1||.  \000C(L1[j]  =  L[f  j])))))


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `index-split\_property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}ids\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  InstConcl  [  \mkleeneopen{}fst(index-split(L;ids))\mkleeneclose{};\mkleeneopen{}snd(index-split(L;ids))\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  Try  (((GenConclAtAddr  [1]  THEN  Complete  (Auto))
                            ORELSE  (GenConclAtAddr  [2]  THEN  Complete  (Auto))
                            ))
        THEN  Thin  (-1))xxx

---

Home Index