Previously, we forced everything to NF, so we should not have any not-normalized terms as $\rho$.
Computing inside $\rho$ is generally redundant, and may lead to explosion of the term. This is, however, not relevant in the context of confluence test as far as I can see. So we can allow reduction under $\rho$ for confluence tests, but forbid them when actually normalizing stuff (making it more lazy in a sense).
This PR removes NF conditions from the rule set.
Also, test from #448 is fixed, but the issue still needs to be considered, because this breaks confluence.
The confluence via Quickcheck fails as well, but not because of the above; there are critical pairs with
⊥
that do not look critical to me, e.g.:PR-Codex overview
This PR focuses on updating object structures and fixing application patterns related to ξ in the codebase.
Detailed summary
dataization.yaml
dataization.yaml
yegor.yaml