set i = (a,k1) >=0_goto 2;
set j = 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 10 :: thesis: ( not stop (if>=0 (a,k1,I)) c= s or ProgramPart s halts_on s )
AA: Initialize s = s by COMPOS_1:78;
assume stop (if>=0 (a,k1,I)) c= s ; :: thesis: ProgramPart s halts_on s
then A1: s = (Initialize s) +* (stop (if>=0 (a,k1,I))) by AA, FUNCT_4:79;
A2: ( I is_closed_on s & I is_halting_on s ) by Th34, Th35;

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

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

then if>=0 (a,k1,I) is_halting_on s by A2, Th132;
hence ProgramPart s halts_on s by A1, Def3; :: thesis: verum

end;

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

then if>=0 (a,k1,I) is_halting_on s by Th133;
hence ProgramPart s halts_on s by A1, Def3; :: thesis: verum

end;

end;