---

Step * 1 2 of Lemma last_with_property


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))
15. 0 < ||L1||
⊢ ∃i:ℕ||L||. ((P i) ∧ (∀j:ℕ||L||. ¬(P j) supposing i < j))
BY
{ (InstConcl [f1 (||L1|| - 1)] THEN Auto') }

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))
15. 0 < ||L1||
16. P (f1 (||L1|| - 1))
17. j : ℕ||L||
18. f1 (||L1|| - 1) < j
⊢ ¬(P j)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  [P]  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:\mBbbN{}||L||.  Dec(P  x)
5.  i  :  \mBbbN{}||L||
6.  P  i
7.  L1  :  T  List
8.  L2  :  T  List
9.  f1  :  \mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L||
10.  f2  :  \mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L||
11.  interleaving\_occurence(T;L1;L2;L;f1;f2)
12.  \mforall{}i:\mBbbN{}||L1||.  (P  (f1  i))
13.  \mforall{}i:\mBbbN{}||L2||.  (\mneg{}(P  (f2  i)))
14.  \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))
15.  0  <  ||L1||
\mvdash{}  \mexists{}i:\mBbbN{}||L||.  ((P  i)  \mwedge{}  (\mforall{}j:\mBbbN{}||L||.  \mneg{}(P  j)  supposing  i  <  j))


By

---

Latex:
(InstConcl  [f1  (||L1||  -  1)]  THEN  Auto')

---

Home Index