let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for F being pre-Macro of S holds F ';' (Stop S) = F
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N; :: thesis: for F being pre-Macro of S holds F ';' (Stop S) = F
let F be pre-Macro of S; :: thesis: F ';' (Stop S) = F
set k = (card F) -' 1;
A1: F ';' (Stop S) = (CutLastLoc F) +* (Shift ((Stop S),((card F) -' 1))) by Th57;
A2: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by VALUED_1:38;
dom (Shift ((Stop S),((card F) -' 1))) = dom (((card F) -' 1) .--> (halt S)) by Th108
.= {((card F) -' 1)} by FUNCOP_1:19
.= {(LastLoc F)} by AFINSQ_1:74 ;
then A3: dom (F ';' (Stop S)) = dom F by A1, A2, FUNCT_4:def 1;
for x being set st x in dom F holds
(F ';' (Stop S)) . x = F . x

proof

let x be set ; :: thesis: ( x in dom F implies (F ';' (Stop S)) . x = F . x )
assume A4: x in dom F ; :: thesis: (F ';' (Stop S)) . x = F . x
dom (CutLastLoc F) misses dom (Shift ((IncAddr ((Stop S),((card F) -' 1))),((card F) -' 1))) by Th100;
then A5: {} = (dom (CutLastLoc F)) /\ (dom (Shift ((IncAddr ((Stop S),((card F) -' 1))),((card F) -' 1)))) by XBOOLE_0:def 7;

per cases ( x in dom (CutLastLoc F) or x in {(LastLoc F)} ) by A2, A4, XBOOLE_0:def 3;

suppose A6: x in dom (CutLastLoc F) ; :: thesis: (F ';' (Stop S)) . x = F . x

then not x in dom (Shift ((IncAddr ((Stop S),((card F) -' 1))),((card F) -' 1))) by A5, XBOOLE_0:def 4;
hence (F ';' (Stop S)) . x = (CutLastLoc F) . x by FUNCT_4:12
.= F . x by A6, GRFUNC_1:8 ;
:: thesis: verum

end;

suppose x in {(LastLoc F)} ; :: thesis: (F ';' (Stop S)) . x = F . x

then A7: x = LastLoc F by TARSKI:def 1;
then A8: x = (card F) -' 1 by AFINSQ_1:74;
A9: 0 in dom (Stop S) by Lm5;
dom (Shift ((Stop S),((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Element of NAT : m in dom (Stop S) } by VALUED_1:def 12;
then 0 + ((card F) -' 1) in dom (Shift ((Stop S),((card F) -' 1))) by A9;
hence (F ';' (Stop S)) . x = (Shift ((Stop S),(0 + ((card F) -' 1)))) . x by A1, A8, FUNCT_4:14
.= (Stop S) . 0 by A8, A9, VALUED_1:def 12
.= halt S by FUNCOP_1:87
.= F . x by A7, Def25 ;
:: thesis: verum

end;

end;

end;

hence F ';' (Stop S) = F by A3, FUNCT_1:9; :: thesis: verum