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) . (inspos 0 ) = a,i <=0_goto ((card I) + 3) & (for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,(- n) & (for-down a,i,n,I) . (inspos ((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) . (inspos 0 ) = a,i <=0_goto ((card I) + 3) & (for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,(- n) & (for-down a,i,n,I) . (inspos ((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) . (inspos 0 ) = a,i <=0_goto ((card I) + 3) & (for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,(- n) & (for-down a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) )
let I be Program of SCMPDS ; :: thesis: ( (for-down a,i,n,I) . (inspos 0 ) = a,i <=0_goto ((card I) + 3) & (for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,(- n) & (for-down a,i,n,I) . (inspos ((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));
A1: card ((a,i <=0_goto ((card I) + 3)) ';' I) = (card I) + 1 by SCMPDS_6:15;
then A2: card (((a,i <=0_goto ((card I) + 3)) ';' I) ';' (AddTo a,i,(- n))) = ((card I) + 1) + 1 by SCMP_GCD:8
.= (card I) + (1 + 1) ;
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) . (inspos 0 ) = a,i <=0_goto ((card I) + 3) by SCMPDS_6:16; :: thesis: ( (for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,(- n) & (for-down a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) )
thus (for-down a,i,n,I) . (inspos ((card I) + 1)) = AddTo a,i,(- n) by A1, SCMP_GCD:11; :: thesis: (for-down a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2))
thus (for-down a,i,n,I) . (inspos ((card I) + 2)) = goto (- ((card I) + 2)) by A2, SCMP_GCD:10; :: thesis: verum