let S be COM-Struct ; for F being Program of S
for G being non empty preProgram of S holds dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
let F be Program of S; for G being non empty preProgram of S holds dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
let G be non empty preProgram of S; dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
set k = (card F) -' 1;
assume
not dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
; contradiction
then consider il being object such that
A1:
il in (dom (CutLastLoc F)) /\ (dom (Reloc (G,((card F) -' 1))))
by XBOOLE_0:4;
A2:
il in dom (CutLastLoc F)
by A1, XBOOLE_0:def 4;
A3:
il in dom (Reloc (G,((card F) -' 1)))
by A1, XBOOLE_0:def 4;
dom (Reloc (G,((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Nat : m in dom (IncAddr (G,((card F) -' 1))) }
by VALUED_1:def 12;
then consider m being Nat such that
A4:
il = m + ((card F) -' 1)
and
m in dom (IncAddr (G,((card F) -' 1)))
by A3;
reconsider f = CutLastLoc F as non empty NAT -defined finite Function by A1;
m + ((card F) -' 1) <= LastLoc f
by A2, A4, VALUED_1:32;
then A5:
m + ((card F) -' 1) <= (card f) -' 1
by AFINSQ_1:70;
A6: card f =
(card F) - 1
by VALUED_1:38
.=
(card F) -' 1
by PRE_CIRC:20
;