---

Step * of Lemma FOL-sequent-evidence_and

∀hyps:mFOL() List. ∀[x,y:mFOL()].  (FOL-sequent-evidence{i:l}(<hyps, x>) ⇒ FOL-sequent-evidence{i:l}(<hyps, y>) ⇒ FOL-\000Csequent-evidence{i:l}(<hyps, x ∧ y>))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN ((Assert Dom,S,a +|= FOL-sequent-abstract(<hyps, x>) ∧ Dom,S,a +|= FOL-sequent-abstract(<hyps, y>) BY
                (Auto
                 THEN All (RepUR ``FOL-sequent-evidence FO-uniform-evidence``)
                 THEN BackThruSomeHyp
                 THEN (DoSubsume THEN Auto)
                 THEN SubtypeReasoning1
                 THEN Auto
                 THEN BLemma_o (ioid Obid: mFOL-sequent-freevars-subset-3)⋅
                 THEN Auto
                 THEN RepUR ``mFOL-freevars`` 0
                 THEN Fold `mFOL-freevars` 0
                 THEN RWO "val-union-l-union" 0
                 THEN Auto))
         THEN (D -1
               THEN All (RepUR ``FOL-sequent-abstract FOSatWith+``)⋅
               THEN (All (Fold `implies`) THEN All (Fold `FOSatWith+`))
               THEN Auto
               THEN ThinTrivial
               THEN (RepUR ``FOL-abstract`` 0
                     THEN Fold `FOL-abstract` 0
                     THEN RepUR ``FOConnective+ FOSatWith+ let`` 0
                     THEN All (Fold `FOSatWith+`)
                     THEN Auto)⋅)
         )⋅) }

1
1. hyps : mFOL() List@i
2. [x] : mFOL()
3. [y] : mFOL()
4. FOL-sequent-evidence{i:l}(<hyps, x>)@i'
5. FOL-sequent-evidence{i:l}(<hyps, y>)@i'
6. [Dom] : Type
7. [S] : FOStruct+{i:l}(Dom)
8. a : FOAssignment(mFOL-sequent-freevars(<hyps, x ∧ y>),Dom)@i
9. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))@i
10. Dom,S,a +|= FOL-abstract(y)
11. Dom,S,a +|= FOL-abstract(x)
⊢ (Dom,S,a +|= FOL-abstract(x) ∧ Dom,S,a +|= FOL-abstract(y)) ⋃ (S "false" [])

---

Latex:

---

Latex:
\mforall{}hyps:mFOL()  List
    \mforall{}[x,y:mFOL()].    (FOL-sequent-evidence\{i:l\}(<hyps,  x>)  {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(<hyps,  y>)  {}\mRightarrow{}  F\000COL-sequent-evidence\{i:l\}(<hyps,  x  \mwedge{}  y>))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  ((Assert  Dom,S,a  +|=  FOL-sequent-abstract(<hyps,  x>)  \mwedge{}  Dom,S,a  +|=  FOL-sequent-abstract(<hyps,\000C  y>)  BY
                            (Auto
                              THEN  All  (RepUR  ``FOL-sequent-evidence  FO-uniform-evidence``)
                              THEN  BackThruSomeHyp
                              THEN  (DoSubsume  THEN  Auto)
                              THEN  SubtypeReasoning1
                              THEN  Auto
                              THEN  BLemma\_o  (ioid  Obid:  mFOL-sequent-freevars-subset-3)\mcdot{}
                              THEN  Auto
                              THEN  RepUR  ``mFOL-freevars``  0
                              THEN  Fold  `mFOL-freevars`  0
                              THEN  RWO  "val-union-l-union"  0
                              THEN  Auto))
              THEN  (D  -1
                          THEN  All  (RepUR  ``FOL-sequent-abstract  FOSatWith+``)\mcdot{}
                          THEN  (All  (Fold  `implies`)  THEN  All  (Fold  `FOSatWith+`))
                          THEN  Auto
                          THEN  ThinTrivial
                          THEN  (RepUR  ``FOL-abstract``  0
                                      THEN  Fold  `FOL-abstract`  0
                                      THEN  RepUR  ``FOConnective+  FOSatWith+  let``  0
                                      THEN  All  (Fold  `FOSatWith+`)
                                      THEN  Auto)\mcdot{})
              )\mcdot{})

---

Home Index