let I, J be Program 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
thus card (if=0 a,I,J) = card (((((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by SCMFSA6A:def 6
.= (card ((((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) + 1 by SCMFSA6A:61, SCMFSA8A:17
.= ((card (((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1))))) + (card I)) + 1 by SCMFSA6A:61
.= (((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))) + (card I)) + 1 by SCMFSA6A:61
.= (((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1) + (card I)) + 1 by SCMFSA8A:29
.= ((((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1) + (card I)) + 1 by SCMFSA6A:61
.= (((2 + (card J)) + 1) + (card I)) + 1 by SCMFSA7B:6
.= ((card I) + (card J)) + 4 ; :: thesis: verum