We have rigorously proved that UniStore correctly implements the specification of
PoR consistency for the case when the data store manages last-writer-wins registers. The
proof uses the formal framework
from [1]}, [2]}, [3]} and establishes
Properties REF -REF  stated earlier. Due to
space constraints, we defer the proof
to §REF .
