let a be Int_position; :: thesis: 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)) )
let i be Integer; :: thesis: 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)) )
let I be Program of SCMPDS; :: thesis: ( (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)) )
set i1 = (a,i) <>0_goto 2;
set i2 = goto ((card I) + 2);
set i3 = goto (- ((card I) + 2));
set I4 = (((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I;
set WHL = while<>0 (a,i,I);
A1: while<>0 (a,i,I) = (((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' (I ';' (goto (- ((card I) + 2)))) by SCMPDS_4:11;
hence (while<>0 (a,i,I)) . 0 = (a,i) <>0_goto 2 by Th1; :: thesis: ( (while<>0 (a,i,I)) . 1 = goto ((card I) + 2) & (while<>0 (a,i,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
thus (while<>0 (a,i,I)) . 1 = goto ((card I) + 2) by A1, Th1; :: thesis: (while<>0 (a,i,I)) . ((card I) + 2) = goto (- ((card I) + 2))
card ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) = (card (((a,i) <>0_goto 2) ';' (goto ((card I) + 2)))) + (card I) by AFINSQ_1:17
.= (card I) + 2 by SCMP_GCD:5 ;
hence (while<>0 (a,i,I)) . ((card I) + 2) = goto (- ((card I) + 2)) by SCMP_GCD:6; :: thesis: verum