---

Step * 1 2 of Lemma max-of-intset


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))))
BY
{ !two_place_expr{(, THENL ,)}((Unfold `decidable` -1 THEN D -1);((OrRight THENA Auto)
                                                                  THEN (InstConcl [⌈0⌉])⋅
                                                                  THEN Auto); ((OrLeft THENA Auto) THEN D 0 THEN Auto) 
                                                                              THEN !two_place_expr{(, THENL ,)}(Assert 
                                                                                     ⌈y = 0 ∈ ℤ⌉⋅;Auto; (HypSubst' -1 0
                                                                                                         THEN Trivial
                                                                                                         ))) }

---

Latex:



1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}n:\mBbbN{}.  Dec(P[n])@i
3.  Dec(P[0])
\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

!two\_place\_expr\{(,  THENL  ,)\}((Unfold  `decidable`  -1  THEN  D  -1);
    ((OrRight  THENA  Auto)
      THEN  (InstConcl  [\mkleeneopen{}0\mkleeneclose{}])\mcdot{}
      THEN  Auto);  ((OrLeft  THENA  Auto)  THEN  D  0  THEN  Auto) 
                              THEN  !two\_place\_expr\{(,  THENL  ,)\}(Assert  \mkleeneopen{}y  =  0\mkleeneclose{}\mcdot{};Auto;  (HypSubst'  -1  0
                                                                                                                                                THEN  Trivial
                                                                                                                                                )))

---

Home Index