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 regular AMI-Struct of N
for F, G being NAT -defined non empty lower FinPartState of holds (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . (il. S,0 )
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for F, G being NAT -defined non empty lower FinPartState of holds (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . (il. S,0 )
let F, G be NAT -defined non empty lower FinPartState of ; :: thesis: (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . (il. S,0 )
set k = (card F) -' 1;
A1: LastLoc F = il. S,(0 + ((card F) -' 1)) by AMISTD_1:55;
A2: il. S,0 in dom (IncAddr G,((card F) -' 1)) by AMISTD_1:49;
dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (il. S,(m + ((card F) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr G,((card F) -' 1)) } by Def16;
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)) . (il. S,0 ) by A1, A2, Def16 ;
:: thesis: verum