Después de   Inversion H
 
 
 
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')