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