let I be halt-free 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))),((Initialize s) +* (stop I)),k))),(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_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))),((Initialize s) +* (stop I)),k))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),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))),((Initialize s) +* (stop I)),k))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) <> halt SCMPDS )
set ss = (Initialize s) +* (stop I);
set s2 = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k);
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by COMPOS_1:125;
assume ( I is_closed_on s & I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ) ; :: thesis: CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) <> halt SCMPDS
then A1: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom I by Th40;
Y: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) by COMPOS_1:38;
( Initialize (stop I) c= (Initialize s) +* (stop I) & I c= Initialize (stop I) ) by Th17, I1, FUNCT_4:26;
then I c= (Initialize s) +* (stop I) by XBOOLE_1:1;
then I c= Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) by AMI_1:81;
then CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = I . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) by A1, Y, GRFUNC_1:8;
hence CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) <> halt SCMPDS by A1, SCMPDS_5:def 3; :: thesis: verum