---

Step * 1 2 1 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. ||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
BY
{ (Decide j@0 < ||L1|| - 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
29. j@0 < ||L1|| - 1
⊢ False

2
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
29. ¬j@0 < ||L1|| - 1
⊢ 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.  ||L||  =  (||L1||  +  ||L2||)
12.  increasing(f1;||L1||)
13.  \mforall{}j:\mBbbN{}||L1||.  (L1[j]  =  L[f1  j])
14.  increasing(f2;||L2||)
15.  \mforall{}j:\mBbbN{}||L2||.  (L2[j]  =  L[f2  j])
16.  \mforall{}j1:\mBbbN{}||L1||.  \mforall{}j2:\mBbbN{}||L2||.    (\mneg{}((f1  j1)  =  (f2  j2)))
17.  \mforall{}i:\mBbbN{}||L1||.  (P  (f1  i))
18.  \mforall{}i:\mBbbN{}||L2||.  (\mneg{}(P  (f2  i)))
19.  \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))
20.  0  <  ||L1||
21.  P  (f1  (||L1||  -  1))
22.  j  :  \mBbbN{}||L||
23.  f1  (||L1||  -  1)  <  j
24.  P  j
25.  \mexists{}j@0:\mBbbN{}||L2||.  ((f2  j@0)  =  j)  supposing  \mneg{}(P  j)
26.  j@0  :  \mBbbN{}||L1||
27.  (f1  j@0)  =  j
28.  \mforall{}[x,y:\mBbbN{}||L1||].    f1  x  <  f1  y  supposing  x  <  y
\mvdash{}  False


By

---

Latex:
(Decide  j@0  <  ||L1||  -  1  THENA  Auto)

---

Home Index