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