| Constructores | semwhilefa:
(m:memory)(e:bexpr)(c:com) (bexprval m e false) ->(semcom m (while e c) m) |
semwhiletr:
(m1,m2:memory)(e:bexpr)(c:com) (bexprval m1 e true) ->(m3:memory)(semcom m1 c m3) ->(semcom m3 (while e c) m2) ->(semcom m1 (while e c) m2) |
| Unificación | (semcom m (while b c) m')
------------------------- (semcom m (while e c) m) |
(semcom m (while b
c) m')
-------------------------- (semcom m1 (while e c) m2) |
| b=e | m1=m | |
| m'=m | m2=m' | |
| b=e | ||
| Premisa
Hipótesis |
(bexprval m e false)
(bexprval m b false) |
(semcom m3 (while e c) m2)
(semcom m3 (while b c) m') |
| Premisa
Hipótesis |
(bexprval m1 e true)
(bexprval m b true) |
|
| Premisa
Hipótesis |
(semcom m1 c m3)
(semcom m c m3) |
|
| Subobjetivos | (semcom
m' (cond b (seq c (while b c)) skip) m') |
(semcom
m (cond b (seq c (while b c)) skip) m') |