set i = (a,k1) <>0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
set IF = if=0 (a,k1,I,J);
reconsider IJ = (I ';' (Goto ((card J) + 1))) ';' J as shiftable Program of ;
thus if=0 (a,k1,I,J) is shiftable ; :: thesis: if=0 (a,k1,I,J) is parahalting
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 7 :: thesis: for b1 being set holds
( not stop (if=0 (a,k1,I,J)) c= b1 or b1 halts_on s )
let P be Instruction-Sequence of SCMPDS; :: thesis: ( not stop (if=0 (a,k1,I,J)) c= P or P halts_on s )
A1: Initialize s = s by MEMSTR_0:44;
assume stop (if=0 (a,k1,I,J)) c= P ; :: thesis: P halts_on s
then A2: P = P +* (stop (if=0 (a,k1,I,J))) by FUNCT_4:98;
A3: ( J is_closed_on s,P & J is_halting_on s,P ) by Th11, Th12;
A4: ( 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,J) is_halting_on s,P by A4, Th29;
hence P halts_on s by A1, A2; :: thesis: verum
end;
suppose s . (DataLoc ((s . a),k1)) <> 0 ; :: thesis: P halts_on s
then if=0 (a,k1,I,J) is_halting_on s,P by A3, Th30;
hence P halts_on s by A1, A2; :: thesis: verum
end;
end;