Step
*
of Lemma
subst-term_functionality
No Annotations
∀[opr:Type]
∀t1,t2:term(opr). ∀s1,s2:(varname() × term(opr)) List.
(alpha-eq-terms(opr;t1;t2) ⇒ equiv-substs(opr;s1;s2) ⇒ alpha-eq-terms(opr;subst-term(s1;t1);subst-term(s2;t2)))
BY
{ (Auto
THEN Unfold `subst-term` 0
THEN (Assert alpha-eq-terms(opr;subst-frame(s1;t1);subst-frame(s2;t2)) BY
((Assert alpha-eq-terms(opr;subst-frame(s1;t1);t1) BY
Auto)
THEN (Assert alpha-eq-terms(opr;subst-frame(s2;t2);t2) BY
Auto)
THEN RelRST
THEN Auto))
THEN (Assert binders-disjoint(opr;vars-of-subst(s1);subst-frame(s1;t1)) BY
Auto)
THEN (Assert binders-disjoint(opr;vars-of-subst(s2);subst-frame(s2;t2)) BY
Auto)
THEN RepeatFor 3 (MoveToConcl (-1))
THEN (GenConcl ⌜subst-frame(s1;t1) = A ∈ term(opr)⌝⋅ THENA Auto)
THEN (GenConcl ⌜subst-frame(s2;t2) = B ∈ term(opr)⌝⋅ THENA Auto)
THEN ThinVar `t1'
THEN ThinVar `t2'
THEN (Enough to prove ∀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;A;B)
⇒ binders-disjoint(opr;vars-of-subst(s1);A)
⇒ binders-disjoint(opr;vars-of-subst(s2);B)
⇒ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;A);replace-vars(s2;B)))
Because (RepeatFor 2 ((D -1 With ⌜[]⌝ THENA Auto)) THEN Fold `alpha-eq-terms` (-1) THEN D -1 THEN Auto))
THEN RepeatFor 2 (MoveToConcl (-1))
THEN (BLemma `term-induction` THENA Auto)
THEN Intro
THEN ((Assert varterm(v) ∈ term(opr) BY Auto) ORELSE RepeatFor 2 (Intro))
THEN (BLemma `term-induction` THENW Auto)
THEN Intros
THEN Try ((Unfold `alpha-aux` -3 THEN Reduce -3 THEN FalseHD (-3)))) }
1
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. v : {v:varname()| ¬(v = nullvar() ∈ varname())}
6. varterm(v) ∈ term(opr)
7. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())}
8. bnds1 : varname() List
9. bnds2 : varname() List
10. l_disjoint(varname();bnds1;vars-of-subst(s1))
11. l_disjoint(varname();bnds2;vars-of-subst(s2))
12. alpha-aux(opr;bnds1;bnds2;varterm(v);varterm(v1))
13. binders-disjoint(opr;vars-of-subst(s1);varterm(v))
14. binders-disjoint(opr;vars-of-subst(s2);varterm(v1))
⊢ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;varterm(v));replace-vars(s2;varterm(v1)))
2
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)))
Latex:
Latex:
No Annotations
\mforall{}[opr:Type]
\mforall{}t1,t2:term(opr). \mforall{}s1,s2:(varname() \mtimes{} term(opr)) List.
(alpha-eq-terms(opr;t1;t2)
{}\mRightarrow{} equiv-substs(opr;s1;s2)
{}\mRightarrow{} alpha-eq-terms(opr;subst-term(s1;t1);subst-term(s2;t2)))
By
Latex:
(Auto
THEN Unfold `subst-term` 0
THEN (Assert alpha-eq-terms(opr;subst-frame(s1;t1);subst-frame(s2;t2)) BY
((Assert alpha-eq-terms(opr;subst-frame(s1;t1);t1) BY
Auto)
THEN (Assert alpha-eq-terms(opr;subst-frame(s2;t2);t2) BY
Auto)
THEN RelRST
THEN Auto))
THEN (Assert binders-disjoint(opr;vars-of-subst(s1);subst-frame(s1;t1)) BY
Auto)
THEN (Assert binders-disjoint(opr;vars-of-subst(s2);subst-frame(s2;t2)) BY
Auto)
THEN RepeatFor 3 (MoveToConcl (-1))
THEN (GenConcl \mkleeneopen{}subst-frame(s1;t1) = A\mkleeneclose{}\mcdot{} THENA Auto)
THEN (GenConcl \mkleeneopen{}subst-frame(s2;t2) = B\mkleeneclose{}\mcdot{} THENA Auto)
THEN ThinVar `t1'
THEN ThinVar `t2'
THEN (Enough to prove \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;A;B)
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s1);A)
{}\mRightarrow{} binders-disjoint(opr;vars-of-subst(s2);B)
{}\mRightarrow{} alpha-aux(opr;bnds1;bnds2;replace-vars(s1;A);replace-vars(s2;B)))
Because (RepeatFor 2 ((D -1 With \mkleeneopen{}[]\mkleeneclose{} THENA Auto))
THEN Fold `alpha-eq-terms` (-1)
THEN D -1
THEN Auto))
THEN RepeatFor 2 (MoveToConcl (-1))
THEN (BLemma `term-induction` THENA Auto)
THEN Intro
THEN ((Assert varterm(v) \mmember{} term(opr) BY Auto) ORELSE RepeatFor 2 (Intro))
THEN (BLemma `term-induction` THENW Auto)
THEN Intros
THEN Try ((Unfold `alpha-aux` -3 THEN Reduce -3 THEN FalseHD (-3))))
Home
Index