Currently data-based synthesis performs symbolic reachability using full transition relations, in the sense that `CifToBddConverter#convertUpdates` generates 'unchanged state predicates' for every variable that's not written to by the edge update. However, such unchanged state predicates are not needed for symbolically computing reachable states, as one could also quantify over only the BDD variables that are updated by an edge, when applying `CifBddEdge#apply`. Moreover, the BDD operations `relnext` and `relprev`, as proposed in #865, are implemented to be able to handle partial transition relations. Not having to generate/consider unchanged state predicates further improves the performance and memory usage of data-based synthesis with respect to #865.