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