---

Step * of Lemma FOL-sequent-evidence_transitivity2

∀hyps:mFOL() List. ∀[x,y:mFOL()].  (mFOL-freevars(y) ⊆ mFOL-sequent-freevars(<hyps, x>) ⇒ FOL-sequent-evidence{i:l}(<hy\000Cps, y>) ⇒ FOL-sequent-evidence{i:l}(<[y / hyps], x>) ⇒ FOL-sequent-evidence{i:l}(<hyps, x>))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert Dom,S,a +|= FOL-sequent-abstract(<[y / hyps], x>) BY
               (Auto
                THEN All (RepUR ``FOL-sequent-evidence FO-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. FOL-sequent-evidence{i:l}(<hyps, y>)
6. FOL-sequent-evidence{i:l}(<[y / hyps], x>)
7. [Dom] : Type
8. [S] : FOStruct+{i:l}(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, x>),Dom)
10. Dom,S,a +|= FOL-sequent-abstract(<[y / hyps], x>)
⊢ Dom,S,a +|= FOL-sequent-abstract(<hyps, x>)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  Dom,S,a  +|=  FOL-sequent-abstract(<[y  /  hyps],  x>)  BY
                          (Auto
                            THEN  All  (RepUR  ``FOL-sequent-evidence  FO-uniform-evidence``)
                            THEN  BackThruSomeHyp
                            THEN  (DoSubsume  THEN  Auto)
                            THEN  SubtypeReasoning1
                            THEN  Auto))\mcdot{})

---

Home Index