let I be MacroInstruction of SCM+FSA ; :: thesis: for k being Nat holds UsedILoc (I ';' (goto k)) = UsedILoc I
let k be Nat; :: thesis: UsedILoc (I ';' (goto k)) = UsedILoc 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 UsedILoc (I ';' (goto k)) = UsedILoc (I ';' (Macro (goto k)))
.= UsedILoc ((CutLastLoc I) +* (Reloc ((Macro (goto k)),((card I) -' 1))))
.= (UsedILoc (CutLastLoc I)) \/ (UsedILoc (Reloc ((Macro (goto k)),((card I) -' 1)))) by A3, Th21
.= (UsedILoc (CutLastLoc I)) \/ (UsedILoc (Macro (goto k))) by Th25
.= (UsedILoc (CutLastLoc I)) \/ (UsedIntLoc (goto k)) by Th28
.= (UsedILoc (CutLastLoc I)) \/ {} by Th15
.= (UsedILoc (CutLastLoc I)) \/ (UsedIntLoc (halt SCM+FSA)) by Th13
.= (UsedILoc (CutLastLoc I)) \/ (UsedILoc ((LastLoc I) .--> (halt SCM+FSA))) by Lm7
.= UsedILoc ((CutLastLoc I) +* ((LastLoc I) .--> (halt SCM+FSA))) by A2, Th21
.= UsedILoc I by COMPOS_2:20 ; :: thesis: verum