not AddTo a,b destroysdestroy intloc 0 by SCMFSA7B:13;
hence AddTo a,b is good by SCM_HALT:def 6; :: thesis: verum