m : memory
m' : memory b : bexpr c : com H : (semcom m (while b c) m') m1 : memory m2 : memory e : bexpr c0 : com m3 : memory H3 : m1=m H0 : e=b H1 : c0=c H5 : m2=m' H2 : (bexprval m b true) H4 : (semcom m c m3) H6 : (semcom m3 (while b c) m') ============================ (semcom m (cond b (seq c (while b c)) skip) m') |
m : memory
m' : memory b : bexpr c : com H : (semcom m (while b c) m') m0 : memory e : bexpr c0 : com H1 : m0=m H0 : e=b H3 : c0=c H2 : m=m' H4 : (bexprval m' b false) ============================ (semcom m' (cond b (seq c (while b c)) skip) m') |