let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedInt*Loc (Times a,I) = UsedInt*Loc I
let I be Program of SCM+FSA ; :: thesis: UsedInt*Loc (Times a,I) = UsedInt*Loc I
set g1 = Goto 2;
set SF = SubFrom a,(intloc 0 );
set if0 = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )));
thus UsedInt*Loc (Times a,I) = (UsedInt*Loc (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) \/ {} by SCMFSA9A:10, SCMFSA9A:16
.= UsedInt*Loc (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by Th36
.= (UsedInt*Loc (Goto 2)) \/ (UsedInt*Loc (I ';' (SubFrom a,(intloc 0 )))) by SCMFSA9A:14
.= {} \/ (UsedInt*Loc (I ';' (SubFrom a,(intloc 0 )))) by SCMFSA9A:12
.= (UsedInt*Loc I) \/ (UsedInt*Loc (SubFrom a,(intloc 0 ))) by SF_MASTR:50
.= (UsedInt*Loc I) \/ {} by SF_MASTR:36
.= UsedInt*Loc I ; :: thesis: verum