---

{ [Info:Type]. [es:EO+(Info)]. [T:Type]. [X,Y:EClass(T)].
  [f,g:E(X)  E(Y)].
    (f = g) 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))) and 
       (x1,x2:E(X).  (loc(x1) = loc(x2)))) }

{ Proof }

---

Definitions occuring in Statement :  es-fwd-propagation-via: f:X  Y:T,  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-loc: loc(e),  Id: Id,  surject: Surj(A;B;f),  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  function: x:A  B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  es-E-interface: E(X),  uimplies: b supposing a,  all: x:A. B[x],  member: t  T,  nat: ,  implies: P  Q,  guard: {T},  assert: b,  prop: ,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  ge: i  j ,  le: A  B,  not: A,  false: False,  label: ...$L... t,  es-fwd-propagation-via: f:X  Y:T,  and: P  Q,  strongwellfounded: SWellFounded(R[x; y]),  exists: x:A. B[x],  so_apply: x[s1;s2],  or: P  Q,  sq_type: SQType(T),  surject: Surj(A;B;f),  es-locl-op: LocalOrderPreserving(f),  order-preserving: order-preserving(A;B;a1,a2.R1[a1; a2];b1,b2.R2[b1; b2];f),  es-locl: (e <loc e'),  inject: Inj(A;B;f),  subtype: S  T
Lemmas :  es-causl-swellfnd,  event-ordering+_inc,  nat_wf,  le_wf,  es-E-interface_wf,  surject_wf,  es-interface-top,  es-fwd-propagation-via_wf,  Id_wf,  es-loc_wf,  eclass_wf,  es-E_wf,  event-ordering+_wf,  es-causl_wf,  es-locl-total,  es-E-interface-subtype_rel,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert_wf,  in-eclass_wf,  assert_elim,  nat_properties,  ge_wf,  es-locl_transitivity2,  es-le_weakening,  es-le_weakening_eq,  es-locl_irreflexivity

---

\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))))


Date html generated: 2011_08_16-PM-05_13_49
Last ObjectModification: 2011_06_20-AM-01_14_39

Home Index