---

Step * of Lemma interleaving_split

∀[T:Type]
  ∀L:T List
    ∀[P:ℕ||L|| ⟶ ℙ]
      ((∀x:ℕ||L||. Dec(P x))
      ⇒ (∃L1,L2:T List
           ∃f1:ℕ||L1|| ⟶ ℕ||L||
            ∃f2:ℕ||L2|| ⟶ ℕ||L||
             (interleaving_occurence(T;L1;L2;L;f1;f2)
             ∧ ((∀i:ℕ||L1||. (P (f1 i))) ∧ (∀i:ℕ||L2||. (¬(P (f2 i)))))
             ∧ (∀i:ℕ||L||
                  (((P i) ⇒ (∃j:ℕ||L1||. ((f1 j) = i ∈ ℤ))) ∧ ∃j:ℕ||L2||. ((f2 j) = i ∈ ℤ) supposing ¬(P i))))))
BY
{ (((Auto THEN InstLemma `increasing_split` [||L||;P]) THENA Auto) THEN ExRepD) }

1
1. [T] : Type
2. L : T List
3. [P] : ℕ||L|| ⟶ ℙ
4. ∀x:ℕ||L||. Dec(P x)
5. n : ℕ
6. k : ℕ
7. f : ℕn ⟶ ℕ||L||
8. g : ℕk ⟶ ℕ||L||
9. increasing(f;n)
10. increasing(g;k)
11. ∀i:ℕn. (P (f i))
12. ∀j:ℕk. (¬(P (g j)))
13. ∀i:ℕ||L||. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
⊢ ∃L1,L2:T List
   ∃f1:ℕ||L1|| ⟶ ℕ||L||
    ∃f2:ℕ||L2|| ⟶ ℕ||L||
     (interleaving_occurence(T;L1;L2;L;f1;f2)
     ∧ ((∀i:ℕ||L1||. (P (f1 i))) ∧ (∀i:ℕ||L2||. (¬(P (f2 i)))))
     ∧ (∀i:ℕ||L||. (((P i) ⇒ (∃j:ℕ||L1||. ((f1 j) = i ∈ ℤ))) ∧ ∃j:ℕ||L2||. ((f2 j) = i ∈ ℤ) supposing ¬(P i))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[P:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}x:\mBbbN{}||L||.  Dec(P  x))
            {}\mRightarrow{}  (\mexists{}L1,L2:T  List
                      \mexists{}f1:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L||
                        \mexists{}f2:\mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L||
                          (interleaving\_occurence(T;L1;L2;L;f1;f2)
                          \mwedge{}  ((\mforall{}i:\mBbbN{}||L1||.  (P  (f1  i)))  \mwedge{}  (\mforall{}i:\mBbbN{}||L2||.  (\mneg{}(P  (f2  i)))))
                          \mwedge{}  (\mforall{}i:\mBbbN{}||L||
                                    (((P  i)  {}\mRightarrow{}  (\mexists{}j:\mBbbN{}||L1||.  ((f1  j)  =  i)))
                                    \mwedge{}  \mexists{}j:\mBbbN{}||L2||.  ((f2  j)  =  i)  supposing  \mneg{}(P  i))))))


By

---

Latex:
(((Auto  THEN  InstLemma  `increasing\_split`  [||L||;P])  THENA  Auto)  THEN  ExRepD)

---

Home Index