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-up 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-up a,i,n,I) = (card I) + 3
let n be Element of NAT ; :: thesis: for I being Program of SCMPDS holds card (for-up a,i,n,I) = (card I) + 3
let I be Program of SCMPDS ; :: thesis: card (for-up 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-up a,i,n,I) = ((card I) + 2) + 1 by SCMP_GCD:8
.= (card I) + 3 ;
:: thesis: verum