theorem Th49: :: SCMPDS_7:51

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Nat st s . GBP = 0 & s . (intpos 2) = n & s . (intpos 3) = 0 holds
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,s)) . (intpos 3) = n