Go backward to Simplification
Go up to Top
Go forward to Simplification
|
Go backward to Simplification Go up to Top Go forward to Simplification |
|
(access [[A]] s2) equals zero
= two equals zero
= false
C[[Z:=3]](B[[A=0]]s2 ->
C[[diverge]]s2 [] s2)
= C[[Z:=3]](false ->
C[[diverge]]s2 [] s2)
= C[[Z:=3]]s2
= (lambdas.update [[Z]] (E[[3]]s) s)s2
= update [[Z]] (E[[3]]s2) s2
= update [[Z]] (N[[3]]) s2
= update [[Z]] three s2
= [ [[Z]] |-> three ]s2