let a be Int_position ; :: thesis: for i being Integer
for I being Program of SCMPDS holds card (stop (while>0 a,i,I)) = (card I) + 3
let i be Integer; :: thesis: for I being Program of SCMPDS holds card (stop (while>0 a,i,I)) = (card I) + 3
let I be Program of SCMPDS ; :: thesis: card (stop (while>0 a,i,I)) = (card I) + 3
thus card (stop (while>0 a,i,I)) = (card (while>0 a,i,I)) + 1 by SCMPDS_5:7
.= ((card I) + 2) + 1 by Th17
.= (card I) + 3 ; :: thesis: verum