Nuprl Lemma : Memory-loc-class-invariant

[Info,B,A:Type].

P:B

.

f:Id

A

B

B.

init:Id

bag(B).

X:EClass(A).

es:EO+(Info).

e:E.

v:B.
((

s:B. SqStable(P[s]))

(

a:A.

e':E. ((e' <loc e)

a

X(e')

(

s:B. (P[s]

P[f loc(e') a s]))))

(

v:B. (v

init loc(e)

P[v]))

v

Memory-loc-class(f;init;X)(e)

P[v])

Proof not projected

Definitions occuring in Statement : Memory-loc-class: Memory-loc-class(f;init;X), classrel: v

X(e), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-locl: (e <loc e'), es-loc: loc(e), es-E: E, Id: Id, sq_stable: SqStable(P), uall:

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

, so_apply: x[s], all:

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

Q, apply: f a, function: x:A

B[x], universe: Type, bag-member: x

bs, bag: bag(T)
Definitions : uall:

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

x:A. B[x], prop:

, implies: P

Q, so_apply: x[s], member: t

T, so_lambda:

x.t[x], so_lambda:

x y.t[x; y], and: P

Q, es-locl: (e <loc e'), uimplies: b supposing a, uiff: uiff(P;Q), so_apply: x[s1;s2], subtype: S

T
Lemmas : Memory-classrel-loc, Memory-class-invariant, es-loc_wf, classrel_wf, es-locl_wf, Memory-loc-class_wf, all_wf, bag-member_wf, event-ordering+_inc, es-E_wf, sq_stable_wf, event-ordering+_wf, eclass_wf, Id_wf, bag_wf, and_wf, equal_wf

\mforall{}[Info,B,A:Type]. \mforall{}P:B {}\mrightarrow{} \mBbbP{}. \mforall{}f:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B. \mforall{}init:Id {}\mrightarrow{} bag(B). \mforall{}X:EClass(A). \mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}v:B. ((\mforall{}s:B. SqStable(P[s])) {}\mRightarrow{} (\mforall{}a:A. \mforall{}e':E. ((e' <loc e) {}\mRightarrow{} a \mmember{} X(e') {}\mRightarrow{} (\mforall{}s:B. (P[s] {}\mRightarrow{} P[f loc(e') a s])))) {}\mRightarrow{} (\mforall{}v:B. (v \mdownarrow{}\mmember{} init loc(e) {}\mRightarrow{} P[v])) {}\mRightarrow{} v \mmember{} Memory-loc-class(f;init;X)(e) {}\mRightarrow{} P[v]) Date html generated: 2012_01_23-PM-01_02_47 Last ObjectModification: 2012_01_21-PM-08_39_37 Home Index