---

Step * of Lemma imax-wf-partial-nat

∀[x,y:partial(ℕ)].  (imax(x;y) ∈ partial(ℕ))
BY
{ ((Assert partial(Base) ⊆r Base BY
          Auto)
   THEN (Assert partial(ℕ) ⊆r Base BY
               Auto)
   THEN ((InstLemma `apply-2-partial` [⌜ℕ⌝;⌜ℕ⌝;⌜ℕ⌝;⌜λx,y. imax(x;y)⌝]⋅ THENM (Reduce -1 THEN Hypothesis))
         THENA (Reduce 0 THEN Auto THEN Try ((Unfold `imax` 5 THEN Complete (RepeatFor 2 ((D 5 THEN Auto))))))
         )⋅) }

1
1. partial(Base) ⊆r Base
2. partial(ℕ) ⊆r Base
3. a : partial(ℕ)
4. b : partial(ℕ)
5. ¬is-exception(a)
6. ¬is-exception(b)
⊢ ¬is-exception(imax(a;b))

---

Latex:

---

Latex:
\mforall{}[x,y:partial(\mBbbN{})].    (imax(x;y)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
((Assert  partial(Base)  \msubseteq{}r  Base  BY
                Auto)
  THEN  (Assert  partial(\mBbbN{})  \msubseteq{}r  Base  BY
                          Auto)
  THEN  ((InstLemma  `apply-2-partial`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  imax(x;y)\mkleeneclose{}]\mcdot{}  THENM  (Reduce  -1  THEN  Hypothesi\000Cs))
              THENA  (Reduce  0
                            THEN  Auto
                            THEN  Try  ((Unfold  `imax`  5  THEN  Complete  (RepeatFor  2  ((D  5  THEN  Auto))))))
              )\mcdot{})

---

Home Index