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 holds (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . 0
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 holds (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . 0
let F, G be NAT -defined the Instructions of S -valued non empty initial FinPartState of ; :: thesis: (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 ;
:: thesis: verum