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