[[P:H]] in [[H]], for
every well-typed phrase P:H
- Case n: int
- [[n: int]] = n in Int = [[int]]
- Case @L: intexp
- We know [[L: intloc]] = l in [[intloc]] =
Location. Then, for every Store s, [[@L: intexp]](s) =
lookup(l, s) in Int i.e. [[@L: intexp]] in Store -> Int = [[intexp]].
- Case C_1;C_2: comm
- We know [[C_1: comm]] and [[C_2: comm]] are elements of
Store -> Store_bottom. For every Store s,
we
have [[C_1;C_2: comm]](s) = [[C_2: comm]]([[C_1:
comm]](s)) and [[C_2:comm]](s) = s_1 in Store_bottom. If s_1=bottom,
[[C_2: comm]](s_1)=bottom in Store_bottom. If s_1 in Store, then
[[C_2: comm]](s_1) in Store_bottom. Hence,
[[C_1;C_2: comm]] in Store ->
Store_bottom = [[comm]].
Prove one case for each typing rule.
