---

Step * of Lemma append_split2

∀[T:Type]
  ∀L:T List
    ∀[P:ℕ||L|| ⟶ ℙ]
      ((∀x:ℕ||L||. Dec(P x))
      ⇒ (∀i,j:ℕ||L||.  ((P i) ⇒ P j supposing i < j))
      ⇒ (∃L_1,L_2:T List. ((L = (L_1 @ L_2) ∈ (T List)) ∧ (∀i:ℕ||L||. (P i ⇐⇒ ||L_1|| ≤ i)))))
BY
{ ((Auto THEN Decide ∃i:ℕ||L||. ((P i) ∧ (∀j:ℕi. (¬(P j))))) THEN Auto) }

1
1. [T] : Type
2. L : T List
3. [P] : ℕ||L|| ⟶ ℙ
4. ∀x:ℕ||L||. Dec(P x)
5. ∀i,j:ℕ||L||.  ((P i) ⇒ P j supposing i < j)
6. ∃i:ℕ||L||. ((P i) ∧ (∀j:ℕi. (¬(P j))))
⊢ ∃L_1,L_2:T List. ((L = (L_1 @ L_2) ∈ (T List)) ∧ (∀i:ℕ||L||. (P i ⇐⇒ ||L_1|| ≤ i)))

2
1. [T] : Type
2. L : T List
3. [P] : ℕ||L|| ⟶ ℙ
4. ∀x:ℕ||L||. Dec(P x)
5. ∀i,j:ℕ||L||.  ((P i) ⇒ P j supposing i < j)
6. ¬(∃i:ℕ||L||. ((P i) ∧ (∀j:ℕi. (¬(P j)))))
⊢ ∃L_1,L_2:T List. ((L = (L_1 @ L_2) ∈ (T List)) ∧ (∀i:ℕ||L||. (P i ⇐⇒ ||L_1|| ≤ i)))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[P:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}x:\mBbbN{}||L||.  Dec(P  x))
            {}\mRightarrow{}  (\mforall{}i,j:\mBbbN{}||L||.    ((P  i)  {}\mRightarrow{}  P  j  supposing  i  <  j))
            {}\mRightarrow{}  (\mexists{}L$_{1}$,L$_{2}$:T  List.  ((L  =  (L$_{1\mbackslash{}\000Cff7d$  @  L$_{2}$))  \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  (P  i  \mLeftarrow{}{}\mRightarrow{}  ||L$_{1}$||  \mleq{}  i\000C)))))


By

---

Latex:
((Auto  THEN  Decide  \mexists{}i:\mBbbN{}||L||.  ((P  i)  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}(P  j)))))  THEN  Auto)

---

Home Index