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) + 2
let i be Integer; :: thesis: for I being Program of SCMPDS holds card (while>0 a,i,I) = (card I) + 2
let I be Program of SCMPDS ; :: thesis: card (while>0 a,i,I) = (card I) + 2
set i1 = a,i <=0_goto ((card I) + 2);
set I4 = (a,i <=0_goto ((card I) + 2)) ';' I;
thus card (while>0 a,i,I) = (card ((a,i <=0_goto ((card I) + 2)) ';' I)) + 1 by SCMP_GCD:8
.= ((card I) + 1) + 1 by SCMPDS_6:15
.= (card I) + 2 ; :: thesis: verum