---

Step * of Lemma goes-thru-goes-thru-last

∀[Info:Type]
  ∀es:EO+(Info). ∀Sys:EClass(Top). ∀f:sys-antecedent(es;Sys). ∀x,y:E(Sys). ∀i:Id.
    x-f*-y thru i ⇒ x-f*-y goes thru i last supposing ¬(loc(x) = i ∈ Id)
BY
{ Auto }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. Sys : EClass(Top)@i'
4. f : sys-antecedent(es;Sys)@i
5. x : E(Sys)@i
6. y : E(Sys)@i
7. i : Id@i
8. ¬(loc(x) = i ∈ Id)
9. x-f*-y thru i@i
⊢ x-f*-y goes thru i last

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}Sys:EClass(Top).  \mforall{}f:sys-antecedent(es;Sys).  \mforall{}x,y:E(Sys).  \mforall{}i:Id.
        x-f*-y  thru  i  {}\mRightarrow{}  x-f*-y  goes  thru  i  last  supposing  \mneg{}(loc(x)  =  i)


By

---

Latex:
Auto

---

Home Index