let a be Int_position ; :: thesis: for i being Integer
for n being Element of NAT
for I being Program of SCMPDS holds card (for-down a,i,n,I) = (card I) + 3
let i be Integer; :: thesis: for n being Element of NAT
for I being Program of SCMPDS holds card (for-down a,i,n,I) = (card I) + 3
let n be Element of NAT ; :: thesis: for I being Program of SCMPDS holds card (for-down a,i,n,I) = (card I) + 3
let I be Program of SCMPDS ; :: thesis: card (for-down a,i,n,I) = (card I) + 3
set i1 = a,i <=0_goto ((card I) + 3);
set i2 = AddTo a,i,(- n);
set I4 = (a,i <=0_goto ((card I) + 3)) ';' I;
set I5 = ((a,i <=0_goto ((card I) + 3)) ';' I) ';' (AddTo a,i,(- n));
card ((a,i <=0_goto ((card I) + 3)) ';' I) = (card I) + 1 by SCMPDS_6:15;
then 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) ;
hence card (for-down a,i,n,I) = ((card I) + 2) + 1 by SCMP_GCD:8
.= (card I) + 3 ;
:: thesis: verum