let P be Instruction-Sequence of SCMPDS; :: thesis: for I being halt-free Program of SCMPDS
for s being State of SCMPDS
for k being Element of 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 SCMPDS; :: thesis: for s being State of SCMPDS
for k being Element of 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 Element of 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 Element of 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 A2: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I by Th40;
A3: (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;
XX: 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 XX, 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 A2, A3, GRFUNC_1:2;
hence CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS by A2, COMPOS_1:def 25; :: thesis: verum