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:4
.= ((card I) + 1) + 1 by SCMPDS_6:6
.= (card I) + 2 ; :: thesis: verum