---

Step * of Lemma has-value-implies-dec-isatom-2

∀t:Base. ((t)↓ ⇒ ((t ∈ Atom) ∨ (∀a,b:Base.  (if t is an atom then a otherwise b ~ b))))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `has-value-implies-dec-isatom` [⌜t⌝;⌜0⌝;⌜1⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN CanonicalTestCases
   THEN Auto
   THEN Reduce 3
   THEN Auto
   THEN FLemma `not_zero_sqequal_one` [3]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}t:Base.  ((t)\mdownarrow{}  {}\mRightarrow{}  ((t  \mmember{}  Atom)  \mvee{}  (\mforall{}a,b:Base.    (if  t  is  an  atom  then  a  otherwise  b  \msim{}  b))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `has-value-implies-dec-isatom`  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  CanonicalTestCases
  THEN  Auto
  THEN  Reduce  3
  THEN  Auto
  THEN  FLemma  `not\_zero\_sqequal\_one`  [3]
  THEN  Auto)

---

Home Index