let a be Int_position; for i being Integer
for I being Program of SCMPDS holds card (while<>0 (a,i,I)) = (card I) + 3
let i be Integer; for I being Program of SCMPDS holds card (while<>0 (a,i,I)) = (card I) + 3
let I be Program of SCMPDS; card (while<>0 (a,i,I)) = (card I) + 3
set i1 = (a,i) <>0_goto 2;
set i2 = goto ((card I) + 2);
set I4 = (((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I;
thus card (while<>0 (a,i,I)) =
(card ((((a,i) <>0_goto 2) ';' (goto ((card I) + 2))) ';' I)) + 1
by SCMP_GCD:4
.=
((card (((a,i) <>0_goto 2) ';' (goto ((card I) + 2)))) + (card I)) + 1
by AFINSQ_1:17
.=
(2 + (card I)) + 1
by SCMP_GCD:5
.=
(card I) + 3
; verum