let b be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedInt*Loc (while=0 b,I) = UsedInt*Loc I
let I be Program of SCM+FSA ; :: thesis: UsedInt*Loc (while=0 b,I) = UsedInt*Loc I
set a = b;
set J = Stop SCM+FSA ;
set IG = I ';' (Goto (insloc 0 ));
while=0 b,I = (if=0 b,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by SCMFSA_9:def 1;
hence UsedInt*Loc (while=0 b,I) = UsedInt*Loc (if=0 b,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by Lm3
.= (UsedInt*Loc (I ';' (Goto (insloc 0 )))) \/ (UsedInt*Loc (Stop SCM+FSA )) by Th14
.= ((UsedInt*Loc I) \/ (UsedInt*Loc (Goto (insloc 0 )))) \/ (UsedInt*Loc (Stop SCM+FSA )) by SF_MASTR:47
.= (UsedInt*Loc I) \/ {} by Th10, Th12
.= UsedInt*Loc I ;
:: thesis: verum