for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F, G being NAT -defined the InstructionsF of b₂ -valued non empty finite Function st F c= G holds
LastLoc F <= LastLoc G,T