Expanding simplify inference about metis HOT 1 CLOSED

Hi Jonathan,

I agree that there could be a lot happening inside a single "simplify" inference. Unfortunately, I've just taken a look at the relevant code and I think it would take a major redesign to emit finer-grained proof steps, which I don't have the bandwidth to undertake for the foreseeable future.

In case it helps, here is what Metis is doing during this specific "simplify" inference:

1. The formula normalize_0_0 is traversed, and the subformula ~q is replaced with $false using normalize_0_3.

2. When reassembling normalize_0_0 the built-in simplification rules $false | r = r and ~r & r = $false are applied, resulting in what you see in normalize_0_4.

If you needed to implement this functionality for your project I'd be happy to receive a pull-request from you :-)

from metis.