---

Step * 1 3 2 1 1 1 of Lemma alpha-rename-binders-disjoint


1. [opr] : Type
2. L : 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().
           ((∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))} 
               ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
           ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt))))))
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) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f@0 x ∈ L)))
9. bts ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  List
10. λbt.let vs,a = bt 
        in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  ⟶ bound\000C-term(opr)
11. i : ℕ||bts||
12. v1 : varname() List
13. v2 : term(opr)
14. [%5] : (<v1, v2> ∈ bts)
15. ∀bnds:varname() List. ∀f:{v@0:varname()| (v@0 ∈ bnds @ all-vars(v2))}  ⟶ varname().
      ((∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(v2))} 
          ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
      ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;v2)))
16. x : varname()
⊢ ¬((x ∈ map(f@0;v1)) ∧ (x ∈ L))
BY
{ (Assert v1 ∈ {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}  List BY
         (SubsumeC ⌜{v:varname()| (v ∈ v1)}  List⌝⋅
          THENL [Auto
                ; (SubtypeReasoning1
                   THEN Auto
                   THEN (GenListD 0 THEN (OrRight THENA Auto))
                   THEN (RWO "member-all-vars-mkterm" 0 THENA Auto)
                   THEN D 0 With ⌜<v1, v2>⌝ 
                   THEN Auto)]
         )) }

1
1. [opr] : Type
2. L : 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().
           ((∀x:{v:varname()| (v ∈ bnds @ all-vars(snd(bt)))} 
               ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
           ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt))))))
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) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f@0 x ∈ L)))
9. bts ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  List
10. λbt.let vs,a = bt 
        in <map(f@0;vs), alpha-rename-aux(f@0;rev(vs) + bnds;a)> ∈ {bt:varname() List × term(opr)| (bt ∈ bts)}  ⟶ bound\000C-term(opr)
11. i : ℕ||bts||
12. v1 : varname() List
13. v2 : term(opr)
14. [%5] : (<v1, v2> ∈ bts)
15. ∀bnds:varname() List. ∀f:{v@0:varname()| (v@0 ∈ bnds @ all-vars(v2))}  ⟶ varname().
      ((∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(v2))} 
          ((((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname())) ∧ (¬(f x ∈ L))))
      ⇒ binders-disjoint(opr;L;alpha-rename-aux(f;bnds;v2)))
16. x : varname()
17. v1 ∈ {v:varname()| (v ∈ bnds @ all-vars(mkterm(f;bts)))}  List
⊢ ¬((x ∈ map(f@0;v1)) ∧ (x ∈ L))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  L  :  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().
                      ((\mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(snd(bt)))\} 
                              ((((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))  \mwedge{}  (\mneg{}(f  x  \mmember{}  L))))
                      {}\mRightarrow{}  binders-disjoint(opr;L;alpha-rename-aux(f;bnds;snd(bt))))))
5.  f  :  opr
6.  bnds  :  varname()  List
7.  f@0  :  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\}    {}\mrightarrow{}  varname()
8.  \mforall{}x:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\} 
          ((((f@0  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))  \mwedge{}  (\mneg{}(f@0  x  \mmember{}  L)))
9.  bts  \mmember{}  \{bt:varname()  List  \mtimes{}  term(opr)|  (bt  \mmember{}  bts)\}    List
10.  \mlambda{}bt.let  vs,a  =  bt 
                in  <map(f@0;vs),  alpha-rename-aux(f@0;rev(vs)  +  bnds;a)>  \mmember{}  \{bt:varname()  List  \mtimes{}  term(opr)| 
                                                                                                                                        (bt  \mmember{}  bts)\}    {}\mrightarrow{}  bound-term(opr)
11.  i  :  \mBbbN{}||bts||
12.  v1  :  varname()  List
13.  v2  :  term(opr)
14.  [\%5]  :  (<v1,  v2>  \mmember{}  bts)
15.  \mforall{}bnds:varname()  List.  \mforall{}f:\{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(v2))\}    {}\mrightarrow{}  varname().
            ((\mforall{}x:\{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(v2))\} 
                    ((((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))  \mwedge{}  (\mneg{}(f  x  \mmember{}  L))))
            {}\mRightarrow{}  binders-disjoint(opr;L;alpha-rename-aux(f;bnds;v2)))
16.  x  :  varname()
\mvdash{}  \mneg{}((x  \mmember{}  map(f@0;v1))  \mwedge{}  (x  \mmember{}  L))


By

---

Latex:
(Assert  v1  \mmember{}  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\}    List  BY
              (SubsumeC  \mkleeneopen{}\{v:varname()|  (v  \mmember{}  v1)\}    List\mkleeneclose{}\mcdot{}
                THENL  [Auto
                            ;  (SubtypeReasoning1
                                  THEN  Auto
                                  THEN  (GenListD  0  THEN  (OrRight  THENA  Auto))
                                  THEN  (RWO  "member-all-vars-mkterm"  0  THENA  Auto)
                                  THEN  D  0  With  \mkleeneopen{}<v1,  v2>\mkleeneclose{} 
                                  THEN  Auto)]
              ))

---

Home Index