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:51;
hence (while>0 a,i,I) . 0 = a,i <=0_goto ((card I) + 2) by SCMPDS_6:16; :: 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:15;
hence (while>0 a,i,I) . ((card I) + 1) = goto (- ((card I) + 1)) by SCMP_GCD:10; :: thesis: verum