---

Step * 2 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. Surj(E(X);E(Y);g)
18. x : E(X)@i
19. ∀x1:E(X). ((x1 < x) ⇒ ((f x1) = (g x1) ∈ E(Y)))
20. (g x <loc f x)
⊢ (f x) = (g x) ∈ E(Y)
BY
{ (((With ⌜g x⌝ (D (-5))⋅ THENM ExRepD) THENA Auto)
   THEN (InstLemma `es-locl-total` [⌜es⌝;⌜x⌝;⌜a⌝]⋅ THENM SplitOrHyps)
   THEN Auto) }

1
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);g)
17. x : E(X)@i
18. ∀x1:E(X). ((x1 < x) ⇒ ((f x1) = (g x1) ∈ E(Y)))
19. (g x <loc f x)
20. a : E(X)
21. (f a) = (g x) ∈ E(Y)
22. (x <loc a)
⊢ (f x) = (g x) ∈ E(Y)

2
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);g)
17. x : E(X)@i
18. ∀x1:E(X). ((x1 < x) ⇒ ((f x1) = (g x1) ∈ E(Y)))
19. (g x <loc f x)
20. a : E(X)
21. (f a) = (g x) ∈ E(Y)
22. (a <loc x)
⊢ (f x) = (g x) ∈ E(Y)

---

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.  Surj(E(X);E(Y);g)
18.  x  :  E(X)@i
19.  \mforall{}x1:E(X).  ((x1  <  x)  {}\mRightarrow{}  ((f  x1)  =  (g  x1)))
20.  (g  x  <loc  f  x)
\mvdash{}  (f  x)  =  (g  x)


By

---

Latex:
(((With  \mkleeneopen{}g  x\mkleeneclose{}  (D  (-5))\mcdot{}  THENM  ExRepD)  THENA  Auto)
  THEN  (InstLemma  `es-locl-total`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENM  SplitOrHyps)
  THEN  Auto)

---

Home Index