let I be MacroInstruction of SCM+FSA ; :: thesis: for k being Nat holds UsedI*Loc (I ';' (goto k)) = UsedI*Loc I
let k be Nat; :: thesis: UsedI*Loc (I ';' (goto k)) = UsedI*Loc I
not LastLoc I in dom (CutLastLoc I) by COMPOS_2:17;
then {(LastLoc I)} misses dom (CutLastLoc I) by ZFMISC_1:50;
then A2: dom (CutLastLoc I) misses dom ((LastLoc I) .--> (halt SCM+FSA)) ;
A3: dom (CutLastLoc I) misses dom (Reloc ((Macro (goto k)),((card I) -' 1))) by COMPOS_1:18;
thus UsedI*Loc (I ';' (goto k)) = UsedI*Loc (I ';' (Macro (goto k)))
.= UsedI*Loc ((CutLastLoc I) +* (Reloc ((Macro (goto k)),((card I) -' 1))))
.= (UsedI*Loc (CutLastLoc I)) \/ (UsedI*Loc (Reloc ((Macro (goto k)),((card I) -' 1)))) by A3, Th37
.= (UsedI*Loc (CutLastLoc I)) \/ (UsedI*Loc (Macro (goto k))) by Th41
.= (UsedI*Loc (CutLastLoc I)) \/ (UsedInt*Loc (goto k)) by Th44
.= (UsedI*Loc (CutLastLoc I)) \/ {} by Th32
.= (UsedI*Loc (CutLastLoc I)) \/ (UsedInt*Loc (halt SCM+FSA)) by Th32
.= (UsedI*Loc (CutLastLoc I)) \/ (UsedI*Loc ((LastLoc I) .--> (halt SCM+FSA))) by Lm8
.= UsedI*Loc ((CutLastLoc I) +* ((LastLoc I) .--> (halt SCM+FSA))) by A2, Th37
.= UsedI*Loc I by COMPOS_2:20 ; :: thesis: verum