---

Step * 1 2 1 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||
16. P (f1 (||L1|| - 1))
17. j : ℕ||L||
18. f1 (||L1|| - 1) < j
⊢ ¬(P j)
BY
{ (((((((D 0 THENA Auto) THEN InstHyp [j] (-6)) THENA Auto) THEN D (-1)) THEN D (-2)) 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))
15. 0 < ||L1||
16. P (f1 (||L1|| - 1))
17. j : ℕ||L||
18. f1 (||L1|| - 1) < j
19. P j
20. ∃j@0:ℕ||L2||. ((f2 j@0) = j ∈ ℤ) supposing ¬(P j)
21. j@0 : ℕ||L1||
22. (f1 j@0) = j ∈ ℤ
⊢ False

---

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||
16.  P  (f1  (||L1||  -  1))
17.  j  :  \mBbbN{}||L||
18.  f1  (||L1||  -  1)  <  j
\mvdash{}  \mneg{}(P  j)


By

---

Latex:
(((((((D  0  THENA  Auto)  THEN  InstHyp  [j]  (-6))  THENA  Auto)  THEN  D  (-1))  THEN  D  (-2))  THENA  Auto)
  THEN  ExRepD
  )

---

Home Index