let a be Int_position; for i being Integer
for I being Program of SCMPDS holds card (stop (while<>0 (a,i,I))) = (card I) + 4
let i be Integer; for I being Program of SCMPDS holds card (stop (while<>0 (a,i,I))) = (card I) + 4
let I be Program of SCMPDS; card (stop (while<>0 (a,i,I))) = (card I) + 4
thus card (stop (while<>0 (a,i,I))) =
(card (while<>0 (a,i,I))) + 1
by COMPOS_1:55
.=
((card I) + 3) + 1
by Th8
.=
(card I) + 4
; verum