let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I being MacroInstruction of S holds I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))
let I be MacroInstruction of S; :: thesis: I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))
E: LastLoc I in dom I by VALUED_1:30;
D: {(LastLoc I)} misses dom (CutLastLoc I) by Th17, ZFMISC_1:50;
A: dom ((LastLoc I) .--> (I . (LastLoc I))) = {(LastLoc I)} by FUNCOP_1:13;
I = (CutLastLoc I) \/ ((LastLoc I) .--> (I . (LastLoc I))) by E, FUNCOP_1:84, XBOOLE_1:45
.= (CutLastLoc I) +* ((LastLoc I) .--> (I . (LastLoc I))) by A, D, FUNCT_4:31 ;
hence I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S)) by COMPOS_1:def 14; :: thesis: verum