let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds card (Times a,I) = (card I) + 12
let I be Program of SCM+FSA ; :: thesis: card (Times a,I) = (card I) + 12
set g1 = Goto (insloc 2);
set SF = SubFrom a,(intloc 0 );
set if0 = if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )));
thus card (Times a,I) = ((card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) + 1) + 4 by SCMFSA8A:17, SCMFSA8B:15
.= (card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) + (1 + 4)
.= (card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) + 5 by SCMFSA8A:33
.= (((card (I ';' (SubFrom a,(intloc 0 )))) + (card (Goto (insloc 2)))) + 4) + 5 by SCMFSA8B:14
.= (((card (I ';' (SubFrom a,(intloc 0 )))) + 1) + 4) + 5 by SCMFSA8A:29
.= ((((card I) + (card (Macro (SubFrom a,(intloc 0 ))))) + 1) + 4) + 5 by SCMFSA6A:61
.= ((((card I) + 2) + 1) + 4) + 5 by SCMFSA7B:6
.= (card I) + 12 ; :: thesis: verum