Reasoning strategy: reduce equality of ubdds to equality of an arbitrary evaluation.
Suppose we know that
Actually, we can even assume that
It is somewhat tricky to implement this sort of reduction in ACL2. Our approach is very similar to the "pick a point" strategy for proving that sets are equal, described in the following paper:
The computed hint equal-by-eval-bdds-hint automates the strategy.
That is, when this hint is active, ACL2 will automatically try to use
At any rate, if you want to prove that
(equal (eval-bdd (foo ...) values) (... expression 1 ...)) (equal (eval-bdd (bar ...) values) (... expression 2 ...))
Then you will be able to prove
(defthm bdd-equivalence-constraint (implies (and (bdd-hyps) (equal (len arbitrary-values) (max (max-depth (bdd-lhs)) (max-depth (bdd-rhs)))) (boolean-listp arbitrary-values) (ubddp (bdd-lhs)) (ubddp (bdd-rhs))) (equal (eval-bdd (bdd-lhs) arbitrary-values) (eval-bdd (bdd-rhs) arbitrary-values))))
(defthm equal-by-eval-bdds (implies (and (bdd-hyps) (ubddp (bdd-lhs)) (ubddp (bdd-rhs))) (equal (equal (bdd-lhs) (bdd-rhs)) t)))