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 SCMPDS_4:5;
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