let I be Program of SCM+FSA ; :: thesis: for a being Int-Location holds card (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) = (card I) + 11
let a be Int-Location ; :: thesis: card (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) = (card I) + 11
thus card (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) = (1 + (card (if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 )))))) + 4 by SCMFSA8A:17, SCMFSA8B:14
.= ((((card (I ';' (Goto (insloc 0 )))) + 1) + 4) + 1) + 4 by SCMFSA8A:17, SCMFSA8B:15
.= (((((card I) + (card (Goto (insloc 0 )))) + 1) + 4) + 1) + 4 by SCMFSA6A:61
.= (((((card I) + 1) + 1) + 4) + 1) + 4 by SCMFSA8A:29
.= (card I) + 11 ; :: thesis: verum