---

Step * 1 2 1 1 2 of Lemma free-vars_functionality

.....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)
BY
{ (BLemma `list_extensionality`
   THEN Auto
   THEN (RWO "select-map" 0 THENA Auto)
   THEN Reduce 0
   THEN (D -4 With ⌜i + 1⌝  THENA Auto)
   THEN (RWO "select_cons_tl" (-1) THENA Auto)
   THEN (Subst' (i + 1) - 1 ~ i -1 THENA Auto)
   THEN MoveToConcl (-1)
   THEN ((GenConclTerm ⌜v[i]⌝⋅ THENA Auto) THEN D -2)
   THEN ((GenConclTerm ⌜v1[i]⌝⋅ THENA Auto) THEN D -2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{}  map(\mlambda{}bt.let  vs,a  =  bt 
                    in  free-vars-aux(rev(vs)  +  bnds1;a);v)
=  map(\mlambda{}bt.let  vs,a  =  bt 
                    in  free-vars-aux(rev(vs)  +  bnds2;a);v1)


By

---

Latex:
(BLemma  `list\_extensionality`
  THEN  Auto
  THEN  (RWO  "select-map"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (D  -4  With  \mkleeneopen{}i  +  1\mkleeneclose{}    THENA  Auto)
  THEN  (RWO  "select\_cons\_tl"  (-1)  THENA  Auto)
  THEN  (Subst'  (i  +  1)  -  1  \msim{}  i  -1  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((GenConclTerm  \mkleeneopen{}v[i]\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2)
  THEN  ((GenConclTerm  \mkleeneopen{}v1[i]\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index