Step * of Lemma imax-wf-partial

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

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


Latex:


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


By


Latex:
((Assert  partial(Base)  \msubseteq{}r  Base  BY
                Auto)
  THEN  (Assert  partial(\mBbbZ{})  \msubseteq{}r  Base  BY
                          Auto)
  THEN  ((InstLemma  `apply-2-partial`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\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