---

Step * of Lemma member-free-vars-mkterm

No Annotations
∀[opr:Type]
  ∀f:opr. ∀v:varname(). ∀bts:bound-term(opr) List.
    ((v ∈ free-vars(mkterm(f;bts))) ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars(snd(bt))) ∧ (¬(v ∈ fst(bt)))))
BY
{ (Intros
   THEN Unfold `free-vars` 0
   THEN (Enough to prove ∀bnds:varname() List
                           ((v ∈ free-vars-aux(bnds;mkterm(f;bts)))
                           ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars-aux(rev(fst(bt)) + bnds;snd(bt)))))
          Because ((RWO "-1" 0 THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto) THEN RepeatFor 2 (ParallelLast)))) }

1
1. [opr] : Type
2. f : opr
3. v : varname()
4. bts : bound-term(opr) List
⊢ ∀bnds:varname() List
    ((v ∈ free-vars-aux(bnds;mkterm(f;bts)))
    ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars-aux(rev(fst(bt)) + bnds;snd(bt)))))

2
.....aux..... 
1. [opr] : Type
2. f : opr
3. v : varname()
4. bts : bound-term(opr) List
5. ∀bnds:varname() List
     ((v ∈ free-vars-aux(bnds;mkterm(f;bts)))
     ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars-aux(rev(fst(bt)) + bnds;snd(bt)))))
6. bt : bound-term(opr)
7. (bt ∈ bts)
8. (v ∈ free-vars-aux(rev(fst(bt)) + [];snd(bt)))
⊢ (v ∈ free-vars-aux([];snd(bt))) ∧ (¬(v ∈ fst(bt)))

3
.....aux..... 
1. [opr] : Type
2. f : opr
3. v : varname()
4. bts : bound-term(opr) List
5. ∀bnds:varname() List
     ((v ∈ free-vars-aux(bnds;mkterm(f;bts)))
     ⇐⇒ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (v ∈ free-vars-aux(rev(fst(bt)) + bnds;snd(bt)))))
6. bt : bound-term(opr)
7. (bt ∈ bts)
8. (v ∈ free-vars-aux([];snd(bt))) ∧ (¬(v ∈ fst(bt)))
⊢ (v ∈ free-vars-aux(rev(fst(bt)) + [];snd(bt)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}f:opr.  \mforall{}v:varname().  \mforall{}bts:bound-term(opr)  List.
        ((v  \mmember{}  free-vars(mkterm(f;bts)))
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  \mwedge{}  (v  \mmember{}  free-vars(snd(bt)))  \mwedge{}  (\mneg{}(v  \mmember{}  fst(bt)))))


By

---

Latex:
(Intros
  THEN  Unfold  `free-vars`  0
  THEN  (Enough  to  prove  \mforall{}bnds:varname()  List
                                                  ((v  \mmember{}  free-vars-aux(bnds;mkterm(f;bts)))
                                                  \mLeftarrow{}{}\mRightarrow{}  \mexists{}bt:bound-term(opr)
                                                            ((bt  \mmember{}  bts)  \mwedge{}  (v  \mmember{}  free-vars-aux(rev(fst(bt))  +  bnds;snd(bt)))))
                Because  ((RWO  "-1"  0  THENA  Auto)
                                  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
                                  THEN  RepeatFor  2  (ParallelLast))))

---

Home Index