let N be non empty with_non-empty_elements set ; for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for F, G being non empty NAT -defined the Instructions of b1 -valued initial FinPartState of holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N; for F, G being non empty NAT -defined the Instructions of S -valued initial FinPartState of holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
let F, G be non empty NAT -defined the Instructions of S -valued initial FinPartState of ; (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
set k = (card F) -' 1;
A1:
LastLoc F = 0 + ((card F) -' 1)
by AFINSQ_1:74;
A2:
0 in dom (IncAddr (G,((card F) -' 1)))
by AFINSQ_1:69;
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
LastLoc F in dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))
by A1, A2;
hence (F ';' G) . (LastLoc F) =
(Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) . (LastLoc F)
by FUNCT_4:14
.=
(IncAddr (G,((card F) -' 1))) . 0
by A1, A2, VALUED_1:def 12
;
verum