---

Step * of Lemma free-vars-aux_wf

No Annotations
∀[opr:Type]. ∀[t:term(opr)]. ∀[bnds:varname() List].
  (free-vars-aux(bnds;t) ∈ {v:varname()| ¬(v = nullvar() ∈ varname())}  List)
BY
{ (Intro
   THEN (Enough to prove ∀n:ℕ
                           ∀[a:term(opr)]
                             ((term-size(a) ≤ n)
                             ⇒ (∀[bnds:varname() List]
                                   (free-vars-aux(bnds;a) ∈ {v:varname()| ¬(v = nullvar() ∈ varname())}  List)))
          Because ((D 0 THENA Auto) THEN (D -2 With ⌜term-size(t)⌝  THENA Auto) THEN InstHyp [⌜t⌝] (-1)⋅ THEN Auto))
   THEN CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN (InstLemma `term-ext` [⌜opr⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜a = t ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN (Assert t ∈ term(opr) BY
               Auto)
   THEN (Assert 0 ≤ term-size(t) BY
               Auto)
   THEN RepeatFor 2 (D -3)
   THEN Folds  ``varterm mkterm`` (-1)
   THEN Reduce -1
   THEN Folds  ``varterm mkterm`` 0
   THEN Reduce 0
   THEN Unfold `free-vars-aux` 0
   THEN Reduce 0
   THEN Try ((Assert y2 ∈ {bt:varname() List × term(opr)| (bt ∈ y2)}  List BY Auto))
   THEN Auto
   THEN ((Assert 1 ≤ term-size(inr <y1, y2> ) BY (Fold `mkterm` 0 THEN Auto)) THEN Fold `mkterm` (-1) THEN Reduce -1)
   THEN (D 3 With ⌜n - 1⌝  THENA Auto)
   THEN BHyp -1
   THEN Auto
   THEN (InstLemma `summand-le-lsum` [⌜varname() List × term(opr)⌝;⌜y2⌝;⌜λ2bt.term-size(snd(bt))⌝;⌜<b1, b2>⌝]⋅
         THENA Auto
         )
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t:term(opr)].  \mforall{}[bnds:varname()  List].
    (free-vars-aux(bnds;t)  \mmember{}  \{v:varname()|  \mneg{}(v  =  nullvar())\}    List)


By

---

Latex:
(Intro
  THEN  (Enough  to  prove  \mforall{}n:\mBbbN{}
                                                  \mforall{}[a:term(opr)]
                                                      ((term-size(a)  \mleq{}  n)
                                                      {}\mRightarrow{}  (\mforall{}[bnds:varname()  List]
                                                                  (free-vars-aux(bnds;a)  \mmember{}  \{v:varname()|  \mneg{}(v  =  nullvar())\}    List)))
                Because  ((D  0  THENA  Auto)
                                  THEN  (D  -2  With  \mkleeneopen{}term-size(t)\mkleeneclose{}    THENA  Auto)
                                  THEN  InstHyp  [\mkleeneopen{}t\mkleeneclose{}]  (-1)\mcdot{}
                                  THEN  Auto))
  THEN  CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `term-ext`  [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}a  =  t\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  (Assert  t  \mmember{}  term(opr)  BY
                          Auto)
  THEN  (Assert  0  \mleq{}  term-size(t)  BY
                          Auto)
  THEN  RepeatFor  2  (D  -3)
  THEN  Folds    ``varterm  mkterm``  (-1)
  THEN  Reduce  -1
  THEN  Folds    ``varterm  mkterm``  0
  THEN  Reduce  0
  THEN  Unfold  `free-vars-aux`  0
  THEN  Reduce  0
  THEN  Try  ((Assert  y2  \mmember{}  \{bt:varname()  List  \mtimes{}  term(opr)|  (bt  \mmember{}  y2)\}    List  BY  Auto))
  THEN  Auto
  THEN  ((Assert  1  \mleq{}  term-size(inr  <y1,  y2>  )  BY  (Fold  `mkterm`  0  THEN  Auto))  THEN  Fold  `mkterm`  (-1)  \000CTHEN  Reduce  -1)
  THEN  (D  3  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
  THEN  BHyp  -1
  THEN  Auto
  THEN  (InstLemma  `summand-le-lsum`  [\mkleeneopen{}varname()  List  \mtimes{}  term(opr)\mkleeneclose{};\mkleeneopen{}y2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bt.term-size(snd(bt))\mkleeneclose{};
              \mkleeneopen{}<b1,  b2>\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index