---

Step * 1 of Lemma mFOL-sequent-evidence_transitivity2


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>)
BY
{ (Assert Dom,S,a |= mFOL-sequent-abstract(<hyps, y>) 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>)
11. Dom,S,a |= mFOL-sequent-abstract(<hyps, y>)
⊢ Dom,S,a |= mFOL-sequent-abstract(<hyps, x>)

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  [x]  :  mFOL()
3.  [y]  :  mFOL()
4.  mFOL-freevars(y)  \msubseteq{}  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>)
\mvdash{}  Dom,S,a  |=  mFOL-sequent-abstract(<hyps,  x>)


By

---

Latex:
(Assert  Dom,S,a  |=  mFOL-sequent-abstract(<hyps,  y>)  BY
              (Auto
                THEN  All  (RepUR  ``mFOL-sequent-evidence  mFO-uniform-evidence``)
                THEN  BackThruSomeHyp
                THEN  (DoSubsume  THEN  Auto)
                THEN  SubtypeReasoning1
                THEN  Auto))

---

Home Index