Open jaypantone opened 2 years ago
this issue is slightly more subtle. The rule needed to expand the verified node 25 is 25 -> (4, 24), but our original spec contains the reverse rule 24 -> (25, 4). I believe this is because locally factorable tells us 25 relies on 0, but really it relies on 24, and in our spec its the only place 24 occurs so we don't recognise the shift between 0 and 24.
Another observation, if we had the reverse add assumption to give the rule 24 -> (0), perhaps we wouldn't need to go through the reverse cartesian product in the first place.
To recreate in about 5 minutes:
The problem, seems to be:
Full traceback: