let I be Program of ; :: thesis: for a being Int-Location holds card (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 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 0)))))) = (card I) + 11
thus card (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) = (1 + (card (if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) + 4 by Lm1, SCMFSA8B:11
.= ((((card (I ';' (Goto 0))) + 1) + 4) + 1) + 4 by Lm1, SCMFSA8B:12
.= (((((card I) + (card (Goto 0))) + 1) + 4) + 1) + 4 by SCMFSA6A:21
.= (((((card I) + 1) + 1) + 4) + 1) + 4 by SCMFSA8A:15
.= (card I) + 11 ; :: thesis: verum