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