---

Step * 1 2 1 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
19. P j
20. ∃j@0:ℕ||L2||. ((f2 j@0) = j ∈ ℤ) supposing ¬(P j)
21. j@0 : ℕ||L1||
22. (f1 j@0) = j ∈ ℤ
⊢ False
BY
{ (AllHyps (\i. (((Unfold `interleaving_occurence` i THEN ExRepD) THEN FwdThruLemma `increasing_implies` [i+1])
                 THENA 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. ||L|| = (||L1|| + ||L2||) ∈ ℕ
12. increasing(f1;||L1||)
13. ∀j:ℕ||L1||. (L1[j] = L[f1 j] ∈ T)
14. increasing(f2;||L2||)
15. ∀j:ℕ||L2||. (L2[j] = L[f2 j] ∈ T)
16. ∀j1:ℕ||L1||. ∀j2:ℕ||L2||.  (¬((f1 j1) = (f2 j2) ∈ ℤ))
17. ∀i:ℕ||L1||. (P (f1 i))
18. ∀i:ℕ||L2||. (¬(P (f2 i)))
19. ∀i:ℕ||L||. (((P i) ⇒ (∃j:ℕ||L1||. ((f1 j) = i ∈ ℤ))) ∧ ∃j:ℕ||L2||. ((f2 j) = i ∈ ℤ) supposing ¬(P i))
20. 0 < ||L1||
21. P (f1 (||L1|| - 1))
22. j : ℕ||L||
23. f1 (||L1|| - 1) < j
24. P j
25. ∃j@0:ℕ||L2||. ((f2 j@0) = j ∈ ℤ) supposing ¬(P j)
26. j@0 : ℕ||L1||
27. (f1 j@0) = j ∈ ℤ
28. ∀[x,y:ℕ||L1||].  f1 x < f1 y supposing x < y
⊢ 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
19.  P  j
20.  \mexists{}j@0:\mBbbN{}||L2||.  ((f2  j@0)  =  j)  supposing  \mneg{}(P  j)
21.  j@0  :  \mBbbN{}||L1||
22.  (f1  j@0)  =  j
\mvdash{}  False


By

---

Latex:
(AllHyps  (\mbackslash{}i.  (((Unfold  `interleaving\_occurence`  i  THEN  ExRepD)
                                THEN  FwdThruLemma  `increasing\_implies`  [i+1]
                                )
                              THENA  Auto
                              )))

---

Home Index