---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X,Y:EClass(T)]. ∀[f,g:E(X) ⟶ E(Y)].
  (f = g ∈ (E(X) ⟶ E(Y))) supposing 
     (Surj(E(X);E(Y);g) and 
     Surj(E(X);E(Y);f) and 
     g:X ⇒ Y:T and 
     f:X ⇒ Y:T and 
     (∀y1,y2:E(Y).  (loc(y1) = loc(y2) ∈ Id)) and 
     (∀x1,x2:E(X).  (loc(x1) = loc(x2) ∈ Id)))
BY
{ (Auto
   THEN D -4
   THEN D -3
   THEN Ext
   THEN Auto
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN (InstLemma `es-locl-total` [⌜es⌝;⌜f x⌝;⌜g x⌝]⋅ 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);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. (f x <loc g x)
⊢ (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);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)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X,Y:EClass(T)].  \mforall{}[f,g:E(X)  {}\mrightarrow{}  E(Y)].
    (f  =  g)  supposing 
          (Surj(E(X);E(Y);g)  and 
          Surj(E(X);E(Y);f)  and 
          g:X  {}\mRightarrow{}  Y:T  and 
          f:X  {}\mRightarrow{}  Y:T  and 
          (\mforall{}y1,y2:E(Y).    (loc(y1)  =  loc(y2)))  and 
          (\mforall{}x1,x2:E(X).    (loc(x1)  =  loc(x2))))


By

---

Latex:
(Auto
  THEN  D  -4
  THEN  D  -3
  THEN  Ext
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  (InstLemma  `es-locl-total`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}f  x\mkleeneclose{};\mkleeneopen{}g  x\mkleeneclose{}]\mcdot{}  THENM  SplitOrHyps)
  THEN  Auto)

---

Home Index