Step
*
2
1
3
1
2
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)
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]))
BY
{ (((RWO "-4<" 0 THENA Auto) THEN (RWO "select-map" 0 THENA Auto)) THEN Reduce 0) }
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. [%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(let vs,a = bts[i]
in <map(f@0;vs)
, alpha-rename-aux(f@0;rev(vs) + bnds;a)
>)) + map(f@0;bnds);rev(fst(bts[i])) + bnds;snd(let vs,a = bts[i]
in <map(f@0;vs)
, alpha-rename-aux(f@0;rev(vs) + bnds;a)
>);snd(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
14. f = f
15. ||L|| = ||bts||
16. i : \mBbbN{}||L||
\mvdash{} alpha-aux(opr;rev(fst(L[i])) + map(f@0;bnds);rev(fst(bts[i])) + bnds;snd(L[i]);snd(bts[i]))
By
Latex:
(((RWO "-4<" 0 THENA Auto) THEN (RWO "select-map" 0 THENA Auto)) THEN Reduce 0)
Home
Index