Step
*
2
of Lemma
subst-term_functionality
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. ∀bt:bound-term(opr)
((bt ∈ bts)
⇒ (∀B:term(opr). ∀bnds1,bnds2:varname() List.
(l_disjoint(varname();bnds1;vars-of-subst(s1))
⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
⇒ alpha-aux(opr;bnds1;bnds2;snd(bt);B)
⇒ binders-disjoint(opr;vars-of-subst(s1);snd(bt))
⇒ binders-disjoint(opr;vars-of-subst(s2);B)
⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. ∀bt:bound-term(opr)
((bt ∈ b1)
⇒ (∀bnds1,bnds2:varname() List.
(l_disjoint(varname();bnds1;vars-of-subst(s1))
⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
⇒ alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
⇒ binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
⇒ binders-disjoint(opr;vars-of-subst(s2);snd(bt))
⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l_disjoint(varname();bnds1;vars-of-subst(s1))
14. l_disjoint(varname();bnds2;vars-of-subst(s2))
15. alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);mkterm(f1;b1))
16. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
17. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
⊢ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;mkterm(f1;b1)))
BY
{ (Unfold `replace-vars` 0
THEN Reduce 0
THEN (RWO "eager-map-is-map" 0 THEN Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN (RWO "alpha-aux-mkterm" 0 THENA Auto)
THEN (RWO "map-length" 0 THENA Auto)
THEN (RWO "alpha-aux-mkterm" (-3) THENA Auto)
THEN RepeatFor 3 (ParallelOp -3)
THEN ParallelLast
THEN (RWO "select-map" 0 THENA Auto)
THEN Reduce 0
THEN MoveToConcl (-1)
THEN (GenConclTerm ⌜bts[i]⌝⋅ THENA Auto)
THEN (GenConclTerm ⌜b1[i]⌝⋅ THENA Auto)
THEN D -4
THEN D -2
THEN Reduce 0
THEN Auto) }
1
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. ∀bt:bound-term(opr)
((bt ∈ bts)
⇒ (∀B:term(opr). ∀bnds1,bnds2:varname() List.
(l_disjoint(varname();bnds1;vars-of-subst(s1))
⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
⇒ alpha-aux(opr;bnds1;bnds2;snd(bt);B)
⇒ binders-disjoint(opr;vars-of-subst(s1);snd(bt))
⇒ binders-disjoint(opr;vars-of-subst(s2);B)
⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. ∀bt:bound-term(opr)
((bt ∈ b1)
⇒ (∀bnds1,bnds2:varname() List.
(l_disjoint(varname();bnds1;vars-of-subst(s1))
⇒ l_disjoint(varname();bnds2;vars-of-subst(s2))
⇒ alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
⇒ binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
⇒ binders-disjoint(opr;vars-of-subst(s2);snd(bt))
⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l_disjoint(varname();bnds1;vars-of-subst(s1))
14. l_disjoint(varname();bnds2;vars-of-subst(s2))
15. f = f1 ∈ opr
16. ||bts|| = ||b1|| ∈ ℤ
17. ∀i:ℕ||bts||
(alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i]))
∧ (||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ))
18. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
19. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
20. i : ℕ||bts||
21. ||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ
22. v2 : varname() List
23. v3 : term(opr)
24. bts[i] = <v2, v3> ∈ bound-term(opr)
25. v4 : varname() List
26. v5 : term(opr)
27. b1[i] = <v4, v5> ∈ bound-term(opr)
28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5)
⊢ alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;replace-vars(s1;v3);replace-vars(s2;v5))
Latex:
Latex:
1. [opr] : Type
2. s1 : (varname() \mtimes{} term(opr)) List
3. s2 : (varname() \mtimes{} term(opr)) List
4. equiv-substs(opr;s1;s2)
5. bts : bound-term(opr) List
6. \mforall{}bt:bound-term(opr)
((bt \mmember{} bts)
{}\mRightarrow{} (\mforall{}B:term(opr). \mforall{}bnds1,bnds2:varname() List.
(l\_disjoint(varname();bnds1;vars-of-subst(s1))
{}\mRightarrow{} l\_disjoint(varname();bnds2;vars-of-subst(s2))
{}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;snd(bt);B)
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s1);snd(bt))
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s2);B)
{}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;replace-vars(s1;snd(bt));replace-vars(s2;B)))))
7. f : opr
8. b1 : bound-term(opr) List
9. \mforall{}bt:bound-term(opr)
((bt \mmember{} b1)
{}\mRightarrow{} (\mforall{}bnds1,bnds2:varname() List.
(l\_disjoint(varname();bnds1;vars-of-subst(s1))
{}\mRightarrow{} l\_disjoint(varname();bnds2;vars-of-subst(s2))
{}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s2);snd(bt))
{}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;snd(bt))))))
10. f1 : opr
11. bnds1 : varname() List
12. bnds2 : varname() List
13. l\_disjoint(varname();bnds1;vars-of-subst(s1))
14. l\_disjoint(varname();bnds2;vars-of-subst(s2))
15. alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);mkterm(f1;b1))
16. binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts))
17. binders-disjoint(opr;vars-of-subst(s2);mkterm(f1;b1))
\mvdash{} alpha-aux(opr;bnds1;bnds2;replace-vars(s1;mkterm(f;bts));replace-vars(s2;mkterm(f1;b1)))
By
Latex:
(Unfold `replace-vars` 0
THEN Reduce 0
THEN (RWO "eager-map-is-map" 0 THEN Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN (RWO "alpha-aux-mkterm" 0 THENA Auto)
THEN (RWO "map-length" 0 THENA Auto)
THEN (RWO "alpha-aux-mkterm" (-3) THENA Auto)
THEN RepeatFor 3 (ParallelOp -3)
THEN ParallelLast
THEN (RWO "select-map" 0 THENA Auto)
THEN Reduce 0
THEN MoveToConcl (-1)
THEN (GenConclTerm \mkleeneopen{}bts[i]\mkleeneclose{}\mcdot{} THENA Auto)
THEN (GenConclTerm \mkleeneopen{}b1[i]\mkleeneclose{}\mcdot{} THENA Auto)
THEN D -4
THEN D -2
THEN Reduce 0
THEN Auto)
Home
Index