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

proof

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

end;

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