let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for F, G being NAT -defined non empty lower FinPartState of holds CutLastLoc F c= CutLastLoc (F ';' G)
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for F, G being NAT -defined non empty lower FinPartState of holds CutLastLoc F c= CutLastLoc (F ';' G)
let F, G be NAT -defined non empty lower FinPartState of ; :: thesis: CutLastLoc F c= CutLastLoc (F ';' G)
set k = (card F) -' 1;
set P = F ';' G;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by FUNCT_4:def 1;
A2: dom (CutLastLoc F) = { (il. S,m) where m is Element of NAT : m < card (CutLastLoc F) } by Th15;
A3: card (CutLastLoc (F ';' G)) = (card (F ';' G)) - 1 by Th49
.= (((card F) + (card G)) - 1) - 1 by Th52
.= ((card F) - 1) + ((card G) - 1) ;
A4: for m being Element of NAT st m < card (CutLastLoc F) holds
m < card (CutLastLoc (F ';' G))

proof

let m be Element of NAT ; :: thesis: ( m < card (CutLastLoc F) implies m < card (CutLastLoc (F ';' G)) )
assume A5: m < card (CutLastLoc F) ; :: thesis: m < card (CutLastLoc (F ';' G))
A6: card (CutLastLoc F) = (card F) - 1 by Th49;
1 <= card G by NAT_1:14;
then 1 - 1 <= (card G) - 1 by XREAL_1:11;
then ((card F) - 1) + 0 <= ((card F) - 1) + ((card G) - 1) by XREAL_1:8;
hence m < card (CutLastLoc (F ';' G)) by A3, A5, A6, XXREAL_0:2; :: thesis: verum

end;

A7: dom (CutLastLoc F) c= dom (CutLastLoc (F ';' G))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (CutLastLoc F) or x in dom (CutLastLoc (F ';' G)) )
assume x in dom (CutLastLoc F) ; :: thesis: x in dom (CutLastLoc (F ';' G))
then consider m being Element of NAT such that
A8: x = il. S,m and
A9: m < card (CutLastLoc F) by A2;
m < card (CutLastLoc (F ';' G)) by A4, A9;
hence x in dom (CutLastLoc (F ';' G)) by A8, AMISTD_1:50; :: thesis: verum

end;

for x being set st x in dom (CutLastLoc F) holds
(CutLastLoc F) . x = (CutLastLoc (F ';' G)) . x

proof

let x be set ; :: thesis: ( x in dom (CutLastLoc F) implies (CutLastLoc F) . x = (CutLastLoc (F ';' G)) . x )
assume A10: x in dom (CutLastLoc F) ; :: thesis: (CutLastLoc F) . x = (CutLastLoc (F ';' G)) . x
then consider m being Element of NAT such that
A11: x = il. S,m and
A12: m < card (CutLastLoc F) by A2;
A13: dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (il. S,(w + ((card F) -' 1))) where w is Element of NAT : il. S,w in dom (IncAddr G,((card F) -' 1)) } by Def16;

A14: now

assume x in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) ; :: thesis: contradiction
then consider w being Element of NAT such that
A15: x = il. S,(w + ((card F) -' 1)) and
il. S,w in dom (IncAddr G,((card F) -' 1)) by A13;
m < (card F) - 1 by A12, Th49;
then A16: m < (card F) -' 1 by PRE_CIRC:25;
m = w + ((card F) -' 1) by A11, A15, AMISTD_1:25;
hence contradiction by A16, NAT_1:11; :: thesis: verum

end;

A17: x in dom (F ';' G) by A1, A10, XBOOLE_0:def 3;

now

assume x = LastLoc (F ';' G) ; :: thesis: contradiction
then il. S,m = il. S,((card (F ';' G)) -' 1) by A11, AMISTD_1:55;
then A18: m = (card (F ';' G)) -' 1 by AMISTD_1:25
.= (card (F ';' G)) - 1 by PRE_CIRC:25 ;
card (CutLastLoc (F ';' G)) = (card (F ';' G)) - 1 by Th49;
hence contradiction by A4, A12, A18; :: thesis: verum

end;

then not x in {(LastLoc (F ';' G))} by TARSKI:def 1;
then not x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) by FUNCOP_1:19;
then x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A17, XBOOLE_0:def 5;
hence (CutLastLoc (F ';' G)) . x = ((CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) . x by GRFUNC_1:93
.= (CutLastLoc F) . x by A14, FUNCT_4:12 ;
:: thesis: verum

end;

hence CutLastLoc F c= CutLastLoc (F ';' G) by A7, GRFUNC_1:8; :: thesis: verum