---

Step * of Lemma binders-disjoint_wf

No Annotations
∀[opr:Type]. ∀[L:varname() List]. ∀[t:term(opr)].  (binders-disjoint(opr;L;t) ∈ ℙ)
BY
{ (RepeatFor 2 (Intro)
   THEN (Enough to prove ∀n:ℕ. ∀[a:term(opr)]. ((term-size(a) ≤ n) ⇒ (binders-disjoint(opr;L;a) ∈ ℙ))
          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 1 ≤ 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 `binders-disjoint` 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 Auto) THEN Fold `mkterm` (-1) THEN Reduce -1)
   THEN (D 4 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))⌝;⌜bt⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[L:varname()  List].  \mforall{}[t:term(opr)].    (binders-disjoint(opr;L;t)  \mmember{}  \mBbbP{})


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (Enough  to  prove  \mforall{}n:\mBbbN{}.  \mforall{}[a:term(opr)].  ((term-size(a)  \mleq{}  n)  {}\mRightarrow{}  (binders-disjoint(opr;L;a)  \mmember{}  \mBbbP{}))
                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  1  \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  `binders-disjoint`  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  Auto)  THEN  Fold  `mkterm`  (-1)  THEN  Reduce  -1)
  THEN  (D  4  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{}bt\mkleeneclose{}
              ]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index