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