let S be COM-Struct ; :: thesis: for F, G being Program of S holds CutLastLoc F c= CutLastLoc (F ';' G)
let F, G be Program of S; :: thesis: CutLastLoc F c= CutLastLoc (F ';' G)
set k = (card F) -' 1;
set P = F ';' G;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def 1;
A2: dom (CutLastLoc F) = { m where m is Element of NAT : m < card (CutLastLoc F) } by AFINSQ_1:68;
A3: card (CutLastLoc (F ';' G)) = (card (F ';' G)) - 1 by VALUED_1:38
.= (((card F) + (card G)) - 1) - 1 by Th11
.= ((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 VALUED_1:38;
1 <= card G by NAT_1:14;
then 1 - 1 <= (card G) - 1 by XREAL_1:9;
then ((card F) - 1) + 0 <= ((card F) - 1) + ((card G) - 1) by XREAL_1:6;
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 object ; :: 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 = 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, AFINSQ_1:66; :: thesis: verum

end;

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

proof

let x be object ; :: 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 = m and
A12: m < card (CutLastLoc F) by A2;
A13: dom (Reloc (G,((card F) -' 1))) = { (w + ((card F) -' 1)) where w is Nat : w in dom (IncAddr (G,((card F) -' 1))) } by VALUED_1:def 12;

A14: now :: thesis: not x in dom (Reloc (G,((card F) -' 1)))

assume x in dom (Reloc (G,((card F) -' 1))) ; :: thesis: contradiction
then consider w being Nat such that
A15: x = w + ((card F) -' 1) and
w in dom (IncAddr (G,((card F) -' 1))) by A13;
m < (card F) - 1 by A12, VALUED_1:38;
then m < (card F) -' 1 by PRE_CIRC:20;
hence contradiction by A11, A15, NAT_1:11; :: thesis: verum

end;

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

now :: thesis: not x = LastLoc (F ';' G)

assume x = LastLoc (F ';' G) ; :: thesis: contradiction
then A17: m = (card (F ';' G)) -' 1 by A11, AFINSQ_1:70
.= (card (F ';' G)) - 1 by PRE_CIRC:20 ;
card (CutLastLoc (F ';' G)) = (card (F ';' G)) - 1 by VALUED_1:38;
hence contradiction by A4, A12, A17; :: 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)))) ;
then x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A16, XBOOLE_0:def 5;
hence (CutLastLoc (F ';' G)) . x = ((CutLastLoc F) +* (Reloc (G,((card F) -' 1)))) . x by GRFUNC_1:32
.= (CutLastLoc F) . x by A14, FUNCT_4:11 ;
:: thesis: verum

end;

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