TLA+ Linearizability proof for a concurrent union-find object - Ram, Karun