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 Th1

.= ((card I) + 1) + 4 by COMPOS_2:11

.= (card I) + 5 ; :: thesis: verum

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 Th1

.= ((card I) + 1) + 4 by COMPOS_2:11

.= (card I) + 5 ; :: thesis: verum