---

Step * of Lemma sq-decider-name-deq

sq-decider(NameDeq)
BY
{ (Unfold `name-deq` 0
   THEN BLemma `sq-decider-list-deq`
   THEN Try (Complete (Auto))
   THEN D 0
   THEN (UnivCD THENA Auto)
   THEN Try ((BLemma `atom-deq-symmetry`⋅ THEN Auto))
   THEN BLemma `sq-decider-atom-deq`) }

---

Latex:

---

Latex:
sq-decider(NameDeq)


By

---

Latex:
(Unfold  `name-deq`  0
  THEN  BLemma  `sq-decider-list-deq`
  THEN  Try  (Complete  (Auto))
  THEN  D  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  ((BLemma  `atom-deq-symmetry`\mcdot{}  THEN  Auto))
  THEN  BLemma  `sq-decider-atom-deq`)

---

Home Index