---

Step * of Lemma subterm-varterm

No Annotations
∀[opr:Type]. ∀[s:term(opr)]. ∀[v:{v:varname()| ¬(v = nullvar() ∈ varname())} ].  (¬s << varterm(v))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (FLemma `subterm-size` [-1] THENA Auto)
   THEN Reduce -1
   THEN (Assert 1 ≤ term-size(s) BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[s:term(opr)].  \mforall{}[v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  ].    (\mneg{}s  <<  varterm(v))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (FLemma  `subterm-size`  [-1]  THENA  Auto)
  THEN  Reduce  -1
  THEN  (Assert  1  \mleq{}  term-size(s)  BY
                          Auto)
  THEN  Auto)

---

Home Index