@pervognsen reminds me of how in TLA+, inveraints are much faster to model-check than temporal properties. Would the difference between "not exists two list elements with the same next" and "next[prev[x]] = x" be of similar magnitude?
=> More informations about this toot | View the thread | More toots from wolf480pl@mstdn.io
=> View pervognsen@mastodon.social profile
text/geminiThis content has been proxied by September (ba2dc).