let S be COM-Struct ; :: thesis: 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; :: thesis: 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; :: thesis: 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))) ; :: thesis: 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 ;
per cases ( ((card F) -' 1) - 1 >= 0 or ((card F) -' 1) - 1 < 0 ) ;
suppose ((card F) -' 1) - 1 >= 0 ; :: thesis: contradiction
then m + ((card F) -' 1) <= ((card F) -' 1) - 1 by A5, A6, XREAL_0:def 2;
then (m + ((card F) -' 1)) - ((card F) -' 1) <= (((card F) -' 1) - 1) - ((card F) -' 1) by XREAL_1:9;
hence contradiction by Lm4; :: thesis: verum
end;
suppose ((card F) -' 1) - 1 < 0 ; :: thesis: contradiction
then ( m + ((card F) -' 1) = 0 or m + ((card F) -' 1) < 0 ) by A5, A6, XREAL_0:def 2;
hence contradiction by A6; :: thesis: verum
end;
end;