---

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


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()))
9. ∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} 
     (((f@0 x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
10. Inj({v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} ;varname();f@0)
11. bnds ∈ {v:varname()| (v ∈ bnds)}  List
12. λbt.let vs,a = bt 
        in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> ∈ {bt:bound-term(opr)| (bt ∈ bts)}  ⟶ bound-term(opr)
13. bts ∈ {bt:bound-term(opr)| (bt ∈ bts)}  List
14. L : bound-term(opr) List
15. map(λbt.let vs,a = bt in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>;bts) = L ∈ (bound-term(opr) List)
16. f = f ∈ opr
17. ||L|| = ||bts|| ∈ ℤ
18. i : ℕ||L||
19. alpha-aux(opr;rev(fst(L[i])) + map(f@0;bnds);rev(fst(bts[i])) + bnds;snd(L[i]);snd(bts[i]))
⊢ ||fst(L[i])|| = ||fst(bts[i])|| ∈ ℤ
BY
{ (((StrengthenEquation (-5) THEN ApFunToHypEquands `Z' ⌜Z[i]⌝ ⌜bound-term(opr)⌝ (-1)⋅)
    THENA (Auto THEN D -1 THEN Unhide THEN D -1 THEN RWO  "-1" 0 THEN Auto)
    )
   THEN (RWO "select-map" (-1) THENA Auto)
   THEN Reduce -1) }

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. 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()))
9. ∀x:{v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} 
     (((f@0 x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
10. Inj({v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))} ;varname();f@0)
11. bnds ∈ {v:varname()| (v ∈ bnds)}  List
12. λbt.let vs,a = bt 
        in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> ∈ {bt:bound-term(opr)| (bt ∈ bts)}  ⟶ bound-term(opr)
13. bts ∈ {bt:bound-term(opr)| (bt ∈ bts)}  List
14. L : bound-term(opr) List
15. map(λbt.let vs,a = bt in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>;bts) = L ∈ (bound-term(opr) List)
16. f = f ∈ opr
17. ||L|| = ||bts|| ∈ ℤ
18. i : ℕ||L||
19. alpha-aux(opr;rev(fst(L[i])) + map(f@0;bnds);rev(fst(bts[i])) + bnds;snd(L[i]);snd(bts[i]))
20. map(λbt.let vs,a = bt 
            in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>;bts)
= L
∈ {z:bound-term(opr) List| 
   (z = map(λbt.let vs,a = bt in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>;bts) ∈ (bound-term(opr) List))
   ∧ (z = L ∈ (bound-term(opr) List))} 
21. let vs,a = bts[i] in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> = L[i] ∈ bound-term(opr)
⊢ ||fst(L[i])|| = ||fst(bts[i])|| ∈ ℤ

---

Latex:

---

Latex:

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))
9.  \mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\} 
          (((f@0  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))
10.  Inj(\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\}  ;varname();f@0)
11.  bnds  \mmember{}  \{v:varname()|  (v  \mmember{}  bnds)\}    List
12.  \mlambda{}bt.let  vs,a  =  bt 
                in  <map(f@0;vs),  alpha-rename-aux(f@0;rev(vs)  +  bnds;a)>  \mmember{}  \{bt:bound-term(opr)|  (bt  \mmember{}  bts)\}  \000C  {}\mrightarrow{}  bound-term(opr)
13.  bts  \mmember{}  \{bt:bound-term(opr)|  (bt  \mmember{}  bts)\}    List
14.  L  :  bound-term(opr)  List
15.  map(\mlambda{}bt.let  vs,a  =  bt  in  <map(f@0;vs),  alpha-rename-aux(f@0;rev(vs)  +  bnds;a)>bts)  =  L
16.  f  =  f
17.  ||L||  =  ||bts||
18.  i  :  \mBbbN{}||L||
19.  alpha-aux(opr;rev(fst(L[i]))  +  map(f@0;bnds);rev(fst(bts[i]))  +  bnds;snd(L[i]);snd(bts[i]))
\mvdash{}  ||fst(L[i])||  =  ||fst(bts[i])||


By

---

Latex:
(((StrengthenEquation  (-5)  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z[i]\mkleeneclose{}  \mkleeneopen{}bound-term(opr)\mkleeneclose{}  (-1)\mcdot{})
    THENA  (Auto  THEN  D  -1  THEN  Unhide  THEN  D  -1  THEN  RWO    "-1"  0  THEN  Auto)
    )
  THEN  (RWO  "select-map"  (-1)  THENA  Auto)
  THEN  Reduce  -1)

---

Home Index