---

Step * of Lemma alpha-rename-binders-disjoint

No Annotations
∀[opr:Type]
  ∀L:varname() List. ∀t:term(opr). ∀f:{v:varname()| (v ∈ all-vars(t))}  ⟶ varname().
    ((∀x:{v:varname()| (v ∈ all-vars(t))} 
        ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
    ⇒ binders-disjoint(opr;L;alpha-rename(f;t)))
BY
{ ((RepeatFor 2 (Intro)
    THEN (Enough to prove ∀t:term(opr). ∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname().
                            ((∀x:{v:varname()| (v ∈ bnds @ all-vars(t))} 
                                ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
                            ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;t)))
           Because (ParallelLast
                    THEN (D -1 With ⌜[]⌝  THENA Auto)
                    THEN RepeatFor 2 ((ParallelLast THENA ParallelLast))
                    THEN Fold `alpha-rename` (-1)
                    THEN Trivial))
    )
   THEN (BLemma `term-induction` THENW Auto)
   THEN ((Intro
          THEN (Assert varterm(v) ∈ term(opr) BY
                      Auto)
          THEN DVar `v'
          THEN Auto
          THEN RepUR ``alpha-rename-aux`` 0
          THEN AutoSplit
          THEN RepUR ``binders-disjoint`` 0
          THEN Auto)
   ORELSE (Auto THEN Unfold `alpha-rename-aux` 0 THEN Reduce 0)
   )) }

1
1. [opr] : Type
2. L : varname() List
3. bts : bound-term(opr) List
4. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))}  ⟶ varname().
           ((∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))} 
               ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
           ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt))))))
5. f : opr
6. bnds : varname() List
7. f@0 : {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}  ⟶ varname()
8. ∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} 
     ((((f@0 x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f@0 x ∈ L)))
⊢ binders-disjoint(opr;L;eval bts' = eager-map(λbt.let vs,a = bt 
                                                   in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>;bts) in
                         mkterm(f;bts'))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}L:varname()  List.  \mforall{}t:term(opr).  \mforall{}f:\{v:varname()|  (v  \mmember{}  all-vars(t))\}    {}\mrightarrow{}  varname().
        ((\mforall{}x:\{v:varname()|  (v  \mmember{}  all-vars(t))\} 
                ((((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))  \mwedge{}  (\mneg{}(f  x  \mmember{}  L))))
        {}\mRightarrow{}  binders-disjoint(opr;L;alpha-rename(f;t)))


By

---

Latex:
((RepeatFor  2  (Intro)
    THEN  (Enough  to  prove  \mforall{}t:term(opr).  \mforall{}bnds:varname()  List.  \mforall{}f:\{v:varname()| 
                                                                                                                                (v  \mmember{}  bnds  @  all-vars(t))\} 
                                                                                                                              {}\mrightarrow{}  varname().
                                                    ((\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\} 
                                                            ((((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))  \mwedge{}  (\mneg{}(f  x  \mmember{}  L))))
                                                    {}\mRightarrow{}  binders-disjoint(opr;L;alpha-rename-aux(f;bnds;t)))
                  Because  (ParallelLast
                                    THEN  (D  -1  With  \mkleeneopen{}[]\mkleeneclose{}    THENA  Auto)
                                    THEN  RepeatFor  2  ((ParallelLast  THENA  ParallelLast))
                                    THEN  Fold  `alpha-rename`  (-1)
                                    THEN  Trivial))
    )
  THEN  (BLemma  `term-induction`  THENW  Auto)
  THEN  ((Intro
                THEN  (Assert  varterm(v)  \mmember{}  term(opr)  BY
                                        Auto)
                THEN  DVar  `v'
                THEN  Auto
                THEN  RepUR  ``alpha-rename-aux``  0
                THEN  AutoSplit
                THEN  RepUR  ``binders-disjoint``  0
                THEN  Auto)
  ORELSE  (Auto  THEN  Unfold  `alpha-rename-aux`  0  THEN  Reduce  0)
  ))

---

Home Index