let a be Int_position ; :: thesis: for i being Integer
for n being Element of NAT
for I being Program of SCMPDS holds
( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
let i be Integer; :: thesis: for n being Element of NAT
for I being Program of SCMPDS holds
( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
let n be Element of NAT ; :: thesis: for I being Program of SCMPDS holds
( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
let I be Program of SCMPDS; :: thesis: ( (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) & (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
set i1 = (a,i) <=0_goto ((card I) + 3);
set i2 = AddTo (a,i,(- n));
set i3 = goto (- ((card I) + 2));
set I4 = ((a,i) <=0_goto ((card I) + 3)) ';' I;
set I5 = (((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)));
set J6 = (AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2)));
set J5 = I ';' ((AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2))));
set FLOOP = for-down (a,i,n,I);
for-down (a,i,n,I) = (((a,i) <=0_goto ((card I) + 3)) ';' I) ';' ((AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2)))) by SCMPDS_4:49;
then for-down (a,i,n,I) = ((a,i) <=0_goto ((card I) + 3)) ';' (I ';' ((AddTo (a,i,(- n))) ';' (goto (- ((card I) + 2))))) by SCMPDS_4:50;
hence (for-down (a,i,n,I)) . 0 = (a,i) <=0_goto ((card I) + 3) by SCMPDS_6:16; :: thesis: ( (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) & (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) )
A1: card (((a,i) <=0_goto ((card I) + 3)) ';' I) = (card I) + 1 by SCMPDS_6:15;
hence (for-down (a,i,n,I)) . ((card I) + 1) = AddTo (a,i,(- n)) by SCMP_GCD:11; :: thesis: (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2))
card ((((a,i) <=0_goto ((card I) + 3)) ';' I) ';' (AddTo (a,i,(- n)))) = ((card I) + 1) + 1 by A1, SCMP_GCD:8
.= (card I) + (1 + 1) ;
hence (for-down (a,i,n,I)) . ((card I) + 2) = goto (- ((card I) + 2)) by SCMP_GCD:10; :: thesis: verum