Nuprl Lemma : parallel-classrel

[T,Info:Type]. ∀[X,Y:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].  uiff(v ∈ || Y(e);v ∈ X(e) ↓∨ v ∈ Y(e))


Proof




Definitions occuring in Statement :  parallel-class: || Y classrel: v ∈ X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E sq_or: a ↓∨ b uiff: uiff(P;Q) uall: [x:A]. B[x] universe: Type
Lemmas :  bag-member-append
\mforall{}[T,Info:Type].  \mforall{}[X,Y:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
    uiff(v  \mmember{}  X  ||  Y(e);v  \mmember{}  X(e)  \mdownarrow{}\mvee{}  v  \mmember{}  Y(e))



Date html generated: 2015_07_17-PM-00_46_23
Last ObjectModification: 2015_01_27-PM-11_06_08

Home Index