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
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 unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
Memory-loc-class: Memory-loc-class(f;init;X),
Accum-loc-class: Accum-loc-class(f;init;X),
classrel: v ∈ X(e),
rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|,
rec-comb: rec-comb(X;f;init),
select: L[n],
cons: [a / b]
Latex:
\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:
2016_05_17-AM-09_21_50
Last ObjectModification:
2015_12_29-PM-04_06_11
Theory : classrel!lemmas
Home
Index