theorem Th13: :: SF_MASTR:13

UsedIntLoc (halt SCM+FSA) = {}