---

Step * of Lemma mFOL-sequent-evidence_and

∀hyps:mFOL() List. ∀[x,y:mFOL()].  (mFOL-sequent-evidence(<hyps, x>) ⇒ mFOL-sequent-evidence(<hyps, y>) ⇒ mFOL-sequent\000C-evidence(<hyps, x ∧ 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 (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 (All (Fold `implies`) THEN All (Fold `FOSatWith`))
               THEN Auto
               THEN ThinTrivial
               THEN (RepUR ``mFOL-abstract`` 0
                     THEN Fold `mFOL-abstract` 0
                     THEN RepUR ``FOConnective FOSatWith let`` 0
                     THEN All (Fold `FOSatWith`)
                     THEN Auto)⋅)⋅
         )⋅) }

---

Latex:


\mforall{}hyps:mFOL()  List.  \mforall{}[x,y:mFOL()].    (mFOL-sequent-evidence(<hyps,  x>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,\000C  y>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  x  \mwedge{}  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  (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  (All  (Fold  `implies`)  THEN  All  (Fold  `FOSatWith`))
                          THEN  Auto
                          THEN  ThinTrivial
                          THEN  (RepUR  ``mFOL-abstract``  0
                                      THEN  Fold  `mFOL-abstract`  0
                                      THEN  RepUR  ``FOConnective  FOSatWith  let``  0
                                      THEN  All  (Fold  `FOSatWith`)
                                      THEN  Auto)\mcdot{})\mcdot{}
              )\mcdot{})

---

Home Index