---

Step * 1 1 1 of Lemma es-fwd-propagation-via-unique


1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T)
5. Y : EClass(T)
6. f : E(X) ─→ E(Y)
7. g : E(X) ─→ E(Y)
8. ∀x1,x2:E(X).  (loc(x1) = loc(x2) ∈ Id)
9. ∀y1,y2:E(Y).  (loc(y1) = loc(y2) ∈ Id)
10. ∀e:E(X). ((Y(f e) = X(e) ∈ T) ∧ (e < f e))
11. LocalOrderPreserving(f)
12. Inj(E(X);E(Y);f)
13. ∀e:E(X). ((Y(g e) = X(e) ∈ T) ∧ (e < g e))
14. LocalOrderPreserving(g)
15. Inj(E(X);E(Y);g)
16. Surj(E(X);E(Y);f)
17. x : E(X)@i
18. ∀x1:E(X). ((x1 < x) ⇒ ((f x1) = (g x1) ∈ E(Y)))
19. (f x <loc g x)
20. a : E(X)
21. (g a) = (f x) ∈ E(Y)
22. (x <loc a)
23. (g x <loc g a)
⊢ (f x) = (g x) ∈ E(Y)
BY
{ (RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  T  :  Type
4.  X  :  EClass(T)
5.  Y  :  EClass(T)
6.  f  :  E(X)  {}\mrightarrow{}  E(Y)
7.  g  :  E(X)  {}\mrightarrow{}  E(Y)
8.  \mforall{}x1,x2:E(X).    (loc(x1)  =  loc(x2))
9.  \mforall{}y1,y2:E(Y).    (loc(y1)  =  loc(y2))
10.  \mforall{}e:E(X).  ((Y(f  e)  =  X(e))  \mwedge{}  (e  <  f  e))
11.  LocalOrderPreserving(f)
12.  Inj(E(X);E(Y);f)
13.  \mforall{}e:E(X).  ((Y(g  e)  =  X(e))  \mwedge{}  (e  <  g  e))
14.  LocalOrderPreserving(g)
15.  Inj(E(X);E(Y);g)
16.  Surj(E(X);E(Y);f)
17.  x  :  E(X)@i
18.  \mforall{}x1:E(X).  ((x1  <  x)  {}\mRightarrow{}  ((f  x1)  =  (g  x1)))
19.  (f  x  <loc  g  x)
20.  a  :  E(X)
21.  (g  a)  =  (f  x)
22.  (x  <loc  a)
23.  (g  x  <loc  g  a)
\mvdash{}  (f  x)  =  (g  x)


By

---

Latex:
(RelRST  THEN  Auto)

---

Home Index