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

Undo involves factorisation

Step 1: Factorise HB with respect to v

selective-undo-hb

Step 2: Apply S-1 = [S5-1 S4-1 S3-1 S2-1 S1-1]

Step 3: Let HB := P