---

Step * 1 2 of Lemma free-vars_functionality


1. opr : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀t2:term(opr). ∀bnds1,bnds2:varname() List.
           (alpha-aux(opr;bnds1;bnds2;snd(bt);t2)
           ⇒ (free-vars-aux(bnds1;snd(bt)) = free-vars-aux(bnds2;t2) ∈ (varname() List)))))
4. f : opr
5. b1 : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀bnds1,bnds2:varname() List.
           (alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
           ⇒ (free-vars-aux(bnds1;mkterm(f;bts)) = free-vars-aux(bnds2;snd(bt)) ∈ (varname() List)))))
7. f1 : opr
8. bnds1 : varname() List
9. bnds2 : varname() List
10. alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);mkterm(f1;b1))
⊢ free-vars-aux(bnds1;mkterm(f;bts)) = free-vars-aux(bnds2;mkterm(f1;b1)) ∈ (varname() List)
BY
{ ((RWO "alpha-aux-mkterm" (-1) THENA Auto)
   THEN ExRepD
   THEN (Assert ∀i:ℕ||bts||
                  (free-vars-aux(rev(fst(bts[i])) + bnds1;snd(bts[i]))
                  = free-vars-aux(rev(fst(b1[i])) + bnds2;snd(b1[i]))
                  ∈ (varname() List)) BY
               (ParallelLast THEN BackThruSomeHyp THEN Auto))) }

1
1. opr : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀t2:term(opr). ∀bnds1,bnds2:varname() List.
           (alpha-aux(opr;bnds1;bnds2;snd(bt);t2)
           ⇒ (free-vars-aux(bnds1;snd(bt)) = free-vars-aux(bnds2;t2) ∈ (varname() List)))))
4. f : opr
5. b1 : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀bnds1,bnds2:varname() List.
           (alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
           ⇒ (free-vars-aux(bnds1;mkterm(f;bts)) = free-vars-aux(bnds2;snd(bt)) ∈ (varname() List)))))
7. f1 : opr
8. bnds1 : varname() List
9. bnds2 : varname() List
10. f = f1 ∈ opr
11. ||bts|| = ||b1|| ∈ ℤ
12. ∀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])|| ∈ ℤ))
13. ∀i:ℕ||bts||
      (free-vars-aux(rev(fst(bts[i])) + bnds1;snd(bts[i]))
      = free-vars-aux(rev(fst(b1[i])) + bnds2;snd(b1[i]))
      ∈ (varname() List))
⊢ free-vars-aux(bnds1;mkterm(f;bts)) = free-vars-aux(bnds2;mkterm(f1;b1)) ∈ (varname() List)

---

Latex:

---

Latex:

1.  opr  :  Type
2.  bts  :  bound-term(opr)  List
3.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\mforall{}t2:term(opr).  \mforall{}bnds1,bnds2:varname()  List.
                      (alpha-aux(opr;bnds1;bnds2;snd(bt);t2)
                      {}\mRightarrow{}  (free-vars-aux(bnds1;snd(bt))  =  free-vars-aux(bnds2;t2)))))
4.  f  :  opr
5.  b1  :  bound-term(opr)  List
6.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  b1)
          {}\mRightarrow{}  (\mforall{}bnds1,bnds2:varname()  List.
                      (alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);snd(bt))
                      {}\mRightarrow{}  (free-vars-aux(bnds1;mkterm(f;bts))  =  free-vars-aux(bnds2;snd(bt))))))
7.  f1  :  opr
8.  bnds1  :  varname()  List
9.  bnds2  :  varname()  List
10.  alpha-aux(opr;bnds1;bnds2;mkterm(f;bts);mkterm(f1;b1))
\mvdash{}  free-vars-aux(bnds1;mkterm(f;bts))  =  free-vars-aux(bnds2;mkterm(f1;b1))


By

---

Latex:
((RWO  "alpha-aux-mkterm"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  \mforall{}i:\mBbbN{}||bts||
                                (free-vars-aux(rev(fst(bts[i]))  +  bnds1;snd(bts[i]))
                                =  free-vars-aux(rev(fst(b1[i]))  +  bnds2;snd(b1[i])))  BY
                          (ParallelLast  THEN  BackThruSomeHyp  THEN  Auto)))

---

Home Index