let I be MacroInstruction of SCM+FSA ; :: thesis: for a being Int-Location holds card (if=0 (a,I)) = (card I) + 4
let a be Int-Location; :: thesis: card (if=0 (a,I)) = (card I) + 4
thus card (if=0 (a,I)) = (card (((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I)) + 1 by Lm1, SCMFSA6A:21
.= ((card ((a =0_goto 3) ";" (Goto ((card I) + 1)))) + (card I)) + 1 by SCMFSA6A:21
.= ((2 + (card (Goto ((card I) + 1)))) + (card I)) + 1 by SCMFSA6A:33
.= ((2 + 1) + (card I)) + 1 by SCMFSA8A:15
.= (card I) + 4 ; :: thesis: verum