set IF = if<=0 a,k1,I;
set IsIF = Initialized (stop (if<=0 a,k1,I));
set i = a,k1 <=0_goto 2;
set j = goto ((card I) + 1);
if<=0 a,k1,I = ((Load (a,k1 <=0_goto 2)) ';' (Load (goto ((card I) + 1)))) ';' I by SCMPDS_4:def 6;
hence if<=0 a,k1,I is shiftable ; :: thesis: if<=0 a,k1,I is parahalting

now

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

then if<=0 a,k1,I is_halting_on s by A2, Th102;
hence s is halting by A1, Def3; :: thesis: verum

end;

suppose s . (DataLoc (s . a),k1) > 0 ; :: thesis: b₁ is halting

then if<=0 a,k1,I is_halting_on s by Th103;
hence s is halting by A1, Def3; :: thesis: verum

end;

end;

end;

then Initialized (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