:: deftheorem defines -' AMI_WSTD:def 14 :
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 loc being Element of NAT
for k being Nat holds loc -' (k,S) = il. (S,((locnum (loc,S)) -' k));