let a be Int-Location ; :: thesis: for I being Program of {INT,(INT *)} holds UsedInt*Loc (Times (a,I)) = UsedInt*Loc I
let I be Program of {INT,(INT *)}; :: 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