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