---

Step * of Lemma mFOL-sequent-evidence_transitivity2

∀hyps:mFOL() List. ∀[x,y:mFOL()].  (mFOL-sequent-evidence(<hyps, y>) ⇒ mFOL-sequent-evidence(<[y / hyps], x>) ⇒ mFOL-s\000Cequent-evidence(<hyps, x>))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (((Assert Dom,S,a |= mFOL-sequent-abstract(<[y / hyps], x>) BY
                 (Auto THEN All (RepUR ``mFOL-sequent-evidence mFO-uniform-evidence``) THEN BackThruSomeHyp))
          THEN (Assert Dom,S,a |= mFOL-sequent-abstract(<hyps, y>) BY
                      (Auto THEN All (RepUR ``mFOL-sequent-evidence mFO-uniform-evidence``) THEN BackThruSomeHyp))⋅
          )
         THEN (All (RepUR ``mFOL-sequent-abstract FOSatWith``)⋅
               THEN D 1
               THEN All Reduce
               THEN All (Fold `implies`)
               THEN All (Fold `and`)
               THEN All (Fold `FOSatWith`)
               THEN Auto
               THEN D (-3)
               THEN Auto)⋅
         )⋅) }

---

Latex:


\mforall{}hyps:mFOL()  List
    \mforall{}[x,y:mFOL()].    (mFOL-sequent-evidence(<hyps,  y>)  {}\mRightarrow{}  mFOL-sequent-evidence(<[y  /  hyps],  x>)  {}\mRightarrow{}  mFO\000CL-sequent-evidence(<hyps,  x>))


By

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

---

Home Index