---

Step * of Lemma max-of-intset

∀[P:ℕ ─→ ℙ]
  ((∀n:ℕ. Dec(P[n]))
  ⇒ (∀n:ℕ. ((∀y:ℕ. ¬P[y] supposing y ≤ n) ∨ (∃y:ℕ. ((y ≤ n) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ n)))))))
BY
{ ((RepeatFor 3 ((D 0 THENA Auto)))⋅ THEN (NatInd (-1)) THEN Auto) }

1
.....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))))

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

---

Latex:


\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}n:\mBbbN{}.  Dec(P[n]))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}
                ((\mforall{}y:\mBbbN{}.  \mneg{}P[y]  supposing  y  \mleq{}  n)
                \mvee{}  (\mexists{}y:\mBbbN{}.  ((y  \mleq{}  n)  \mwedge{}  P[y]  \mwedge{}  (\mforall{}x:\mBbbN{}.  \mneg{}P[x]  supposing  y  <  x  \mwedge{}  (x  \mleq{}  n)))))))


By

((RepeatFor  3  ((D  0  THENA  Auto)))\mcdot{}  THEN  (NatInd  (-1))  THEN  Auto)

---

Home Index