Nuprl Lemma : parallel-class-single-val

[Info,A:Type].

[es:EO+(Info)].

[X,Y:EClass(A)].
  (single-valued-classrel(es;X || Y;A)) supposing
     (single-valued-classrel(es;X;A) and
     single-valued-classrel(es;Y;A) and
     disjoint-classrel(es;A;X;A;Y))

Proof not projected

Definitions occuring in Statement : parallel-class: X || Y, single-valued-classrel: single-valued-classrel(es;X;T), disjoint-classrel: disjoint-classrel(es;A;X;B;Y), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), uimplies: b supposing a, uall:

[x:A]. B[x], universe: Type
Definitions : single-valued-classrel: single-valued-classrel(es;X;T), all:

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

Q, member: t

T, so_lambda:

x y.t[x; y], disjoint-classrel: disjoint-classrel(es;A;X;B;Y), uimplies: b supposing a, sq_or: a

b, uiff: uiff(P;Q), uall:

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

Q, squash:

T, or: P

Q, false: False, not:

A, prop:

, so_apply: x[s1;s2], subtype: S

T, guard: {T}
Lemmas : parallel-classrel, classrel_wf, parallel-class_wf, es-E_wf, event-ordering+_inc, single-valued-classrel_wf, disjoint-classrel_wf, eclass_wf, event-ordering+_wf

\mforall{}[Info,A:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X,Y:EClass(A)]. (single-valued-classrel(es;X || Y;A)) supposing (single-valued-classrel(es;X;A) and single-valued-classrel(es;Y;A) and disjoint-classrel(es;A;X;A;Y)) Date html generated: 2012_01_23-PM-01_17_44 Last ObjectModification: 2012_01_11-PM-05_29_51 Home Index