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, AMI_1:def 46; :: thesis: verum