Proving properties on programs operating over arrays, or array-like data structures, most often involves universally quantified invariants, e.g., “all elements below index i are nonzero”. In this article, we propose a general data abstraction scheme operating on Horn Formula for which we provide a relative completeness resolution scheme: the generated purely scalar invariant search problem has a solution if and only if the original problem has one expressible by the abstraction.