We say the AIG Alists
This is a universal equivalence, introduced using def-universal-equiv.
Function:
(defun aig-alist-equiv (x y) (declare (xargs :non-executable t)) (declare (xargs :guard t)) (prog2$ (throw-nonexec-error 'aig-alist-equiv (list x y)) (let ((k (aig-alist-equiv-witness x y))) (and (iff (hons-assoc-equal k x) (hons-assoc-equal k y)) (aig-equiv (cdr (hons-assoc-equal k x)) (cdr (hons-assoc-equal k y)))))))
Theorem:
(defthm aig-alist-equiv-necc (implies (not (and (iff (hons-assoc-equal k x) (hons-assoc-equal k y)) (aig-equiv (cdr (hons-assoc-equal k x)) (cdr (hons-assoc-equal k y))))) (not (aig-alist-equiv x y))))
Theorem:
(defthm aig-alist-equiv-witnessing-witness-rule-correct (implies (not ((lambda (k y x) (not (if (iff (hons-assoc-equal k x) (hons-assoc-equal k y)) (aig-equiv (cdr (hons-assoc-equal k x)) (cdr (hons-assoc-equal k y))) 'nil))) (aig-alist-equiv-witness x y) y x)) (aig-alist-equiv x y)) :rule-classes nil)
Theorem:
(defthm aig-alist-equiv-instancing-instance-rule-correct (implies (not (if (iff (hons-assoc-equal k x) (hons-assoc-equal k y)) (aig-equiv (cdr (hons-assoc-equal k x)) (cdr (hons-assoc-equal k y))) 'nil)) (not (aig-alist-equiv x y))) :rule-classes nil)
Theorem:
(defthm aig-alist-equiv-is-an-equivalence (and (booleanp (aig-alist-equiv x y)) (aig-alist-equiv x x) (implies (aig-alist-equiv x y) (aig-alist-equiv y x)) (implies (and (aig-alist-equiv x y) (aig-alist-equiv y z)) (aig-alist-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm alist-equiv-refines-aig-alist-equiv (implies (alist-equiv x y) (aig-alist-equiv x y)) :rule-classes (:refinement))