set i = (a,k1) >=0_goto ((card I) + 1);
set IF = if<0 (a,k1,I);
set pIF = stop (if<0 (a,k1,I));
thus if<0 (a,k1,I) is shiftable ; :: thesis: if<0 (a,k1,I) is parahalting
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 7 :: thesis: for b₁ being set holds
( not stop (if<0 (a,k1,I)) c= b₁ or b₁ halts_on s )
let P be Instruction-Sequence of SCMPDS; :: thesis: ( not stop (if<0 (a,k1,I)) c= P or P halts_on s )
A1: Initialize s = s by MEMSTR_0:44;
assume stop (if<0 (a,k1,I)) c= P ; :: thesis: P halts_on s
then A2: P = P +* (stop (if<0 (a,k1,I))) by FUNCT_4:98;
A3: ( I is_closed_on s,P & I is_halting_on s,P ) by Th11, Th12;

per cases ( s . (DataLoc ((s . a),k1)) < 0 or s . (DataLoc ((s . a),k1)) >= 0 ) ;

suppose s . (DataLoc ((s . a),k1)) < 0 ; :: thesis: P halts_on s

then if<0 (a,k1,I) is_halting_on s,P by A3, Th99;
hence P halts_on s by A2, A1; :: thesis: verum

end;

suppose s . (DataLoc ((s . a),k1)) >= 0 ; :: thesis: P halts_on s

then if<0 (a,k1,I) is_halting_on s,P by Th100;
hence P halts_on s by A2, A1; :: thesis: verum

end;

end;