---

Step * 2 1 1 of Lemma alpha-rename-equivalent

.....aux..... 
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. ((∀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)
9. bnds ∈ {v:varname()| (v ∈ bnds)}  List
10. bts ∈ {bt:bound-term(opr)| (bt ∈ bts)}  List
11. b1 : varname() List
12. b2 : term(opr)
13. (<b1, b2> ∈ bts)
⊢ map(f@0;b1) ∈ varname() List
BY
{ ((Enough to prove {v:varname()| (v ∈ b1)}  ⊆r {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} 
     Because ((Assert b1 ∈ {v:varname()| (v ∈ b1)}  List BY Auto) THEN MemCD THEN Auto))
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (MemTypeCD THENW Auto)
   THEN Try (Trivial)
   THEN GenListD 0
   THEN (OrRight THENA Auto)
   THEN (RWO "member-all-vars-mkterm" 0 THENA Auto)
   THEN D 0 With ⌜<b1, b2>⌝ 
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  opr  :  Type
2.  \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)
3.  bts  :  bound-term(opr)  List
4.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\mforall{}bnds:varname()  List.  \mforall{}f:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(snd(bt)))\}    {}\mrightarrow{}  varname().
                      alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;snd(bt));snd(bt)) 
                      supposing  ((\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(snd(bt)))\} 
                                                  ((f  x  \mmember{}  free-vars-aux(bnds;snd(bt)))  {}\mRightarrow{}  ((f  x)  =  x)))
                      \mwedge{}  (\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(snd(bt)))\} 
                                (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))))
                      \mwedge{}  Inj(\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(snd(bt)))\}  ;varname();f)))
5.  f  :  opr
6.  bnds  :  varname()  List
7.  f@0  :  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\}    {}\mrightarrow{}  varname()
8.  ((\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\} 
              ((f@0  x  \mmember{}  free-vars-aux(bnds;mkterm(f;bts)))  {}\mRightarrow{}  ((f@0  x)  =  x)))
\mwedge{}  (\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\} 
          (((f@0  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))))
\mwedge{}  Inj(\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\}  ;varname();f@0)
9.  bnds  \mmember{}  \{v:varname()|  (v  \mmember{}  bnds)\}    List
10.  bts  \mmember{}  \{bt:bound-term(opr)|  (bt  \mmember{}  bts)\}    List
11.  b1  :  varname()  List
12.  b2  :  term(opr)
13.  (<b1,  b2>  \mmember{}  bts)
\mvdash{}  map(f@0;b1)  \mmember{}  varname()  List


By

---

Latex:
((Enough  to  prove  \{v:varname()|  (v  \mmember{}  b1)\}    \msubseteq{}r  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\} 
      Because  ((Assert  b1  \mmember{}  \{v:varname()|  (v  \mmember{}  b1)\}    List  BY  Auto)  THEN  MemCD  THEN  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Try  (Trivial)
  THEN  GenListD  0
  THEN  (OrRight  THENA  Auto)
  THEN  (RWO  "member-all-vars-mkterm"  0  THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}<b1,  b2>\mkleeneclose{} 
  THEN  Reduce  0
  THEN  Auto)

---

Home Index