set IF = if<0 a,k1,I,J;
set IsIF = Initialized (stop (if<0 a,k1,I,J));
set i = a,k1 >=0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
reconsider IJ = (I ';' (Goto ((card J) + 1))) ';' J as shiftable Program of SCMPDS ;
if<0 a,k1,I,J = ((a,k1 >=0_goto ((card I) + 2)) ';' (I ';' (Goto ((card J) + 1)))) ';' J by SCMPDS_4:50
.= (a,k1 >=0_goto ((card I) + 2)) ';' IJ by SCMPDS_4:50
.= (Load (a,k1 >=0_goto ((card I) + 2))) ';' IJ by SCMPDS_4:def 4 ;
hence if<0 a,k1,I,J is shiftable ; :: thesis: if<0 a,k1,I,J is parahalting

now

let s be State of SCMPDS ; :: thesis: ( Initialized (stop (if<0 a,k1,I,J)) c= s implies b₁ is halting )
assume Initialized (stop (if<0 a,k1,I,J)) c= s ; :: thesis: b₁ is halting
then A1: s = s +* (Initialized (stop (if<0 a,k1,I,J))) by FUNCT_4:79;
A2: ( I is_closed_on s & I is_halting_on s ) by Th34, Th35;
A3: ( J is_closed_on s & J 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,J is_halting_on s by A2, Th112;
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,J is_halting_on s by A3, Th113;
hence s is halting by A1, Def3; :: thesis: verum

end;

end;

end;

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