---

Step * of Lemma alpha-rename-equivalent

No Annotations
∀[opr:Type]
  ∀t:term(opr). ∀f:{v:varname()| (v ∈ all-vars(t))}  ⟶ varname().
    alpha-eq-terms(opr;alpha-rename(f;t);t) 
    supposing ((∀x:{v:varname()| (v ∈ all-vars(t))} . ((f x ∈ free-vars(t)) ⇒ ((f x) = x ∈ varname())))
    ∧ (∀x:{v:varname()| (v ∈ all-vars(t))} . (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
    ∧ Inj({v:varname()| (v ∈ all-vars(t))} ;varname();f)
BY
{ (Intro
   THEN (Enough to prove ∀t:term(opr). ∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname().
                           alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;t);t) 
                           supposing ((∀x:{v:varname()| (v ∈ bnds @ all-vars(t))} 
                                         ((f x ∈ free-vars-aux(bnds;t)) ⇒ ((f x) = x ∈ varname())))
                           ∧ (∀x:{v:varname()| (v ∈ bnds @ all-vars(t))} 
                                (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
                           ∧ Inj({v:varname()| (v ∈ bnds @ all-vars(t))} ;varname();f)
          Because (RepUR ``alpha-eq-terms alpha-rename free-vars`` 0
                   THEN (D 0 THENA Auto)
                   THEN (InstHyp [⌜t⌝;⌜[]⌝] 2⋅ THENA Auto)
                   THEN Reduce -1
                   THEN Trivial))
   THEN (Assert ∀t:term(opr). ∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname().
                  (map(f;bnds) ∈ varname() List) BY
               (RepeatFor 3 ((D 0 THENA Auto)) THEN (Assert bnds ∈ {v:varname()| (v ∈ bnds)}  List BY Auto) THEN Auto))
   THEN (BLemma `term-induction` THENW Auto)
   THEN Try ((Intro THEN (Assert varterm(v) ∈ term(opr) BY Auto) THEN DVar `v'))
   THEN Intros) }

1
1. [opr] : Type
2. ∀t:term(opr). ∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname().
     (map(f;bnds) ∈ varname() List)
3. v : varname()
4. [%3] : ¬(v = nullvar() ∈ varname())
5. varterm(v) ∈ term(opr)
6. bnds : varname() List
7. f : {v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))}  ⟶ varname()
8. [%] : ((∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
             ((f x ∈ free-vars-aux(bnds;varterm(v))) ⇒ ((f x) = x ∈ varname())))
∧ (∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
     (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
∧ Inj({v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} ;varname();f)
⊢ alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;varterm(v));varterm(v))

2
1. [opr] : Type
2. ∀t:term(opr). ∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname().
     (map(f;bnds) ∈ 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().
           alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;snd(bt));snd(bt)) 
           supposing ((∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))} 
                         ((f x ∈ free-vars-aux(bnds;snd(bt))) ⇒ ((f x) = x ∈ varname())))
           ∧ (∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))} 
                (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
           ∧ Inj({v:varname()| (v ∈ bnds @ all-vars(snd(bt)))} ;varname();f)))
5. f : opr
6. bnds : varname() List
7. f@0 : {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}  ⟶ varname()
8. [%2] : ((∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} 
              ((f@0 x ∈ free-vars-aux(bnds;mkterm(f;bts))) ⇒ ((f@0 x) = x ∈ varname())))
∧ (∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} 
     (((f@0 x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
∧ Inj({v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} ;varname();f@0)
⊢ alpha-aux(opr;map(f@0;bnds);bnds;alpha-rename-aux(f@0;bnds;mkterm(f;bts));mkterm(f;bts))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}t:term(opr).  \mforall{}f:\{v:varname()|  (v  \mmember{}  all-vars(t))\}    {}\mrightarrow{}  varname().
        alpha-eq-terms(opr;alpha-rename(f;t);t) 
        supposing  ((\mforall{}x:\{v:varname()|  (v  \mmember{}  all-vars(t))\}  .  ((f  x  \mmember{}  free-vars(t))  {}\mRightarrow{}  ((f  x)  =  x)))
        \mwedge{}  (\mforall{}x:\{v:varname()|  (v  \mmember{}  all-vars(t))\}  .  (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))))
        \mwedge{}  Inj(\{v:varname()|  (v  \mmember{}  all-vars(t))\}  ;varname();f)


By

---

Latex:
(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().
                                                  alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;t);t) 
                                                  supposing  ((\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\} 
                                                                              ((f  x  \mmember{}  free-vars-aux(bnds;t))  {}\mRightarrow{}  ((f  x)  =  x)))
                                                  \mwedge{}  (\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\} 
                                                            (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))))
                                                  \mwedge{}  Inj(\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\}  ;varname();f)
                Because  (RepUR  ``alpha-eq-terms  alpha-rename  free-vars``  0
                                  THEN  (D  0  THENA  Auto)
                                  THEN  (InstHyp  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
                                  THEN  Reduce  -1
                                  THEN  Trivial))
  THEN  (Assert  \mforall{}t:term(opr).  \mforall{}bnds:varname()  List.  \mforall{}f:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\} 
                                                                                                          {}\mrightarrow{}  varname().
                                (map(f;bnds)  \mmember{}  varname()  List)  BY
                          (RepeatFor  3  ((D  0  THENA  Auto))
                            THEN  (Assert  bnds  \mmember{}  \{v:varname()|  (v  \mmember{}  bnds)\}    List  BY
                                                    Auto)
                            THEN  Auto))
  THEN  (BLemma  `term-induction`  THENW  Auto)
  THEN  Try  ((Intro  THEN  (Assert  varterm(v)  \mmember{}  term(opr)  BY  Auto)  THEN  DVar  `v'))
  THEN  Intros)

---

Home Index