let I be Program of SCMPDS; :: thesis: for s being State of SCMPDS
for k being Element of NAT st I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) <> halt SCMPDS
let s be State of SCMPDS; :: thesis: for k being Element of NAT st I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) <> halt SCMPDS
let k be Element of NAT ; :: thesis: ( I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) implies CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) <> halt SCMPDS )
set ss = (Initialize s) +* (stop I);
set m = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
assume that
A1: I is_halting_on s and
A2: k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) <> halt SCMPDS
assume A3: CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = halt SCMPDS ; :: thesis: contradiction
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A1, SCMPDS_6:def 3;
hence contradiction by A2, A3, EXTPRO_1:def 14; :: thesis: verum