---

Step * of Lemma mFOL-sequent-evidence_transitivity1

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

---

Latex:


\mforall{}[hyps:mFOL()  List].  \mforall{}[x,y:mFOL()].
    ((\mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].
            \mforall{}a:FOAssignment(Dom).  (Dom,S,a  |=  mFOL-abstract(x)  {}\mRightarrow{}  Dom,S,a  |=  mFOL-abstract(y)))
    {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  x>)
    {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  y>))


By

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

---

Home Index