---

Step * 1 of Lemma free-vars_functionality


1. [opr] : Type
⊢ ∀t1,t2:term(opr). ∀bnds1,bnds2:varname() List.
    (alpha-aux(opr;bnds1;bnds2;t1;t2) ⇒ (free-vars-aux(bnds1;t1) = free-vars-aux(bnds2;t2) ∈ (varname() List)))
BY
{ ((BLemma `term-induction` THENA Auto)
   THEN Intro
   THEN ((Assert varterm(v) ∈ term(opr) BY Auto) ORELSE RepeatFor 2 (Intro))
   THEN BLemma `term-induction`
   THEN Auto
   THEN Try ((Unfold `alpha-aux` -1 THEN Reduce -1 THEN FalseHD (-1)))) }

1
1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. varterm(v) ∈ term(opr)
4. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. bnds1 : varname() List
6. bnds2 : varname() List
7. alpha-aux(opr;bnds1;bnds2;varterm(v);varterm(v1))
⊢ free-vars-aux(bnds1;varterm(v)) = free-vars-aux(bnds2;varterm(v1)) ∈ (varname() List)

2
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)

---

Latex:

---

Latex:

1.  [opr]  :  Type
\mvdash{}  \mforall{}t1,t2:term(opr).  \mforall{}bnds1,bnds2:varname()  List.
        (alpha-aux(opr;bnds1;bnds2;t1;t2)  {}\mRightarrow{}  (free-vars-aux(bnds1;t1)  =  free-vars-aux(bnds2;t2)))


By

---

Latex:
((BLemma  `term-induction`  THENA  Auto)
  THEN  Intro
  THEN  ((Assert  varterm(v)  \mmember{}  term(opr)  BY  Auto)  ORELSE  RepeatFor  2  (Intro))
  THEN  BLemma  `term-induction`
  THEN  Auto
  THEN  Try  ((Unfold  `alpha-aux`  -1  THEN  Reduce  -1  THEN  FalseHD  (-1))))

---

Home Index