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 homogeneous regular J/A-independent AMI-Struct of N
for F being NAT -defined non empty initial FinPartState of
for G being NAT -defined the Instructions of b₁ -valued 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 homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for F being NAT -defined non empty initial FinPartState of
for G being NAT -defined the Instructions of S -valued 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 initial FinPartState of ; :: thesis: for G being NAT -defined the Instructions of S -valued non empty FinPartState of holds dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
let G be NAT -defined the Instructions of S -valued 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)) = { (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr G,((card F) -' 1)) } by VALUED_1:def 12;
then consider m being Element of 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 NAT -defined non empty FinPartState of by A1, RELAT_1:60;
m + ((card F) -' 1) <= LastLoc f by A2, A4, VALUED_1:33;
then A5: m + ((card F) -' 1) <= (card f) -' 1 by AFINSQ_1:74;
A6: card f = (card F) - 1 by VALUED_1:39
.= (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;