Ackermann Encoding, Bisimulations, and OBDD's