intloc (n + 1) <> intloc 0 by AMI_3:52;
hence not intloc (n + 1) is read-only by SF_MASTR:def 5; :: thesis: verum