Step
*
2
1
1
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. 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)
29. ∀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;v3;B)
⇒ binders-disjoint(opr;vars-of-subst(s1);v3)
⇒ binders-disjoint(opr;vars-of-subst(s2);B)
⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;v3);replace-vars(s2;B)))
⊢ l_disjoint(varname();rev(v2) + bnds1;vars-of-subst(s1))
BY
{ ((RWO "rev-append-as-reverse" 0 THENA Auto)
THEN RWO "l_disjoint_append2" 0
THEN Auto
THEN (Assert binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts)) BY
Hypothesis)
THEN Unfold `binders-disjoint` -1
THEN Reduce -1
THEN (RWO "l_all_iff" (-1) THENA Auto)
THEN (InstHyp [⌜<v2, v3>⌝] (-1)⋅ THENA Auto)
THEN Reduce -1
THEN D -1
THEN Thin (-1)
THEN RepeatFor 2 (ParallelLast)
THEN RWO "member-reverse" 0
THEN Auto) }
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. f = f1
16. ||bts|| = ||b1||
17. \mforall{}i:\mBbbN{}||bts||
(alpha-aux(opr;rev(fst(bts[i])) + bnds1;rev(fst(b1[i])) + bnds2;snd(bts[i]);snd(b1[i]))
\mwedge{} (||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 : \mBbbN{}||bts||
21. ||fst(bts[i])|| = ||fst(b1[i])||
22. v2 : varname() List
23. v3 : term(opr)
24. bts[i] = <v2, v3>
25. v4 : varname() List
26. v5 : term(opr)
27. b1[i] = <v4, v5>
28. alpha-aux(opr;rev(v2) + bnds1;rev(v4) + bnds2;v3;v5)
29. \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;v3;B)
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s1);v3)
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s2);B)
{}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;replace-vars(s1;v3);replace-vars(s2;B)))
\mvdash{} l\_disjoint(varname();rev(v2) + bnds1;vars-of-subst(s1))
By
Latex:
((RWO "rev-append-as-reverse" 0 THENA Auto)
THEN RWO "l\_disjoint\_append2" 0
THEN Auto
THEN (Assert binders-disjoint(opr;vars-of-subst(s1);mkterm(f;bts)) BY
Hypothesis)
THEN Unfold `binders-disjoint` -1
THEN Reduce -1
THEN (RWO "l\_all\_iff" (-1) THENA Auto)
THEN (InstHyp [\mkleeneopen{}<v2, v3>\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN Reduce -1
THEN D -1
THEN Thin (-1)
THEN RepeatFor 2 (ParallelLast)
THEN RWO "member-reverse" 0
THEN Auto)
Home
Index