21 Apr
2015
21 Apr
'15
8:36 p.m.
On Tue, Apr 21, 2015 at 02:51:16PM +1200, Richard A. O'Keefe wrote:
You said in words that
Every S can be reconstructed from a sequence of updates:
but your formula
forall s. exists [a]. s == foldl update empty [a]
says that a (not necessarily unique) sequence of updates can be reconstructed from every S. I think you meant something like "there are no elements of S but those that can be constructed by a sequence of updates".
Those sound like the same thing to me!