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
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
Memory-class: Memory-class(f;init;X)
, 
Accum-class: Accum-class(f;init;X)
, 
classrel: v ∈ X(e)
, 
rec-combined-class-opt-1: F|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-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:
2016_05_17-AM-09_21_47
Last ObjectModification:
2015_12_29-PM-04_06_14
Theory : classrel!lemmas
Home
Index