Nuprl Lemma : Accum-classrel-Memory-sq

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

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

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

Proof not projected

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

X(e), uall:

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

bs
Definitions : uall:

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

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

T, rec-combined-class-opt-1: F|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-class(f;init;X)(e) \msim{} v \mdownarrow{}\mmember{} lifting-2(f) (X es e) (Memory-class(f;init;X) es e)) Date html generated: 2012_01_23-PM-12_57_11 Last ObjectModification: 2012_01_11-AM-11_44_22 Home Index