---

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


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
BY
{ ((D -1 THEN Auto) THEN UnfoldTopAb (0)) }

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. e : E(Sys)@i
10. loc(e) = i ∈ Id@i
11. e is f*(y)@i
12. x is f*(e)@i
⊢ ∃e:E(Sys). (((loc(e) = i ∈ Id) ∧ (¬(loc(f e) = loc(e) ∈ Id))) ∧ e is f*(y) ∧ x is f*(e))

---

Latex:

---

Latex:

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.  \mneg{}(loc(x)  =  i)
9.  x-f*-y  thru  i@i
\mvdash{}  x-f*-y  goes  thru  i  last


By

---

Latex:
((D  -1  THEN  Auto)  THEN  UnfoldTopAb  (0))

---

Home Index