let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds
( I is_halting_on s,P iff I is_halting_on Initialize s,P )
let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS holds
( I is_halting_on s,P iff I is_halting_on Initialize s,P )
let I be Program of SCMPDS; :: thesis: ( I is_halting_on s,P iff I is_halting_on Initialize s,P )
thus ( I is_halting_on s,P implies I is_halting_on Initialize s,P ) :: thesis: ( I is_halting_on Initialize s,P implies I is_halting_on s,P )

proof

assume P +* (stop I) halts_on Initialize s ; :: according to SCMPDS_6:def 3 :: thesis: I is_halting_on Initialize s,P
hence P +* (stop I) halts_on Initialize (Initialize s) ; :: according to SCMPDS_6:def 3 :: thesis: verum

end;

assume P +* (stop I) halts_on Initialize (Initialize s) ; :: according to SCMPDS_6:def 3 :: thesis: I is_halting_on s,P
hence P +* (stop I) halts_on Initialize s ; :: according to SCMPDS_6:def 3 :: thesis: verum