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
|
(PROOF-CHECKER-ARRAY::ASSIGNMENTP)
(PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION)
(PROOF-CHECKER-ARRAY::ASSIGNMENTP-TRUE-LISTP)
(PROOF-CHECKER-ARRAY::ASSIGNMENTP-LITERALP-MEMBER
(432 43 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION))
(202 6 (:DEFINITION PROOF-CHECKER-ARRAY::NO-CONFLICTING-LITERALSP))
(201 7 (:DEFINITION PROOF-CHECKER-ARRAY::UNIQUE-LITERALSP))
(162 7 (:DEFINITION PROOF-CHECKER-ARRAY::LITERAL-LISTP))
(152 19 (:DEFINITION MEMBER-EQUAL))
(50 50 (:REWRITE DEFAULT-CDR))
(39 39 (:REWRITE DEFAULT-CAR))
(36 36 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(36 36 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(18 2 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
(14 14 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(14 14 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(2 2 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP))
)
(PROOF-CHECKER-ARRAY::ASSIGNMENTP-CDR
(637 63 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION))
(99 99 (:REWRITE DEFAULT-CDR))
(71 71 (:REWRITE DEFAULT-CAR))
(63 63 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(63 63 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(30 30 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
(30 30 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(11 11 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-LITERALP-MEMBER))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
)
(PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONS
(96 18 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CONJUNCTION))
(24 6 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-CDR))
(23 23 (:REWRITE DEFAULT-CDR))
(17 17 (:REWRITE DEFAULT-CAR))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::SUBSETP-MEMBER-IMPLIES-MEMBER))
(16 16 (:REWRITE PROOF-CHECKER-ARRAY::MEMBER-UNION-VARIABLES1))
(8 8 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-IMPLIES-MEMBER-OR-MEMBER-NEGATE))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::SUBSET-VARIABLESP-NOT-SUBSETP-IMPLIES-NOT-NO-CONFLICTING-LITERALSP))
(6 6 (:REWRITE PROOF-CHECKER-ARRAY::NOT-NO-CONFLICTING-LITERALSP))
(4 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
(4 4 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNMENTP-LITERALP-MEMBER))
)
|
