let N be 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, G being NAT -defined non empty lower FinPartState of
for f being Instruction-Location of S st locnum f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for F, G being NAT -defined non empty lower FinPartState of
for f being Instruction-Location of S st locnum f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f
let F, G be NAT -defined non empty lower FinPartState of ; :: thesis: for f being Instruction-Location of S st locnum f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f
let f be Instruction-Location of S; :: thesis: ( locnum f < (card F) - 1 implies (IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f )
set k = (card F) -' 1;
set P = F ';' G;
assume locnum f < (card F) - 1 ; :: thesis: (IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f
then locnum f < card (CutLastLoc F) by Th49;
then A1: il. S,(locnum f) in dom (CutLastLoc F) by AMISTD_1:50;
A2: f = il. S,(locnum f) by AMISTD_1:def 13;
A3: dom (CutLastLoc F) c= dom F by GRFUNC_1:8;
CutLastLoc F c= CutLastLoc (F ';' G) by Th54;
then CutLastLoc F c= F ';' G by XBOOLE_1:1;
then A4: dom (CutLastLoc F) c= dom (F ';' G) by GRFUNC_1:8;
A5: F . (il. S,(locnum f)) = pi F,(il. S,(locnum f)) by A1, A3, AMI_1:def 47;
dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by Th50;
then (dom (CutLastLoc F)) /\ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) = {} by XBOOLE_0:def 7;
then not il. S,(locnum f) in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A1, XBOOLE_0:def 4;
then A6: (F ';' G) . (il. S,(locnum f)) = (CutLastLoc F) . (il. S,(locnum f)) by FUNCT_4:12
.= F . (il. S,(locnum f)) by A1, GRFUNC_1:8 ;
thus (IncAddr F,((card F) -' 1)) . f = IncAddr (pi F,(il. S,(locnum f))),((card F) -' 1) by A1, A2, A3, Def15
.= IncAddr (pi (F ';' G),(il. S,(locnum f))),((card F) -' 1) by A1, A4, A5, A6, AMI_1:def 47
.= (IncAddr (F ';' G),((card F) -' 1)) . f by A1, A2, A4, Def15 ; :: thesis: verum