theorem Th11: :: SCPINVAR:11

for a being Int_position
for i being Integer
for I being Program of SCMPDS holds
( (while<>0 (a,i,I)) . 0 = (a,i) <>0_goto 2 & (while<>0 (a,i,I)) . 1 = goto ((card I) + 2) & (while<>0 (a,i,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )