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

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