---

Step * 1 2 1 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. 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)
BY
{ (Thin (-2)
   THEN RepeatFor 6 (MoveToConcl (-1))
   THEN Thin (-1)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN Thin (-1)
   THEN ListInd (-1)
   THEN InductionOnList
   THEN (Reduce 0 THEN Auto)
   THEN (Assert 0 ≤ ||v|| BY
               Auto)
   THEN Auto) }

1
1. opr : Type
2. u : bound-term(opr)
3. v : bound-term(opr) List
4. ∀f:opr. ∀b1:bound-term(opr) List. ∀f1:opr. ∀bnds1,bnds2:varname() List.
     ((f = f1 ∈ opr)
     ⇒ (||v|| = ||b1|| ∈ ℤ)
     ⇒ (∀i:ℕ||v||
           (free-vars-aux(rev(fst(v[i])) + bnds1;snd(v[i]))
           = free-vars-aux(rev(fst(b1[i])) + bnds2;snd(b1[i]))
           ∈ (varname() List)))
     ⇒ (free-vars-aux(bnds1;mkterm(f;v)) = free-vars-aux(bnds2;mkterm(f1;b1)) ∈ (varname() List)))
5. f : opr
6. u1 : bound-term(opr)
7. v1 : bound-term(opr) List
8. ∀f1:opr. ∀bnds1,bnds2:varname() List.
     ((f = f1 ∈ opr)
     ⇒ (||[u / v]|| = ||v1|| ∈ ℤ)
     ⇒ (∀i:ℕ||[u / v]||
           (free-vars-aux(rev(fst([u / v][i])) + bnds1;snd([u / v][i]))
           = free-vars-aux(rev(fst(v1[i])) + bnds2;snd(v1[i]))
           ∈ (varname() List)))
     ⇒ (free-vars-aux(bnds1;mkterm(f;[u / v])) = free-vars-aux(bnds2;mkterm(f1;v1)) ∈ (varname() List)))
9. f1 : opr
10. bnds1 : varname() List
11. bnds2 : varname() List
12. f = f1 ∈ opr
13. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
14. ∀i:ℕ||v|| + 1
      (free-vars-aux(rev(fst([u / v][i])) + bnds1;snd([u / v][i]))
      = free-vars-aux(rev(fst([u1 / v1][i])) + bnds2;snd([u1 / v1][i]))
      ∈ (varname() List))
15. 0 ≤ ||v||
⊢ free-vars-aux(bnds1;mkterm(f;[u / v])) = free-vars-aux(bnds2;mkterm(f1;[u1 / v1])) ∈ (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.  f  =  f1
11.  ||bts||  =  ||b1||
12.  \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])||))
13.  \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])))
\mvdash{}  free-vars-aux(bnds1;mkterm(f;bts))  =  free-vars-aux(bnds2;mkterm(f1;b1))


By

---

Latex:
(Thin  (-2)
  THEN  RepeatFor  6  (MoveToConcl  (-1))
  THEN  Thin  (-1)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  Thin  (-1)
  THEN  ListInd  (-1)
  THEN  InductionOnList
  THEN  (Reduce  0  THEN  Auto)
  THEN  (Assert  0  \mleq{}  ||v||  BY
                          Auto)
  THEN  Auto)

---

Home Index