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

now

let s be State of SCMPDS ; :: thesis: ( Initialize (stop (if>0 a,k1,I)) c= s implies ProgramPart b₁ halts_on b₁ )
I2: s +* (Initialize (stop (if>0 a,k1,I))) = (Initialize s) +* (stop (if>0 a,k1,I)) by SCMPDS_4:5;
assume Initialize (stop (if>0 a,k1,I)) c= s ; :: thesis: ProgramPart b₁ halts_on b₁
then A1: s = (Initialize s) +* (stop (if>0 a,k1,I)) by I2, 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 b₁ halts_on b₁

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

end;

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

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

end;

end;

end;

then Initialize (stop (if>0 a,k1,I)) is halting by AMI_1:def 26;
hence if>0 a,k1,I is parahalting by SCMPDS_4:def 10; :: thesis: verum