---

Step * 1 2 1 of Lemma mFOL-sequent-freevars-subset-2


1. u : mFOL()
2. v : mFOL() List
3. ∀concl,h:mFOL().  ((h ∈ v) ⇒ mFOL-freevars(h) ⊆ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v))
4. concl : mFOL()
5. h : mFOL()
6. (h ∈ v)
7. mFOL-freevars(h) ⊆ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)
⊢ mFOL-freevars(h) ⊆ mFOL-freevars(u) ⋃ reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl);v)
BY
{ ((InstLemma `l_contains_transitivity` [⌜ℤ⌝;⌜mFOL-freevars(h)⌝;⌜reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(concl\000C);v)⌝
    ]⋅
   THENM BHyp -1 
   )
   THEN Auto
   ) }

---

Latex:

---

Latex:

1.  u  :  mFOL()
2.  v  :  mFOL()  List
3.  \mforall{}concl,h:mFOL().
          ((h  \mmember{}  v)  {}\mRightarrow{}  mFOL-freevars(h)  \msubseteq{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(concl);v))
4.  concl  :  mFOL()
5.  h  :  mFOL()
6.  (h  \mmember{}  v)
7.  mFOL-freevars(h)  \msubseteq{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(concl);v)
\mvdash{}  mFOL-freevars(h)  \msubseteq{}  mFOL-freevars(u)  \mcup{}  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(concl);v)


By

---

Latex:
((InstLemma  `l\_contains\_transitivity`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}mFOL-freevars(h)\mkleeneclose{};
    \mkleeneopen{}reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(concl);v)\mkleeneclose{}]\mcdot{}
  THENM  BHyp  -1 
  )
  THEN  Auto
  )

---

Home Index