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 COMPOS_1:55
.= ((card I) + 2) + 1 by Th4
.= (card I) + 3 ; :: thesis: verum