Nuprl Lemma : parallel-classrel

[T,Info:Type].

[X,Y:EClass(T)].

[es:EO+(Info)].

[e:E].

[v:T]. uiff(v

X || Y(e);v

X(e)

v

Y(e))

Proof not projected

Definitions occuring in Statement : parallel-class: X || 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
Definitions : so_lambda:

x y.t[x; y], bag-member: x

bs, true: True, uimplies: b supposing a, and: P

Q, member: t

T, squash:

T, sq_or: a

b, classrel: v

X(e), uiff: uiff(P;Q), uall:

[x:A]. B[x], eclass: EClass(A[eo; e]), eclass-compose2: eclass-compose2(f;X;Y), parallel-class: X || Y, so_apply: x[s1;s2], all:

x:A. B[x], iff: P

Q, implies: P

Q, rev_implies: P

Q, subtype: S

T, prop:

Lemmas : eclass_wf, event-ordering+_wf, event-ordering+_inc, es-E_wf, or_wf, squash_wf, parallel-class_wf, classrel_wf, 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: 2012_01_23-PM-12_52_59 Last ObjectModification: 2011_12_11-PM-01_20_46 Home Index