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

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