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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(DUPSP)
(COLLECT-ONCE)
(MAIN-THEOREM-1-ABOUT-COLLECT-ONCE
(242 241 (:REWRITE DEFAULT-CAR))
(238 237 (:REWRITE DEFAULT-CDR))
)
(MEMBER-COLLECT-ONCE
(167 160 (:REWRITE DEFAULT-CAR))
(152 149 (:REWRITE DEFAULT-CDR))
)
(MAIN-THEOREM-2-ABOUT-COLLECT-ONCE
(36 34 (:REWRITE DEFAULT-CDR))
(28 27 (:REWRITE DEFAULT-CAR))
)
(WHILE-LOOP-VERSION)
(REV)
(LIST-MINUS)
(LIST-MINUS-APPEND
(83 73 (:REWRITE DEFAULT-CAR))
(71 64 (:REWRITE DEFAULT-CDR))
(19 19 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(MEMBER-APPEND
(56 44 (:REWRITE DEFAULT-CAR))
(48 24 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(40 31 (:REWRITE DEFAULT-CDR))
(24 24 (:TYPE-PRESCRIPTION TRUE-LISTP))
(24 24 (:TYPE-PRESCRIPTION BINARY-APPEND))
)
(COLLECT-ONCE-APPEND
(183 165 (:REWRITE DEFAULT-CDR))
(157 145 (:REWRITE DEFAULT-CAR))
(30 30 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(ASSOC-APPEND
(1526 613 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(815 613 (:TYPE-PRESCRIPTION BINARY-APPEND))
(613 613 (:TYPE-PRESCRIPTION TRUE-LISTP))
(23 20 (:REWRITE DEFAULT-CAR))
(19 16 (:REWRITE DEFAULT-CDR))
)
(MEMBER-LIST-MINUS
(165 160 (:REWRITE DEFAULT-CAR))
(129 125 (:REWRITE DEFAULT-CDR))
)
(LIST-MINUS-COLLECT-ONCE
(164 159 (:REWRITE DEFAULT-CDR))
(149 144 (:REWRITE DEFAULT-CAR))
)
(LIST-MINUS-LIST-MINUS
(103 100 (:REWRITE DEFAULT-CAR))
(92 90 (:REWRITE DEFAULT-CDR))
(33 11 (:DEFINITION BINARY-APPEND))
)
(GENERAL-EQUIVALENCE
(97 97 (:REWRITE DEFAULT-CAR))
(87 87 (:REWRITE DEFAULT-CDR))
(20 20 (:TYPE-PRESCRIPTION REV))
)
(MAIN-THEOREM-1-ABOUT-WHILE-LOOP
(771 638 (:REWRITE DEFAULT-CAR))
(681 611 (:REWRITE DEFAULT-CDR))
)
(MAIN-THEOREM-2-ABOUT-WHILE-LOOP
(12 1 (:DEFINITION COLLECT-ONCE))
(8 1 (:DEFINITION REV))
(7 7 (:REWRITE DEFAULT-CDR))
(7 7 (:REWRITE DEFAULT-CAR))
(7 1 (:DEFINITION LIST-MINUS))
(5 1 (:DEFINITION BINARY-APPEND))
(4 4 (:TYPE-PRESCRIPTION REV))
(4 2 (:DEFINITION MEMBER-EQUAL))
(2 2 (:TYPE-PRESCRIPTION LIST-MINUS))
(1 1 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
)
(SUBSETP-CONS
(43 43 (:REWRITE DEFAULT-CAR))
(22 22 (:REWRITE DEFAULT-CDR))
)
(SUBSETP-REFLEXIVE
(22 22 (:REWRITE DEFAULT-CAR))
(19 19 (:REWRITE DEFAULT-CDR))
)
(TRANS-SUBSETP
(116 116 (:REWRITE DEFAULT-CAR))
(89 89 (:REWRITE DEFAULT-CDR))
)
(APPEND-CONS-V-CONS-APPEND-1
(340 16 (:REWRITE MEMBER-APPEND))
(207 96 (:REWRITE DEFAULT-CAR))
(181 181 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(151 73 (:REWRITE DEFAULT-CDR))
)
(APPEND-CONS-V-CONS-APPEND-2
(63 51 (:REWRITE DEFAULT-CAR))
(46 37 (:REWRITE DEFAULT-CDR))
)
(SUBSETP-APPEND-CONS-CONS-APPEND
(90 3 (:DEFINITION SUBSETP-EQUAL))
(55 8 (:DEFINITION MEMBER-EQUAL))
(39 3 (:REWRITE MEMBER-APPEND))
(34 2 (:REWRITE SUBSETP-CONS))
(24 21 (:REWRITE DEFAULT-CAR))
(20 17 (:REWRITE DEFAULT-CDR))
(18 6 (:DEFINITION BINARY-APPEND))
(17 17 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(8 4 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(4 4 (:TYPE-PRESCRIPTION TRUE-LISTP))
(4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
(2 2 (:REWRITE CDR-CONS))
(2 2 (:REWRITE CAR-CONS))
)
(MAIN-LEMMA-1-ABOUT-WHILE-LOOP-VERSION
(30 30 (:REWRITE DEFAULT-CAR))
(27 27 (:REWRITE DEFAULT-CDR))
(20 1 (:DEFINITION SUBSETP-EQUAL))
(10 1 (:REWRITE MEMBER-APPEND))
(7 5 (:TYPE-PRESCRIPTION WHILE-LOOP-VERSION))
(1 1 (:REWRITE CDR-CONS))
(1 1 (:REWRITE CAR-CONS))
)
(SUBSETP-APPEND-NIL
(144 18 (:REWRITE APPEND-TO-NIL))
(128 40 (:REWRITE TRANS-SUBSETP))
(99 9 (:DEFINITION BINARY-APPEND))
(90 90 (:TYPE-PRESCRIPTION TRUE-LISTP))
(90 18 (:DEFINITION TRUE-LISTP))
(65 65 (:REWRITE DEFAULT-CDR))
(57 57 (:REWRITE DEFAULT-CAR))
(9 9 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(9 9 (:TYPE-PRESCRIPTION BINARY-APPEND))
)
(MAIN-THEOREM-1-ABOUT-WHILE-LOOP-VERSION)
(MAIN-LEMMA-2-ABOUT-WHILE-LOOP-VERSION
(82 78 (:REWRITE DEFAULT-CDR))
(75 73 (:REWRITE DEFAULT-CAR))
)
(MAIN-THEOREM-2-ABOUT-WHILE-LOOP-VERSION)
|
