---

Step * 1 of Lemma free-vars-all-vars


1. [opr] : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr). ((bt ∈ bts) ⇒ (∀x:varname(). ((x ∈ free-vars(snd(bt))) ⇒ (x ∈ all-vars(snd(bt))))))
4. f : opr
5. x : varname()
6. (x ∈ free-vars(mkterm(f;bts)))
⊢ (x ∈ all-vars(mkterm(f;bts)))
BY
{ ((RWO "member-all-vars-mkterm" 0 THENA Auto) THEN (RWO "member-free-vars-mkterm" (-1) THENA Auto)) }

1
1. [opr] : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr). ((bt ∈ bts) ⇒ (∀x:varname(). ((x ∈ free-vars(snd(bt))) ⇒ (x ∈ all-vars(snd(bt))))))
4. f : opr
5. x : varname()
6. ∃bt:bound-term(opr). ((bt ∈ bts) ∧ (x ∈ free-vars(snd(bt))) ∧ (¬(x ∈ fst(bt))))
⊢ ∃bt:bound-term(opr). ((bt ∈ bts) ∧ ((x ∈ fst(bt)) ∨ (x ∈ all-vars(snd(bt)))))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  bts  :  bound-term(opr)  List
3.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)  {}\mRightarrow{}  (\mforall{}x:varname().  ((x  \mmember{}  free-vars(snd(bt)))  {}\mRightarrow{}  (x  \mmember{}  all-vars(snd(bt))))))
4.  f  :  opr
5.  x  :  varname()
6.  (x  \mmember{}  free-vars(mkterm(f;bts)))
\mvdash{}  (x  \mmember{}  all-vars(mkterm(f;bts)))


By

---

Latex:
((RWO  "member-all-vars-mkterm"  0  THENA  Auto)  THEN  (RWO  "member-free-vars-mkterm"  (-1)  THENA  Auto))

---

Home Index