---

Step * 1 1 of Lemma last_with_property

.....assertion..... 
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))
⊢ 0 < ||L1||
BY
{ ((((((InstHyp [i] (-1) THENA Auto) THEN D (-1)) THEN D (-2)) THENA Auto) THEN ExRepD) THEN Auto') }

---

Latex:

---

Latex:
.....assertion..... 
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))
\mvdash{}  0  <  ||L1||


By

---

Latex:
((((((InstHyp  [i]  (-1)  THENA  Auto)  THEN  D  (-1))  THEN  D  (-2))  THENA  Auto)  THEN  ExRepD)  THEN  Auto')

---

Home Index