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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
(in-package "DJVM")
(include-book "consistent-state")
(include-book "consistent-state-obj-init")
(acl2::set-verify-guards-eagerness 2)
(defun consistent-state-strong (s)
(and (consistent-state s)
(consistent-state-obj-init s)))
;;;
;;; experiment, shall we leave it enabled!!
;;;
;;; Fri Aug 5 14:00:23 2005
;;;
(in-theory (disable consistent-state-strong
consistent-state
consistent-state-obj-init))
(defthm consistent-state-strong-implies-consistent-state-f
(implies (consistent-state-strong s)
(consistent-state s))
:hints (("Goal" :in-theory (enable consistent-state-strong)))
:rule-classes :forward-chaining)
(defthm consistent-state-strong-implies-consistent-state-obj-init-f
(implies (consistent-state-strong s)
(consistent-state-obj-init s))
:hints (("Goal" :in-theory (enable consistent-state-strong)))
:rule-classes :forward-chaining)
(defthm consistent-state-strong-implies-consistent-state-b
(implies (and (syntaxp (symbolp s))
(consistent-state-strong s))
(consistent-state s))
:hints (("Goal" :in-theory (enable consistent-state-strong))))
(defthm consistent-state-strong-implies-consistent-state-obj-init-b
(implies (and (syntaxp (symbolp s))
(consistent-state-strong s))
(consistent-state-obj-init s))
:hints (("Goal" :in-theory (enable consistent-state-strong))))
(defthm consistent-state-strong-implied-by-b
(implies (and (syntaxp (not (symbolp s)))
(consistent-state s)
(consistent-state-obj-init s))
(consistent-state-strong s))
:hints (("Goal" :in-theory (enable consistent-state-strong))))
|
