(svexlists-rewrite-until-same x y limit) → (mv xx yy)
Function:
(defun svexlists-rewrite-until-same (x y limit) (declare (xargs :guard (and (svexlist-p x) (svexlist-p y) (natp limit)))) (let ((__function__ 'svexlists-rewrite-until-same)) (declare (ignorable __function__)) (b* (((when (zp limit)) (cw "svexlists-rewrite-until-same: limit ran out. Total size: ~x0, x: ~x1, y: ~x2~%" (svexlist-opcount (append x y)) (svexlist-opcount x) (svexlist-opcount y)) (mv (svexlist-fix x) (svexlist-fix y))) ((when (hons-equal (svexlist-fix x) (svexlist-fix y))) (cw "svexlists-rewrite-until-same: success~%") (mv (svexlist-fix x) (svexlist-fix y))) (rw (svexlist-rewrite-top (append x y) :verbosep t)) (len (len x)) (newx (take len rw)) (newy (nthcdr len rw)) ((when (and (hons-equal newx (svexlist-fix x)) (hons-equal newy (svexlist-fix y)))) (cw "svexlists-rewrite-until-same: fail, sizes: ~x0, ~x1~%" (svexlist-opcount newx) (svexlist-opcount newy)) (mv newx newy))) (svexlists-rewrite-until-same newx newy (1- limit)))))
Theorem:
(defthm svexlist-p-of-svexlists-rewrite-until-same.xx (b* (((mv ?xx ?yy) (svexlists-rewrite-until-same x y limit))) (svexlist-p xx)) :rule-classes :rewrite)
Theorem:
(defthm svexlist-p-of-svexlists-rewrite-until-same.yy (b* (((mv ?xx ?yy) (svexlists-rewrite-until-same x y limit))) (svexlist-p yy)) :rule-classes :rewrite)
Theorem:
(defthm svexlists-rewrite-until-same-correct (b* (((mv newx newy) (svexlists-rewrite-until-same x y limit))) (and (equal (svexlist-eval newx env) (svexlist-eval x env)) (equal (svexlist-eval newy env) (svexlist-eval y env)))))
Theorem:
(defthm len-of-svexlists-rewrite-until-same (b* (((mv newx newy) (svexlists-rewrite-until-same x y limit))) (and (equal (len newx) (len x)) (equal (len newy) (len y)))))
Theorem:
(defthm consp-of-svexlists-rewrite-until-same (b* (((mv newx newy) (svexlists-rewrite-until-same x y limit))) (and (equal (consp newx) (consp x)) (equal (consp newy) (consp y)))))
Theorem:
(defthm svexlists-rewrite-until-same-of-svexlist-fix-x (equal (svexlists-rewrite-until-same (svexlist-fix x) y limit) (svexlists-rewrite-until-same x y limit)))
Theorem:
(defthm svexlists-rewrite-until-same-svexlist-equiv-congruence-on-x (implies (svexlist-equiv x x-equiv) (equal (svexlists-rewrite-until-same x y limit) (svexlists-rewrite-until-same x-equiv y limit))) :rule-classes :congruence)
Theorem:
(defthm svexlists-rewrite-until-same-of-svexlist-fix-y (equal (svexlists-rewrite-until-same x (svexlist-fix y) limit) (svexlists-rewrite-until-same x y limit)))
Theorem:
(defthm svexlists-rewrite-until-same-svexlist-equiv-congruence-on-y (implies (svexlist-equiv y y-equiv) (equal (svexlists-rewrite-until-same x y limit) (svexlists-rewrite-until-same x y-equiv limit))) :rule-classes :congruence)
Theorem:
(defthm svexlists-rewrite-until-same-of-nfix-limit (equal (svexlists-rewrite-until-same x y (nfix limit)) (svexlists-rewrite-until-same x y limit)))
Theorem:
(defthm svexlists-rewrite-until-same-nat-equiv-congruence-on-limit (implies (nat-equiv limit limit-equiv) (equal (svexlists-rewrite-until-same x y limit) (svexlists-rewrite-until-same x y limit-equiv))) :rule-classes :congruence)