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