A variant of Chris Hughes' solution for the if normalization challenge. #
In this variant we eschew the use of
aesop, and instead write out the proofs.
(In order to avoid duplicated names with
we put primes on the declarations in the file.)
Custom size function for if-expressions, used for proving termination.
Normalizes the expression at the same time as assigning all variables in
e to the literal booleans given by
- One or more equations did not get rendered due to their size.