  The aim of this article is to employ the Lazy Set algorithm as an example for
a mathematical framework for proving the linearizability of distributed
systems. The proof in this approach is divided into two stages of lower and
higher abstraction level. At the higher level a list of "axioms" is formulated
and a proof is given that any model theoretic structure that satisfies these
axioms is linearizable. At this level the algorithm is not mentioned. At the
lower level, a Simpler Lazy Set algorithm is described, and it is shown that
any execution of this simpler algorithm generates a model of these axioms (and
is therefore linearizable). Finally the linearization of the Lazy Set algorithm
is obtained by proving that any of its executions has a {\em reduct} that is an
execution of the Simpler algorithm. So the reduct executions are linearizable
and this entails immediately linearizability of the Lazy Set algorithm itself.
