other
(in-package "ACL2")
tails-ac=tailstheorem
(defthm tails-ac=tails (equal (tails-ac lst ac) (revappend ac (tails lst))))
other
(verify-guards tails)
loop$-as-ac=loop$-astheorem
(defthm loop$-as-ac=loop$-as (equal (loop$-as-ac tuple ac) (revappend ac (loop$-as tuple))))
other
(verify-guards loop$-as)
from-to-by-measurefunction
(defun from-to-by-measure (i j) (if (and (integerp i) (integerp j) (<= i j)) (+ 1 (- j i)) 0))
natp-from-to-by-measuretheorem
(defthm natp-from-to-by-measure (natp (from-to-by-measure i j)) :rule-classes :type-prescription)
natp-from-to-by-measuretheorem
(defthm natp-from-to-by-measure (natp (from-to-by-measure i j)) :rule-classes :type-prescription)
other
(verify-guards from-to-by :hints (("Goal" :in-theory (disable floor) :use from-to-by-ac=from-to-by-special-case)))