5 Selective undo

From any state can selective undo to revert to any other state in the lattice - even to a position not on the path corresponding to the history buffer.

Selective undo from the current state to another lattice state

Undo involves factorisation

Step 1: Factorise the history buffer HB with respect to vector time v:

Factorising the history buffer into a prefix and suffix

Note that since v is a causally valid vector time, we are only transposing concurrent operations.

Step 2: Apply S-1 = [S5-1 S4-1 S3-1 S2-1 S1-1] to undo the effect of those operations on the database.

Step 3: Let HB := P