let S be COM-Struct ; for F, G being Program of S
for f being Nat st f < (card F) - 1 holds
(IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
let F, G be Program of S; for f being Nat st f < (card F) - 1 holds
(IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
let f be Nat; ( 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 A1:
f < (card F) - 1
; (IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
then
f < card (CutLastLoc F)
by VALUED_1:38;
then A2:
f in dom (CutLastLoc F)
by AFINSQ_1:66;
A3:
dom (CutLastLoc F) c= dom F
by GRFUNC_1:2;
CutLastLoc F c= CutLastLoc (F ';' G)
by Th13;
then
CutLastLoc F c= F ';' G
by XBOOLE_1:1;
then A4:
dom (CutLastLoc F) c= dom (F ';' G)
by GRFUNC_1:2;
A5:
F . f = F /. f
by A2, A3, PARTFUN1:def 6;
A6:
(F ';' G) . f = F . f
by Lm6, A1;
thus (IncAddr (F,((card F) -' 1))) . f =
IncAddr ((F /. f),((card F) -' 1))
by A2, A3, Def9
.=
IncAddr (((F ';' G) /. f),((card F) -' 1))
by A2, A4, A5, A6, PARTFUN1:def 6
.=
(IncAddr ((F ';' G),((card F) -' 1))) . f
by A2, A4, Def9
; verum