Consider mentioning TLAPS in "Refactor Properties"

[lemmy]

Instead of having TLC check refactor properties, TLAPS is occasionally able to help:

    Linearizability == LET Ops == {o \in Operations : LSN[o] # 0}
                       IN  \A i, j \in Ops :
                       times[j][2] # Pending
                            => (times[i][1] >= times[j][2] => LSN[i] >= LSN[j])

    LinearizabilityRef ==
        \A i, j \in Operations :
            /\ LSN[i] # 0 /\ LSN[j] # 0
            /\ times[j][2] # Pending
            => (times[i][1] >= times[j][2] => LSN[i] >= LSN[j])

    THEOREM LinearizabilityRef <=> Linearizability
    BY DEF  Linearizability, LinearizabilityRef