---

Step * of Lemma subterm-size

No Annotations
∀[opr:Type]. ∀[s,t:term(opr)].  (s << t ⇒ term-size(s) < term-size(t))
BY
{ (Auto
   THEN Unfold `subterm` -1
   THEN ((InstLemma `transitive-closure-minimal-ext` [⌜term(opr)⌝;⌜λs,t. s < t⌝;⌜λs,t. term-size(s) < term-size(t)⌝]⋅
          THENA Auto
          )
   THENM (Fold `subterm-rel` (-1) THEN Auto)
   )
   THEN D 0
   THEN Reduce 0
   THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[s,t:term(opr)].    (s  <<  t  {}\mRightarrow{}  term-size(s)  <  term-size(t))


By

---

Latex:
(Auto
  THEN  Unfold  `subterm`  -1
  THEN  ((InstLemma  `transitive-closure-minimal-ext`  [\mkleeneopen{}term(opr)\mkleeneclose{};\mkleeneopen{}\mlambda{}s,t.  s  <  t\mkleeneclose{};
                \mkleeneopen{}\mlambda{}s,t.  term-size(s)  <  term-size(t)\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
  THENM  (Fold  `subterm-rel`  (-1)  THEN  Auto)
  )
  THEN  D  0
  THEN  Reduce  0
  THEN  EAuto  1)

---

Home Index