let I be MacroInstruction of SCM+FSA ; :: thesis: for a being Int-Location holds card (while>0 (a,I)) = (card I) + 5
let a be Int-Location; :: thesis: card (while>0 (a,I)) = (card I) + 5
thus card (while>0 (a,I)) = card (if>0 (a,(I ';' (goto 0)))) by FUNCT_7:30
.= (card (I ';' (goto 0))) + 4 by Th2
.= ((card I) + 1) + 4 by COMPOS_2:11
.= (card I) + 5 ; :: thesis: verum