let a be Int-Location ; :: thesis: for I being Program of holds card (Times (a,I)) = (card I) + 12
let I be Program of ; :: thesis: card (Times (a,I)) = (card I) + 12
set g1 = Goto 2;
set SF = SubFrom (a,(intloc 0));
set if0 = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
card (Stop SCM+FSA) = 1 by COMPOS_1:4;
hence card (Times (a,I)) = ((card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) + 1) + 4 by SCMFSA8B:12
.= (card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) + (1 + 4)
.= (card (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) + 5 by SCMFSA8A:19
.= (((card (I ';' (SubFrom (a,(intloc 0))))) + (card (Goto 2))) + 4) + 5 by SCMFSA8B:11
.= (((card (I ';' (SubFrom (a,(intloc 0))))) + 1) + 4) + 5 by SCMFSA8A:15
.= ((((card I) + 2) + 1) + 4) + 5 by SCMFSA6A:34
.= (card I) + 12 ;
:: thesis: verum