### Nuprl 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)))`

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 ∈ T`
Lemmas :  es-causl-swellfnd event-ordering+_subtype nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf int_seg_wf int_seg_subtype-nat decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__equal_int subtype_rel-int_seg le_weakening int_seg_properties le_wf nat_wf zero-le-nat lelt_wf es-causl_wf es-locl-total es-E-interface-property assert_wf in-eclass_wf equal_wf decidable__lt not-equal-2 le-add-cancel-alt not-le-2 sq_stable__le add-mul-special zero-mul surject_wf es-E-interface_wf es-interface-subtype_rel2 es-E_wf event-ordering+_wf top_wf es-fwd-propagation-via_wf all_wf Id_wf es-loc_wf eclass_wf assert_elim subtype_base_sq bool_wf bool_subtype_base and_wf es-locl_transitivity2 es-le_weakening es-le_weakening_eq es-locl_irreflexivity es-causl_weakening

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

Date html generated: 2015_07_21-PM-03_27_19
Last ObjectModification: 2015_01_27-PM-06_49_03

Home Index