---

Step * 1 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>)
11. Dom,S,a |= mFOL-sequent-abstract(<hyps, y>)
⊢ Dom,S,a |= mFOL-sequent-abstract(<hyps, x>)
BY
{ (All (RepUR ``mFOL-sequent-abstract FOSatWith``)⋅
   THEN (All (Fold `implies`) THEN All (Fold `FOSatWith`))
   THEN Auto
   THEN BackThruSomeHyp
   THEN RepUR ``mFOL-hyps-meaning`` 0
   THEN (Fold `mFOL-hyps-meaning` 0 THEN Fold `and` 0)
   THEN (Subst' null(mFOL-hyps-meaning(Dom;S;a;hyps)) ~ null(hyps) 0
         THENA (RepUR ``mFOL-hyps-meaning`` 0 THEN RWO "null-map" 0 THEN Auto)
         )
   THEN AutoSplit) }

---

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


By

---

Latex:
(All  (RepUR  ``mFOL-sequent-abstract  FOSatWith``)\mcdot{}
  THEN  (All  (Fold  `implies`)  THEN  All  (Fold  `FOSatWith`))
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  RepUR  ``mFOL-hyps-meaning``  0
  THEN  (Fold  `mFOL-hyps-meaning`  0  THEN  Fold  `and`  0)
  THEN  (Subst'  null(mFOL-hyps-meaning(Dom;S;a;hyps))  \msim{}  null(hyps)  0
              THENA  (RepUR  ``mFOL-hyps-meaning``  0  THEN  RWO  "null-map"  0  THEN  Auto)
              )
  THEN  AutoSplit)

---

Home Index