Nuprl Lemma : sq_stable__no-prior-classrel

[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E].  SqStable((no prior to e))


Proof




Definitions occuring in Statement :  no-prior-classrel: (no prior to e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E sq_stable: SqStable(P) uall: [x:A]. B[x] universe: Type
Lemmas :  sq_stable__all es-E_wf event-ordering+_subtype es-locl_wf all_wf not_wf classrel_wf sq_stable__not squash_wf event-ordering+_wf eclass_wf
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    SqStable((no  X  prior  to  e))



Date html generated: 2015_07_17-PM-00_29_28
Last ObjectModification: 2015_01_27-PM-11_32_38

Home Index