---

Step * of Lemma ispair-implies-not-isint

∀[t:Base]. (¬↑isint(t)) supposing ((↑ispair(t)) and (t)↓)
BY
{ (Auto
   THEN CanonicalTestCases
   THEN Auto
   THEN (Assert ⌜↑isint(t)⌝⋅ THENA Auto)
   THEN MoveToConcl (-3)
   THEN CanonicalTestCases
   THEN Reduce 0
   THEN Auto
   THEN HypSubst (-2) (-3)
   THEN Reduce (-3)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (\mneg{}\muparrow{}isint(t))  supposing  ((\muparrow{}ispair(t))  and  (t)\mdownarrow{})


By

---

Latex:
(Auto
  THEN  CanonicalTestCases
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}\muparrow{}isint(t)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  CanonicalTestCases
  THEN  Reduce  0
  THEN  Auto
  THEN  HypSubst  (-2)  (-3)
  THEN  Reduce  (-3)
  THEN  Trivial)

---

Home Index