Nuprl Lemma : SM2-class-du-locally-programmable

A,B,C:{T:

'| valueall-type(T)} .

init:Id

bag(C).

tr1:Id

A

C

C.

[X1:EClass'(A)]

tr2:Id

B

C

[X2:EClass'(B)]
(NormalLProgrammable'(A;X1)

NormalLProgrammable'(B;X2)

NormalLProgrammable'(C;SM2-class-du(init;<tr1, X1>;<tr2, X2>)))

Proof not projected

Definitions occuring in Statement : SM2-class-du: SM2-class-du(init;trX1;trX2), Message: Message, normal-locally-programmable: NormalLProgrammable(A;X), eclass: EClass(A[eo; e]), Id: Id, uall:

[x:A]. B[x], all:

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

Q, set: {x:A| B[x]} , function: x:A

B[x], pair: <a, b>, universe: Type, bag: bag(T), valueall-type: valueall-type(T)
Definitions : all:

x:A. B[x], uall:

[x:A]. B[x], eclass: EClass(A[eo; e]), implies: P

Q, SM2-class-du: SM2-class-du(init;trX1;trX2), member: t

T, prop:

, subtype: S

T
Lemmas : Accum-loc-class-locally-programmable, disjoint-union-tr_wf, disjoint-union-class_wf, disjoint-union-class-nlp, normal-locally-programmable_wf, Message_wf, event-ordering+_wf, es-E_wf, event-ordering+_inc, bag_wf, Id_wf, valueall-type_wf

\mforall{}A,B,C:\{T:\mBbbU{}'| valueall-type(T)\} . \mforall{}init:Id {}\mrightarrow{} bag(C). \mforall{}tr1:Id {}\mrightarrow{} A {}\mrightarrow{} C {}\mrightarrow{} C. \mforall{}[X1:EClass'(A)] \mforall{}tr2:Id {}\mrightarrow{} B {}\mrightarrow{} C {}\mrightarrow{} C \mforall{}[X2:EClass'(B)] (NormalLProgrammable'(A;X1) {}\mRightarrow{} NormalLProgrammable'(B;X2) {}\mRightarrow{} NormalLProgrammable'(C;SM2-class-du(init;<tr1, X1><tr2, X2>))) Date html generated: 2012_01_23-PM-01_07_29 Last ObjectModification: 2011_11_30-AM-10_38_56 Home Index