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, G being NAT -defined the Instructions of b₁ -valued non empty initial FinPartState of
for f being Element of NAT st 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 homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for F, G being NAT -defined the Instructions of S -valued non empty initial FinPartState of
for f being Element of NAT st f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f
let F, G be NAT -defined the Instructions of S -valued non empty initial FinPartState of ; :: thesis: for f being Element of NAT st f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f
let f be Element of NAT ; :: thesis: ( 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 f < (card F) - 1 ; :: thesis: (IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f
then f < card (CutLastLoc F) by VALUED_1:39;
then A1: f in dom (CutLastLoc F) by AFINSQ_1:70;
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 . f = F /. f by A1, A3, PARTFUN1:def 8;
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 f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) by A1, XBOOLE_0:def 4;
then A6: (F ';' G) . f = (CutLastLoc F) . f by FUNCT_4:12
.= F . f by A1, GRFUNC_1:8 ;
thus (IncAddr F,((card F) -' 1)) . f = IncAddr (F /. f),((card F) -' 1) by A1, A3, Def15
.= IncAddr ((F ';' G) /. f),((card F) -' 1) by A1, A4, A5, A6, PARTFUN1:def 8
.= (IncAddr (F ';' G),((card F) -' 1)) . f by A1, A4, Def15 ; :: thesis: verum