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

.....aux..... 
1. opr Type
2. 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. 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. b1 varname() List
11. b2 term(opr)
12. (<b1, b2> ∈ bts)
⊢ alpha-rename-aux(f@0;rev(b1) bnds;b2) ∈ term(opr)
BY
((Enough to prove {v:varname()| (v ∈ rev(b1) bnds all-vars(b2))}  ⊆{v:varname()| 
                                                                             (v ∈ bnds all-vars(mkterm(f;bts)))} 
     Because Auto)
   THEN (D THENA Auto)
   THEN -1
   THEN (MemTypeCD THENW Auto)
   THEN Try (Trivial)
   THEN GenListD (-1)
   THEN -1) }

1
1. opr Type
2. 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. 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. b1 varname() List
11. b2 term(opr)
12. (<b1, b2> ∈ bts)
13. varname()
14. (x ∈ rev(b1) bnds)
⊢ (x ∈ bnds all-vars(mkterm(f;bts)))

2
1. opr Type
2. 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. 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. b1 varname() List
11. b2 term(opr)
12. (<b1, b2> ∈ bts)
13. varname()
14. (x ∈ all-vars(b2))
⊢ (x ∈ bnds all-vars(mkterm(f;bts)))


Latex:


Latex:
.....aux..... 
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.  b1  :  varname()  List
11.  b2  :  term(opr)
12.  (<b1,  b2>  \mmember{}  bts)
\mvdash{}  alpha-rename-aux(f@0;rev(b1)  +  bnds;b2)  \mmember{}  term(opr)


By


Latex:
((Enough  to  prove  \{v:varname()|  (v  \mmember{}  rev(b1)  +  bnds  @  all-vars(b2))\} 
                                        \msubseteq{}r  \{v:varname()|  (v  \mmember{}  bnds  @  all-vars(mkterm(f;bts)))\} 
      Because  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Try  (Trivial)
  THEN  GenListD  (-1)
  THEN  D  -1)




Home Index