|
|
|
|
|
|
by ahelwer
953 days ago
|
|
|
It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next monthly TLA+ meeting. |
|
|