---

Step * 1 of Lemma max-of-intset

.....basecase..... 
1. [P] : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
⊢ (∀y:ℕ. ¬P[y] supposing y ≤ 0) ∨ (∃y:ℕ. ((y ≤ 0) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ 0))))
BY
{ Assert ⌈Dec(P[0])⌉⋅ }

1
.....assertion..... 
1. [P] : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
⊢ Dec(P[0])

2
1. [P] : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. Dec(P[0])
⊢ (∀y:ℕ. ¬P[y] supposing y ≤ 0) ∨ (∃y:ℕ. ((y ≤ 0) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ 0))))

---

Latex:


.....basecase..... 
1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}n:\mBbbN{}.  Dec(P[n])@i
\mvdash{}  (\mforall{}y:\mBbbN{}.  \mneg{}P[y]  supposing  y  \mleq{}  0)  \mvee{}  (\mexists{}y:\mBbbN{}.  ((y  \mleq{}  0)  \mwedge{}  P[y]  \mwedge{}  (\mforall{}x:\mBbbN{}.  \mneg{}P[x]  supposing  y  <  x  \mwedge{}  (x  \mleq{}  0))))


By

Assert  \mkleeneopen{}Dec(P[0])\mkleeneclose{}\mcdot{}

---

Home Index