Go backward to Simplification II Go up to Top Go forward to Program Equivalence |
let s3 = [ [[A]] |-> zero ]newstore
s4 = [ [[Z]] |-> one ]s3
s5 = C[[if A=0
then diverge]]s4
s' = C[[Z:=3]]s5
in access [[Z]] s'
= let s3 = [ [[A]] |-> zero ]newstore
s4 = [ [[Z]] |-> one ]s3
s5 = _|_
s' = C[[Z:=3]]s5
in access [[Z]] s'
= let s' = C[[Z:=3]]_|_
in access [[Z]] s'
= let s' = (lambdas.update [[Z]]
(E[[3]]s))_|_
inaccess [[Z]] s'
= let s' = _|_
inaccess [[Z]] s'
= access [[Z]] _|_
= _|_