Avoid overlap of equations for Bool combinators simplifications

[jberthold]

This is a variant of #3786 which turns all equations that focus on the 2nd argument of a Bool combinator as simplifications. In doing this, we retain a complete set of defining equations but avoid the problem described below.

Equations are kept in groups by combinator, rather than splitting them into defining and simplification equations in different modules.

---

Rules like this pair

rule false andBool _:Bool => false
rule _:Bool andBool false => false

were previously in BOOL-COMMON and were said to demonstrate the implemented semantics of the hooks.
As kore-rpc-booster does not have its own hooks, the rules now come into effect themselves.
This causes issues because of the obvious overlap of rule matches (consider subject term false andBool false which matches both rule LHSs).
This PR addresses the kore-rpc-booster issue by declaring some of the rules for Bool combinators as simplifications (whose application is optional - simplifications are trusted to be sound regardless of their (priority) order, whereas function equations with overlapping cases or uncertain matches lead to aborting evaluation in kore-rpc-booster to avoid unsoundness).

Also removed some trailing whitespace from the domains.md file.

[jberthold]

@ehildenb @Baltoli please choose and approve your preferred version and we close the resp. other PR.

[ehildenb]

@jberthold did you have a chance to check the performance of this one on KEVM and Kontrol? This will make it so that the overlapping rules are applied in different phases, the normal equation phase or the simplification phase, so could have a weird effect on performance.

[jberthold]

@jberthold did you have a chance to check the performance of this one on KEVM and Kontrol? This will make it so that the overlapping rules are applied in different phases, the normal equation phase or the simplification phase, so could have a weird effect on performance.

I ran this version with kore-rpc (no significant changes) and with an experimental branch of booster before making the other variant a PR, and re-ran some of the tests with booster from master (speedup comparable to that of the other PR).

AFAICT kore-rpc does not apply any of those rules but instead runs the hooked low-level implementation. For booster the phase separation separates the overlapping equations which resolves the issue of indeterminate matching when the first argument is a variable.

[jberthold]

I re-measured the evm-semantics proofs with booster and K from this branch - consistent results with what I expected.

BTW these measurements are a bit noisy because of the re-compilation (I am getting a screenful of z3 processes when I run with 4-fold parallelism), it would be great if we could avoid recompiling for every test run.