theorem Th48:
for
P being
Instruction-Sequence of
SCMPDS for
s being
0 -started State of
SCMPDS st
s . GBP = 0 holds
(
for-down (
GBP,2,1,
(Load (AddTo (GBP,3,1))))
is_closed_on s,
P &
for-down (
GBP,2,1,
(Load (AddTo (GBP,3,1))))
is_halting_on s,
P )