---

Step * 1 1 of Lemma FOL-sequent-evidence_transitivity2


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>)
11. Dom,S,a +|= FOL-sequent-abstract(<hyps, y>)
⊢ Dom,S,a +|= FOL-sequent-abstract(<hyps, x>)
BY
{ (All (RepUR ``FOL-sequent-abstract FOSatWith+``)⋅
   THEN (All (Fold `implies`) THEN All (Fold `FOSatWith+`))
   THEN Auto
   THEN BackThruSomeHyp
   THEN RepUR ``FOL-hyps-meaning`` 0
   THEN (Fold `FOL-hyps-meaning` 0 THEN Fold `and` 0)
   THEN (Subst' null(FOL-hyps-meaning(Dom;S;a;hyps)) ~ null(hyps) 0
         THENA (RepUR ``FOL-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.  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>)
11.  Dom,S,a  +|=  FOL-sequent-abstract(<hyps,  y>)
\mvdash{}  Dom,S,a  +|=  FOL-sequent-abstract(<hyps,  x>)


By

---

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

---

Home Index