let l be Instruction-Location of SCM+FSA ; :: thesis: UsedInt*Loc (Goto l) = {}
Goto l = (insloc 0 ) .--> (goto l) by SCMFSA8A:def 2;
hence UsedInt*Loc (Goto l) = UsedInt*Loc (goto l) by Th8
.= {} by SF_MASTR:36 ;
:: thesis: verum