let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F being non empty NAT -defined initial FinPartState of
for G being non empty NAT -defined the Instructions of b₁ -valued 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 homogeneous regular J/A-independent COM-Struct of N; :: thesis: for F being non empty NAT -defined initial FinPartState of
for G being non empty NAT -defined the Instructions of S -valued FinPartState of holds dom (CutLastLoc F) misses dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))
let F be non empty NAT -defined initial FinPartState of ; :: thesis: for G being non empty NAT -defined the Instructions of S -valued FinPartState of holds dom (CutLastLoc F) misses dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))
let G be non empty NAT -defined the Instructions of S -valued 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 non empty NAT -defined 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;