theorem Th3: :: AMI_3:3

for a, b being Data-Location
for s being State of SCM holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = (IC s) + 1 & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )