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
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
Lemmas :
top_wf
Latex:
\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:
2015_07_22-PM-00_11_24
Last ObjectModification:
2015_01_28-AM-11_40_13
Home
Index