let a be Int_position ; :: thesis: for i being Integer
for I being Program of SCMPDS holds card (while<>0 a,i,I) = (card I) + 3
let i be Integer; :: thesis: for I being Program of SCMPDS holds card (while<>0 a,i,I) = (card I) + 3
let I be Program of SCMPDS ; :: thesis: 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:8
.= ((card ((a,i <>0_goto 2) ';' (goto ((card I) + 2)))) + (card I)) + 1 by SCMPDS_4:45
.= (2 + (card I)) + 1 by SCMP_GCD:9
.= (card I) + 3 ; :: thesis: verum