---

Step * 1 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. ∃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)))))
BY
{ (ParallelLast THEN Auto) }

---

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.  \mexists{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  \mwedge{}  (x  \mmember{}  free-vars(snd(bt)))  \mwedge{}  (\mneg{}(x  \mmember{}  fst(bt))))
\mvdash{}  \mexists{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  \mwedge{}  ((x  \mmember{}  fst(bt))  \mvee{}  (x  \mmember{}  all-vars(snd(bt)))))


By

---

Latex:
(ParallelLast  THEN  Auto)

---

Home Index