---

Step * of Lemma isatom-implies-not-isint

∀[t:Base]. (¬↑isint(t)) supposing ((↑isatom(t)) and (t)↓)
BY
{ (CanonicalAuto
   THEN (Assert ⌜↑isint(t)⌝⋅ THENA Auto)
   THEN MoveToConcl (-3)
   THEN CanonicalAuto
   THEN Thin (-3)
   THEN RW (AddrC [1] isintReduceAtomC) (-2)
   THEN AllReduce
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(CanonicalAuto
  THEN  (Assert  \mkleeneopen{}\muparrow{}isint(t)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  CanonicalAuto
  THEN  Thin  (-3)
  THEN  RW  (AddrC  [1]  isintReduceAtomC)  (-2)
  THEN  AllReduce
  THEN  Auto)

---

Home Index