---

Step * 1 2 1 1 of Lemma free-vars_functionality


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)
BY
{ ((Unfold `free-vars-aux` 0 THEN Reduce 0) THEN RepeatFor 2 (EqCDA)) }

1
.....subterm..... T:t
1:n
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||
⊢ let vs,a = u 
  in free-vars-aux(rev(vs) + bnds1;a)
= let vs,a = u1 
  in free-vars-aux(rev(vs) + bnds2;a)
∈ (varname() List)

2
.....subterm..... T:t
2:n
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||
⊢ map(λbt.let vs,a = bt 
          in free-vars-aux(rev(vs) + bnds1;a);v)
= map(λbt.let vs,a = bt 
          in free-vars-aux(rev(vs) + bnds2;a);v1)
∈ (varname() List List)

---

Latex:

---

Latex:

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


By

---

Latex:
((Unfold  `free-vars-aux`  0  THEN  Reduce  0)  THEN  RepeatFor  2  (EqCDA))

---

Home Index