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

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