let s be State of SCMPDS ; :: thesis: for I being halt-free parahalting Program of SCMPDS
for k being Element of NAT st Initialize I c= s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCMPDS
let I be halt-free parahalting Program of SCMPDS ; :: thesis: for k being Element of NAT st Initialize I c= s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCMPDS
let k be Element of NAT ; :: thesis: ( Initialize I c= s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) implies CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCMPDS )
set sI = (Initialize s) +* (stop I);
set s1 = Comput (ProgramPart s),s,k;
set s2 = Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k;
assume that
A1: Initialize I c= s and
A2: k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCMPDS
A3: I c= Comput (ProgramPart s),s,k by A1, AMI_1:81, SCMPDS_4:57;
A4: IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) in dom I by A2, Th28;
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by COMPOS_1:38;
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by A1, A2, Th29, Y, COMPOS_1:24
.= I . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) by A3, A4, GRFUNC_1:8 ;
hence CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCMPDS by A4, Def3; :: thesis: verum