---

Step * of Lemma better-FOL-sequent-evidence_transitivity1

∀[hyps:mFOL() List]. ∀[x,y:mFOL()].
  (mFOL-freevars(x) ⊆ mFOL-sequent-freevars(<hyps, y>)
  ⇒ (∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
        ∀a:FOAssignment(mFOL-sequent-freevars(<hyps, y>),Dom). (Dom,S,a +|= FOL-abstract(x) ⇒ Dom,S,a +|= FOL-abstract(\000Cy)))
  ⇒ FOL-sequent-evidence{i:l}(<hyps, x>)
  ⇒ FOL-sequent-evidence{i:l}(<hyps, y>))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert Dom,S,a +|= FOL-sequent-abstract(<hyps, x>) BY
               (Auto THEN All (RepUR ``FOL-sequent-evidence FO-uniform-evidence``) THEN BackThruSomeHyp))
   THEN All (RepUR ``FOL-sequent-abstract FOSatWith+``)⋅
   THEN All (Fold `FOSatWith+`)
   THEN All (Fold `implies`)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[hyps:mFOL()  List].  \mforall{}[x,y:mFOL()].
    (mFOL-freevars(x)  \msubseteq{}  mFOL-sequent-freevars(<hyps,  y>)
    {}\mRightarrow{}  (\mforall{}[Dom:Type].  \mforall{}[S:FOStruct+\{i:l\}(Dom)].
                \mforall{}a:FOAssignment(mFOL-sequent-freevars(<hyps,  y>),Dom).  (Dom,S,a  +|=  FOL-abstract(x)  {}\mRightarrow{}  Dom,S\000C,a  +|=  FOL-abstract(y)))
    {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(<hyps,  x>)
    {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(<hyps,  y>))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  Dom,S,a  +|=  FOL-sequent-abstract(<hyps,  x>)  BY
                          (Auto
                            THEN  All  (RepUR  ``FOL-sequent-evidence  FO-uniform-evidence``)
                            THEN  BackThruSomeHyp))
  THEN  All  (RepUR  ``FOL-sequent-abstract  FOSatWith+``)\mcdot{}
  THEN  All  (Fold  `FOSatWith+`)
  THEN  All  (Fold  `implies`)
  THEN  Auto)

---

Home Index