theorem :: SCMPDS_6:126

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of holds
( I is_halting_on s,P iff I is_halting_on Initialize s,P ) ;