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


1. mFOL()
2. 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. 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