At the moment, projected iteration iterates over all distinct function tables for a specific set of uninterpreted functions. However, often these yield the same update function. This is confusing, because the same function can then appear in the list multiple times, often with different syntax. It would be better to somehow "normalize" this to only list unique functions. But this could in fact be a hard problem.
At the moment, projected iteration iterates over all distinct function tables for a specific set of uninterpreted functions. However, often these yield the same update function. This is confusing, because the same function can then appear in the list multiple times, often with different syntax. It would be better to somehow "normalize" this to only list unique functions. But this could in fact be a hard problem.