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 ((card I) + 2) & (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )
let i be Integer; :: thesis: for I being Program of SCMPDS holds
( (while>0 (a,i,I)) . 0 = (a,i) <=0_goto ((card I) + 2) & (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )
let I be Program of SCMPDS; :: thesis: ( (while>0 (a,i,I)) . 0 = (a,i) <=0_goto ((card I) + 2) & (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
set I4 = ((a,i) <=0_goto ((card I) + 2)) ';' I;
set J5 = I ';' (goto (- ((card I) + 1)));
set WHL = while>0 (a,i,I);
while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:15;
hence (while>0 (a,i,I)) . 0 = (a,i) <=0_goto ((card I) + 2) by SCMPDS_6:7; :: thesis: (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1))
card (((a,i) <=0_goto ((card I) + 2)) ';' I) = (card I) + 1 by SCMPDS_6:6;
hence (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) by SCMP_GCD:6; :: thesis: verum