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 being NAT -defined non empty lower FinPartState of
for G being NAT -defined non empty FinPartState of holds dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for F being NAT -defined non empty lower FinPartState of
for G being NAT -defined non empty FinPartState of holds dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
let F be NAT -defined non empty lower FinPartState of ; :: thesis: for G being NAT -defined non empty FinPartState of holds dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
let G be NAT -defined non empty FinPartState of ; :: thesis: dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
set k = (card F) -' 1;
assume not dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) ; :: thesis: contradiction
then consider il being set such that
A1: il in (dom (CutLastLoc F)) /\ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) by XBOOLE_0:4;
A2: il in dom (CutLastLoc F) by A1, XBOOLE_0:def 4;
A3: il in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A1, XBOOLE_0:def 4;
dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (il. S,(m + ((card F) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr G,((card F) -' 1)) } by Def16;
then consider m being Element of NAT such that
A4: il = il. S,(m + ((card F) -' 1)) and
il. S,m in dom (IncAddr G,((card F) -' 1)) by A3;
reconsider f = CutLastLoc F as NAT -defined non empty FinPartState of by A1, RELAT_1:60;
il. S,(m + ((card F) -' 1)) <= LastLoc f,S by A2, A4, AMISTD_1:53;
then il. S,(m + ((card F) -' 1)) <= il. S,((card f) -' 1),S by AMISTD_1:55;
then A5: m + ((card F) -' 1) <= (card f) -' 1 by AMISTD_1:28;
A6: card f = (card F) - 1 by Th49
.= (card F) -' 1 by PRE_CIRC:25 ;

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:11;
hence contradiction by Lm1; :: 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;