theorem :: SFMASTR2:25

for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for d being read-write Int-Location st s . d <= 0 holds
(IExec ((triv-times d),p,s)) . d = s . d