:: deftheorem Def11 defines LastLoc AMI_WSTD:def 11 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b₂ -valued non empty finite Function
for b₄ being Element of NAT holds
( b₄ = LastLoc F iff ex M being non empty finite natural-membered set st
( M = { (locnum (l,S)) where l is Element of NAT : l in dom F } & b₄ = il. (S,(max M)) ) );