Logically atomic rules for the Treiber stack

It would be nice if the stack refinement could be proven with logically atomic rules for the Treiber stack.