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