---

Step * of Lemma mFOL-sequent-evidence_transitivity2

∀hyps:mFOL() List. ∀[x,y:mFOL()].  (mFOL-freevars(y) ⊆ mFOL-sequent-freevars(<hyps, x>) ⇒ mFOL-sequent-evidence(<hyps, \000Cy>) ⇒ mFOL-sequent-evidence(<[y / hyps], x>) ⇒ mFOL-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 (DoSubsume THEN Auto)
                THEN SubtypeReasoning1
                THEN Auto))⋅) }

1
1. hyps : mFOL() List
2. [x] : mFOL()
3. [y] : mFOL()
4. mFOL-freevars(y) ⊆ mFOL-sequent-freevars(<hyps, x>)
5. mFOL-sequent-evidence(<hyps, y>)
6. mFOL-sequent-evidence(<[y / hyps], x>)
7. [Dom] : Type
8. [S] : FOStruct(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, x>),Dom)
10. Dom,S,a |= mFOL-sequent-abstract(<[y / hyps], x>)
⊢ Dom,S,a |= mFOL-sequent-abstract(<hyps, x>)

---

Latex:

---

Latex:
\mforall{}hyps:mFOL()  List
    \mforall{}[x,y:mFOL()].    (mFOL-freevars(y)  \msubseteq{}  mFOL-sequent-freevars(<hyps,  x>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyp\000Cs,  y>)  {}\mRightarrow{}  mFOL-sequent-evidence(<[y  /  hyps],  x>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  x>))


By

---

Latex:
(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  (DoSubsume  THEN  Auto)
                            THEN  SubtypeReasoning1
                            THEN  Auto))\mcdot{})

---

Home Index