let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of N
for F being pre-Macro of S holds F ';' (Stop S) = F
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-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 Th48;
dom (Shift (Stop S),((card F) -' 1)) = dom ((il. S,((card F) -' 1)) .--> (halt S)) by Th58
.= {(il. S,((card F) -' 1))} by FUNCOP_1:19
.= {(LastLoc F)} by AMISTD_1:55 ;
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 Th50;
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 = il. S,((card F) -' 1) by AMISTD_1:55;
A9: il. S,0 in dom (Stop S) by Lm5;
dom (Shift (Stop S),((card F) -' 1)) = { (il. S,(m + ((card F) -' 1))) where m is Element of NAT : il. S,m in dom (Stop S) } by Def16;
then il. S,(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) . (il. S,0 ) by A8, A9, Def16
.= halt S by FUNCOP_1:87
.= F . x by A7, AMISTD_1:def 22 ;
:: thesis: verum

end;

end;

end;

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