Nuprl Lemma : es-E-equality-univ-independent

∀[es:EO]. ∀[e,e':E].
  (TERMOF{decidable__es-E-equal:o, 1:l, i:l} es e' e ~ TERMOF{decidable__es-E-equal:o, 1:l, 1:l} es e' e)


Proof



Definitions occuring in Statement :  es-E: E,  event_ordering: EO,  uall: ∀[x:A]. B[x],  apply: f a,  sqequal: s ~ t
Lemmas :  es-E_wf,  event_ordering_wf
\mforall{}[es:EO].  \mforall{}[e,e':E].
    (TERMOF\{decidable\_\_es-E-equal:o,  1:l,  i:l\}  es  e'  e  \msim{}  TERMOF\{decidable\_\_es-E-equal:o,  1:l,  1:l\}  es 
                                                                                                              e' 
                                                                                                              e)


Date html generated: 2015_07_17-AM-08_36_44
Last ObjectModification: 2015_01_27-PM-02_57_55

Home Index