reconsider i2 = goto ((card I) + 2) as No-StopCode Instruction of SCMPDS by SCMPDS_5:21;
reconsider i3 = goto (- ((card I) + 2)) as No-StopCode Instruction of SCMPDS by SCMPDS_5:21;
while<>0 (a,i,I) = ((((a,i) <>0_goto 2) ';' i2) ';' I) ';' i3 ;
hence while<>0 (a,i,I) is halt-free ; :: thesis: verum