blob: d819fdfaa779c53504803b7c423c3af2c006cd80 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
; (certify-book "sorts-equivalent3")
(in-package "ACL2")
(include-book "equisort3")
(include-book "isort")
(include-book "msort")
(include-book "qsort")
(include-book "bsort")
; Matt K.: Disabled forcing after Version 6.1, due to heuristic change that
; allows forcing before a failure from the ancestors check.
(local (in-theory (disable (force))))
(defthm msort-is-isort
(equal (msort x) (isort x))
:hints (("Goal" :in-theory (enable equisort))))
(defthm qsort-is-isort
(equal (qsort x) (isort x))
:hints (("Goal" :in-theory (enable equisort))))
(defthm bsort-is-isort
(implies (true-listp x)
(equal (bsort x) (isort x)))
:hints (("Goal" :in-theory (e/d (equisort) (bsort isort)))))
|
