:: deftheorem defines while<>0 SCPINVAR:def 3 :
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds while<>0 (a,i,I) = ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) ';' (goto (- ((card I) + 2)));