let P be Instruction-Sequence of SCMPDS; :: thesis: for I being Program of
for s being State of SCMPDS
for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),()) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) <> halt SCMPDS

let I be Program of ; :: thesis: for s being State of SCMPDS
for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),()) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) <> halt SCMPDS

let s be State of SCMPDS; :: thesis: for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),()) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) <> halt SCMPDS

let k be Nat; :: thesis: ( I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),()) implies CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) <> halt SCMPDS )
set ss = Initialize s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),());
assume that
A1: I is_halting_on s,P and
A2: k < LifeSpan ((P +* (stop I)),()) ; :: thesis: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) <> halt SCMPDS
assume A3: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) = halt SCMPDS ; :: thesis: contradiction
P +* (stop I) halts_on Initialize s by ;
hence contradiction by A2, A3, EXTPRO_1:def 15; :: thesis: verum