let a be Int-Location ; :: thesis: for I being Program of {INT,(INT *)} holds card (Times (a,I)) = (card I) + 12
let I be Program of {INT,(INT *)}; :: 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:46;
hence card (Times (a,I)) = ((card (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) + 1) + 4 by SCMFSA8B:15
.= (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:33
.= (((card (I ';' (SubFrom (a,(intloc 0))))) + (card (Goto 2))) + 4) + 5 by SCMFSA8B:14
.= (((card (I ';' (SubFrom (a,(intloc 0))))) + 1) + 4) + 5 by SCMFSA8A:29
.= ((((card I) + 2) + 1) + 4) + 5 by SCMFSA6A:76
.= (card I) + 12 ;
:: thesis: verum