Nuprl Lemma : Accum-loc-classrel-Memory-sq

[B,f,init,X,es,e,v:Top].
(v

Accum-loc-class(f;init;X)(e) ~ v

lifting-loc-2(f) loc(e) (X es e) (Memory-loc-class(f;init;X) es e))

Proof not projected

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

X(e), es-loc: loc(e), uall:

[x:A]. B[x], top: Top, apply: f a, sqequal: s ~ t, bag-member: x

bs
Definitions : uall:

[x:A]. B[x], classrel: v

X(e), Accum-loc-class: Accum-loc-class(f;init;X), Memory-loc-class: Memory-loc-class(f;init;X), member: t

T, rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|, rec-comb: rec-comb(X;f;init), select: l[i], ycomb: Y, ifthenelse: if b then t else f fi , le_int: i

z j, bnot:

b, lt_int: i <z j, bfalse: ff, btrue: tt
Lemmas : top_wf

\mforall{}[B,f,init,X,es,e,v:Top]. (v \mmember{} Accum-loc-class(f;init;X)(e) \msim{} v \mdownarrow{}\mmember{} lifting-loc-2(f) loc(e) (X es e) (Memory-loc-class(f;init;X) es e)) Date html generated: 2012_01_23-PM-12_57_25 Last ObjectModification: 2012_01_11-AM-11_44_39 Home Index