let S be COM-Struct ; :: thesis: 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; :: thesis: 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; :: 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 A1: 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: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 ; :: thesis: verum