let P be Instruction-Sequence of SCMPDS; :: thesis: for I being halt-free Program of
for s being State of SCMPDS
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
let I be halt-free Program of ; :: thesis: for s being State of SCMPDS
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
let s be State of SCMPDS; :: thesis: for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
let k be Nat; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) implies CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS )
set ss = Initialize s;
set PP = P +* (stop I);
set s2 = Comput ((P +* (stop I)),(Initialize s),k);
set P2 = P +* (stop I);
assume ( I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) ) ; :: thesis: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
then A1: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I by Th17;
A2: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),(Initialize s),k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by PBOOLE:143;
A3: stop I c= P +* (stop I) by FUNCT_4:25;
I c= stop I by AFINSQ_1:74;
then I c= P +* (stop I) by A3, XBOOLE_1:1;
then CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = I . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A1, A2, GRFUNC_1:2;
hence CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS by A1, COMPOS_1:def 27; :: thesis: verum