@whitequark@mastodon.social FWIW for simple equivalence checking without any temporal elements it should be fairly easy to check it with SAT, and most SAT solvers can output a proof for the result (which can get subsequently checked by one of formally verified proof checkers) Though that's a fair bit of work for little benefit (I guess maybe it could be somewhat faster as well)