Step
*
2
1
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
⊢ alpha-aux(opr;map(f@0;bnds);bnds;eval bts' = eager-map(λbt.let vs,a = bt
in <map(f@0;vs)
, alpha-rename-aux(f@0;rev(vs) + bnds;a)
>;bts) in
mkterm(f;bts');mkterm(f;bts))
BY
{ (Assert λ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\000C(opr) BY
((Assert bts ∈ {bt:bound-term(opr)| (bt ∈ bts)} List BY
Auto)
THEN (MemCD THENL [(D -1 THEN D -2 THEN Reduce 0 THEN Unfold `bound-term` 0 THEN MemCD); Auto])
)) }
1
.....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
2
.....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)
⊢ alpha-rename-aux(f@0;rev(b1) + bnds;b2) ∈ term(opr)
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. [%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)
⊢ alpha-aux(opr;map(f@0;bnds);bnds;eval bts' = eager-map(λbt.let vs,a = bt
in <map(f@0;vs)
, alpha-rename-aux(f@0;rev(vs) + bnds;a)
>;bts) in
mkterm(f;bts');mkterm(f;bts))
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
\mvdash{} alpha-aux(opr;map(f@0;
bnds);bnds;eval bts' = eager-map(\mlambda{}bt.let vs,a = bt
in <map(f@0;vs)
, alpha-rename-aux(f@0;rev(vs) + bnds;a)
>bts) in
mkterm(f;bts');mkterm(f;bts))
By
Latex:
(Assert \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)\} {}\mrightarrow{} bound-term(o\000Cpr) BY
((Assert bts \mmember{} \{bt:bound-term(opr)| (bt \mmember{} bts)\} List BY
Auto)
THEN (MemCD
THENL [(D -1 THEN D -2 THEN Reduce 0 THEN Unfold `bound-term` 0 THEN MemCD); Auto]
)
))
Home
Index