let I be No-StopCode 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 (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (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 (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) <> halt SCMPDS
let k be Element of NAT ; :: thesis: ( I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) implies CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) <> halt SCMPDS )
set IsI = Initialized (stop I);
set ss = s +* (Initialized (stop I));
set s2 = Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k;
assume ( I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) ) ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) <> halt SCMPDS
then A1: IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) in dom I by Th40;
Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) /. (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) . (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) by AMI_1:150;
( Initialized (stop I) c= s +* (Initialized (stop I)) & I c= Initialized (stop I) ) by Th17, FUNCT_4:26;
then I c= s +* (Initialized (stop I)) by XBOOLE_1:1;
then I c= Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k by AMI_1:81;
then CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) = I . (IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)) by A1, GRFUNC_1:8, Y;
hence CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) <> halt SCMPDS by A1, SCMPDS_5:def 3; :: thesis: verum