blob: 0235b748124670bd12ebd4e3134e76cf550fc38b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
; (certify-book "equisort3")
(in-package "ACL2")
(include-book "perm")
(include-book "ordered-perms")
(include-book "convert-perm-to-how-many")
(defthm equisort
(implies (and (force (orderedp a))
(force (orderedp b))
(force (true-listp a))
(force (true-listp b))
(force (perm a b)))
(equal (equal a b) t))
:hints (("Goal" :use ordered-perms)))
(in-theory (disable equisort))
|
