Step
*
2
1
3
1
2
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. [%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)
9. bnds ∈ {v:varname()| (v ∈ bnds)} List
10. λ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)
11. bts ∈ {bt:bound-term(opr)| (bt ∈ bts)} List
12. L : bound-term(opr) List
13. 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)
⊢ alpha-aux(opr;map(f@0;bnds);bnds;mkterm(f;L);mkterm(f;bts))
BY
{ (RWO "alpha-aux-mkterm" 0 THEN Auto) }
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
⊢ ||L|| = ||bts|| ∈ ℤ
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)
9. bnds ∈ {v:varname()| (v ∈ bnds)} List
10. λ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)
11. bts ∈ {bt:bound-term(opr)| (bt ∈ bts)} List
12. L : bound-term(opr) List
13. 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)
14. f = f ∈ opr
15. ||L|| = ||bts|| ∈ ℤ
16. i : ℕ||L||
⊢ alpha-aux(opr;rev(fst(L[i])) + map(f@0;bnds);rev(fst(bts[i])) + bnds;snd(L[i]);snd(bts[i]))
3
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])|| ∈ ℤ
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. [\%2] : ((\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. \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)
11. bts \mmember{} \{bt:bound-term(opr)| (bt \mmember{} bts)\} List
12. L : bound-term(opr) List
13. map(\mlambda{}bt.let vs,a = bt in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)>bts) = L
\mvdash{} alpha-aux(opr;map(f@0;bnds);bnds;mkterm(f;L);mkterm(f;bts))
By
Latex:
(RWO "alpha-aux-mkterm" 0 THEN Auto)
Home
Index