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
; if<>0 (a,k1,I) is parahalting
let s be 0 -started State of SCMPDS; SCMPDS_4:def 7 for b1 being set holds
( not stop (if<>0 (a,k1,I)) c= b1 or b1 halts_on s )
let P be Instruction-Sequence of SCMPDS; ( not stop (if<>0 (a,k1,I)) c= P or P halts_on s )
A1:
Initialize s = s
by MEMSTR_0:44;
assume
stop (if<>0 (a,k1,I)) c= P
; P halts_on s
then A2:
P = P +* (stop (if<>0 (a,k1,I)))
by FUNCT_4:98;
A3:
( I is_closed_on s,P & I is_halting_on s,P )
by Th11, Th12;