---

Step * of Lemma vars-of-subst-not-nullvar

No Annotations
∀[opr:Type]. ∀[s:(varname() × term(opr)) List].  (¬(nullvar() ∈ vars-of-subst(s)))
BY
{ (Auto
   THEN (GenConclTerm ⌜vars-of-subst(s)⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN MoveToConcl (-1)
   THEN GenConclTerm ⌜v[i]⌝⋅
   THEN Auto
   THEN D -3
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[s:(varname()  \mtimes{}  term(opr))  List].    (\mneg{}(nullvar()  \mmember{}  vars-of-subst(s)))


By

---

Latex:
(Auto
  THEN  (GenConclTerm  \mkleeneopen{}vars-of-subst(s)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerm  \mkleeneopen{}v[i]\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  -3
  THEN  Auto)

---

Home Index