Nuprl Lemma : Memory4-locally-programmable

A1,A2,A3,A4,B:{T:

'| valueall-type(T)} .

init:Id

bag(B).

tr1:Id

A1

B

B.

[X1:EClass'(A1)]

tr2:Id

A2

B

[X2:EClass'(A2)]

tr3:Id

A3

B

[X3:EClass'(A3)]

tr4:Id

A4

B

[X4:EClass'(A4)]
(NormalLProgrammable'(A1;X1)

NormalLProgrammable'(A2;X2)

NormalLProgrammable'(A3;X3)

NormalLProgrammable'(A4;X4)

NormalLProgrammable'(B;Memory4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4)))

Proof not projected

Definitions occuring in Statement : Memory4: Memory4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4), 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], 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, Memory4: Memory4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4), Memory-loc-class: Memory-loc-class(f;init;X), Accum-loc-class: Accum-loc-class(f;init;X), member: t

T, lifting-loc-2: lifting-loc-2(f), empty-bag: {}, lifting-gen-list-rev: lifting-gen-list-rev(n;bags), select: l[i], lifting2-loc: lifting2-loc(f;loc;abag;bbag), lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f), lifting-gen-rev: lifting-gen-rev(n;f;bags), ifthenelse: if b then t else f fi , eq_int: (i =

j), bag-combine:

x

bs.f[x], ycomb: Y, map: map(f;as), bfalse: ff, bag-union: bag-union(bbs), concat: concat(ll), reduce: reduce(f;k;as), bag-map: bag-map(f;bs), le_int: i

z j, bnot:

b, lt_int: i <z j, btrue: tt, squash:

T, true: True, uimplies: b supposing a, sq_stable: SqStable(P), prop:

, subtype: S

T
Lemmas : primed-class-opt-nlp, Accum-loc-class_wf, Message_wf, disjoint-union-tr_wf, disjoint-union-comb_wf, rec-combined-loc-class-opt-1-nlp, lifting-loc-2_wf, empty-bag_wf, bag_wf, Id_wf, disjoint-union-comb-nlp, union-valueall-type, sq_stable__valueall-type, valueall-type_wf, normal-locally-programmable_wf, event-ordering+_wf, es-E_wf, event-ordering+_inc

\mforall{}A1,A2,A3,A4,B:\{T:\mBbbU{}'| valueall-type(T)\} . \mforall{}init:Id {}\mrightarrow{} bag(B). \mforall{}tr1:Id {}\mrightarrow{} A1 {}\mrightarrow{} B {}\mrightarrow{} B. \mforall{}[X1:EClass'(A1)] \mforall{}tr2:Id {}\mrightarrow{} A2 {}\mrightarrow{} B {}\mrightarrow{} B \mforall{}[X2:EClass'(A2)] \mforall{}tr3:Id {}\mrightarrow{} A3 {}\mrightarrow{} B {}\mrightarrow{} B \mforall{}[X3:EClass'(A3)] \mforall{}tr4:Id {}\mrightarrow{} A4 {}\mrightarrow{} B {}\mrightarrow{} B \mforall{}[X4:EClass'(A4)] (NormalLProgrammable'(A1;X1) {}\mRightarrow{} NormalLProgrammable'(A2;X2) {}\mRightarrow{} NormalLProgrammable'(A3;X3) {}\mRightarrow{} NormalLProgrammable'(A4;X4) {}\mRightarrow{} NormalLProgrammable'(B;Memory4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4))) Date html generated: 2012_01_23-PM-01_31_28 Last ObjectModification: 2012_01_12-AM-11_19_37 Home Index