let a be Int_position ; :: thesis: for i being Integer
for I being Program of SCMPDS holds
( (while<0 a,i,I) . (inspos 0 ) = a,i >=0_goto ((card I) + 2) & (while<0 a,i,I) . (inspos ((card I) + 1)) = goto (- ((card I) + 1)) )
let i be Integer; :: thesis: for I being Program of SCMPDS holds
( (while<0 a,i,I) . (inspos 0 ) = a,i >=0_goto ((card I) + 2) & (while<0 a,i,I) . (inspos ((card I) + 1)) = goto (- ((card I) + 1)) )
let I be Program of SCMPDS ; :: thesis: ( (while<0 a,i,I) . (inspos 0 ) = a,i >=0_goto ((card I) + 2) & (while<0 a,i,I) . (inspos ((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;
A1: card ((a,i >=0_goto ((card I) + 2)) ';' I) = (card I) + 1 by SCMPDS_6:15;
set J5 = I ';' (goto (- ((card I) + 1)));
set FLOOP = 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) . (inspos 0 ) = a,i >=0_goto ((card I) + 2) by SCMPDS_6:16; :: thesis: (while<0 a,i,I) . (inspos ((card I) + 1)) = goto (- ((card I) + 1))
thus (while<0 a,i,I) . (inspos ((card I) + 1)) = goto (- ((card I) + 1)) by A1, SCMP_GCD:10; :: thesis: verum