- ((card I) + 2) <> 0 ;
then reconsider i3 = goto (- ((card I) + 2)) as No-StopCode Instruction of SCMPDS by SCMPDS_5:25;
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 No-StopCode ; :: thesis: verum