---

Step * of Lemma last_with_property

∀[T:Type]
  ∀L:T List
    ∀[P:ℕ||L|| ⟶ ℙ]
      ((∀x:ℕ||L||. Dec(P x)) ⇒ (∃i:ℕ||L||. (P i)) ⇒ (∃i:ℕ||L||. ((P i) ∧ (∀j:ℕ||L||. ¬(P j) supposing i < j))))
BY
{ TACTIC:(((Auto' THEN InstLemma `interleaving_split` [T;L;P]⋅) THENA Auto) THEN ExRepD) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[P:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}x:\mBbbN{}||L||.  Dec(P  x))
            {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||L||.  (P  i))
            {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||L||.  ((P  i)  \mwedge{}  (\mforall{}j:\mBbbN{}||L||.  \mneg{}(P  j)  supposing  i  <  j))))


By

---

Latex:
TACTIC:(((Auto'  THEN  InstLemma  `interleaving\_split`  [T;L;P]\mcdot{})  THENA  Auto)  THEN  ExRepD)

---

Home Index