let a be Int-Location ; :: thesis: for I being Program of holds UsedInt*Loc (Times (a,I)) = UsedInt*Loc I
let I be Program of ; :: 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:4, SCMFSA9A:10
.= 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:8
.= {} \/ (UsedInt*Loc (I ';' (SubFrom (a,(intloc 0))))) by SCMFSA9A:6
.= (UsedInt*Loc I) \/ (UsedInt*Loc (SubFrom (a,(intloc 0)))) by SF_MASTR:46
.= (UsedInt*Loc I) \/ {} by SF_MASTR:32
.= UsedInt*Loc I ; :: thesis: verum