Reasoning strategy: reduce equality of ubdds to equality of an arbitrary evaluation.
Suppose we know that
(forall values (equal (eval-bdd x values) (eval-bdd y values)))
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:
Jared Davis. Finite Set Theory based on Fully Ordered Lists. In ACL2 2004. November, 2004, Austin, TX, USA.
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)))