Nuprl Lemma : eo-reset-dom-reset-dom

[es:EO]. ∀[d1,d2:es-base-E(es) ⟶ 𝔹].  (eo-reset-dom(eo-reset-dom(es;d1);d2) eo-reset-dom(es;d2) ∈ EO)


Proof




Definitions occuring in Statement :  eo-reset-dom: eo-reset-dom(es;d) es-base-E: es-base-E(es) event_ordering: EO bool: 𝔹 uall: [x:A]. B[x] function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T eo-reset-dom: eo-reset-dom(es;d) top: Top

Latex:
\mforall{}[es:EO].  \mforall{}[d1,d2:es-base-E(es)  {}\mrightarrow{}  \mBbbB{}].    (eo-reset-dom(eo-reset-dom(es;d1);d2)  =  eo-reset-dom(es;d2))



Date html generated: 2016_05_16-AM-09_14_02
Last ObjectModification: 2015_12_28-PM-09_58_27

Theory : new!event-ordering


Home Index