---

Step * of Lemma var-num_wf

No Annotations
∀[t:Atom]. ∀[b:varname()].  (var-num(t;b) ∈ {-1...})
BY
{ (Auto THEN D -1 THEN Try (DProdsAndUnions) THEN RepUR ``var-num`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[t:Atom].  \mforall{}[b:varname()].    (var-num(t;b)  \mmember{}  \{-1...\})


By

---

Latex:
(Auto  THEN  D  -1  THEN  Try  (DProdsAndUnions)  THEN  RepUR  ``var-num``  0  THEN  AutoSplit)

---

Home Index