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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
(MEM$C-ENTRYP)
(ST$CP+
(20 4 (:DEFINITION LEN))
(11 11 (:REWRITE DEFAULT-CAR))
(8 8 (:REWRITE DEFAULT-CDR))
(8 4 (:REWRITE DEFAULT-+-2))
(6 3 (:DEFINITION TRUE-LISTP))
(4 4 (:REWRITE DEFAULT-+-1))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(MAP$AP)
(ST$AP)
(MISC$A)
(UPDATE-MISC$A
(10 5 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
(5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(MAP$AP-FORWARD-TO-EQLABLE-ALISTP
(51 51 (:REWRITE DEFAULT-CAR))
(12 12 (:REWRITE DEFAULT-CDR))
(12 12 (:REWRITE DEFAULT-<-2))
(12 12 (:REWRITE DEFAULT-<-1))
)
(LOOKUP$A
(20 1 (:DEFINITION MAP$AP))
(11 11 (:REWRITE DEFAULT-CAR))
(9 9 (:REWRITE DEFAULT-CDR))
(6 2 (:DEFINITION NATP))
(5 5 (:REWRITE DEFAULT-<-2))
(5 5 (:REWRITE DEFAULT-<-1))
(5 1 (:DEFINITION LEN))
(5 1 (:DEFINITION ASSOC-EQUAL))
(4 2 (:DEFINITION NTH))
(2 1 (:REWRITE DEFAULT-+-2))
(2 1 (:DEFINITION TRUE-LISTP))
(1 1 (:TYPE-PRESCRIPTION MEM$C-ENTRYP))
(1 1 (:REWRITE DEFAULT-+-1))
)
(UPDATE$A)
(CORR-MEM)
(ST$CORR)
(CREATE-ST$A)
(ST$CORR-IMPLIES-ST$CP+
(48 48 (:REWRITE DEFAULT-CAR))
(40 2 (:DEFINITION MAP$AP))
(35 35 (:REWRITE DEFAULT-CDR))
(20 10 (:REWRITE DEFAULT-+-2))
(18 2 (:DEFINITION LOOKUP$A))
(12 4 (:DEFINITION NATP))
(10 10 (:REWRITE DEFAULT-+-1))
(10 2 (:DEFINITION ASSOC-EQUAL))
(9 9 (:REWRITE DEFAULT-<-2))
(9 9 (:REWRITE DEFAULT-<-1))
(8 4 (:DEFINITION TRUE-LISTP))
)
(ST$CORR-THM
(53 53 (:REWRITE DEFAULT-CAR))
(40 40 (:REWRITE DEFAULT-CDR))
(18 2 (:DEFINITION LOOKUP$A))
(16 8 (:REWRITE DEFAULT-+-2))
(14 14 (:REWRITE DEFAULT-<-2))
(14 14 (:REWRITE DEFAULT-<-1))
(12 2 (:DEFINITION MEM$CP))
(10 2 (:DEFINITION ASSOC-EQUAL))
(8 8 (:REWRITE DEFAULT-+-1))
)
(CREATE-ST{CORRESPONDENCE})
(CREATE-ST{PRESERVED})
(MISC{CORRESPONDENCE})
(UPDATE-MISC{CORRESPONDENCE}-LEMMA
(506 506 (:REWRITE DEFAULT-CAR))
(311 311 (:REWRITE DEFAULT-+-2))
(311 311 (:REWRITE DEFAULT-+-1))
(78 78 (:REWRITE DEFAULT-<-2))
(78 78 (:REWRITE DEFAULT-<-1))
)
(UPDATE-MISC{CORRESPONDENCE}
(220 220 (:REWRITE DEFAULT-CAR))
(182 182 (:REWRITE DEFAULT-CDR))
(80 40 (:REWRITE DEFAULT-+-2))
(70 14 (:DEFINITION ASSOC-EQUAL))
(40 40 (:REWRITE DEFAULT-+-1))
(39 39 (:REWRITE DEFAULT-<-2))
(39 39 (:REWRITE DEFAULT-<-1))
)
(UPDATE-MISC{PRESERVED}
(67 67 (:REWRITE DEFAULT-CAR))
(65 65 (:REWRITE DEFAULT-CDR))
(38 19 (:REWRITE DEFAULT-+-2))
(27 27 (:REWRITE DEFAULT-<-2))
(27 27 (:REWRITE DEFAULT-<-1))
(19 19 (:REWRITE DEFAULT-+-1))
)
(CORR-MEM-MEMI
(209 209 (:REWRITE DEFAULT-CAR))
(166 166 (:REWRITE DEFAULT-CDR))
(88 88 (:REWRITE DEFAULT-+-2))
(88 88 (:REWRITE DEFAULT-+-1))
(63 63 (:REWRITE DEFAULT-<-2))
(63 63 (:REWRITE DEFAULT-<-1))
(2 2 (:REWRITE NTH-0-CONS))
)
(LOOKUP{CORRESPONDENCE})
(LOOKUP{GUARD-THM})
(ASSOC-EQUAL-PUT-ASSOC-EQUAL
(229 165 (:REWRITE DEFAULT-CAR))
(81 67 (:REWRITE DEFAULT-CDR))
)
(MEM$CP-UPDATE-NTH
(49 25 (:REWRITE DEFAULT-CAR))
(35 28 (:REWRITE DEFAULT-<-2))
(28 28 (:REWRITE DEFAULT-<-1))
(26 14 (:REWRITE DEFAULT-CDR))
(17 10 (:REWRITE DEFAULT-+-2))
(10 10 (:REWRITE DEFAULT-+-1))
(5 5 (:REWRITE ZP-OPEN))
)
(MAP$AP-PUT-ASSOC-EQUAL
(122 107 (:REWRITE DEFAULT-CAR))
(46 46 (:REWRITE DEFAULT-<-2))
(46 46 (:REWRITE DEFAULT-<-1))
(40 37 (:REWRITE DEFAULT-CDR))
)
(CORR-MEM-UPDATE-MEMI
(1564 1564 (:REWRITE DEFAULT-CDR))
(1425 1425 (:REWRITE DEFAULT-CAR))
(969 682 (:REWRITE DEFAULT-+-2))
(682 682 (:REWRITE DEFAULT-+-1))
(510 510 (:REWRITE DEFAULT-<-2))
(510 510 (:REWRITE DEFAULT-<-1))
)
(UPDATE{CORRESPONDENCE}
(51 51 (:REWRITE DEFAULT-CAR))
(49 49 (:REWRITE DEFAULT-CDR))
(36 19 (:REWRITE DEFAULT-+-2))
(24 24 (:REWRITE DEFAULT-<-2))
(24 24 (:REWRITE DEFAULT-<-1))
(19 19 (:REWRITE DEFAULT-+-1))
(12 2 (:DEFINITION PUT-ASSOC-EQUAL))
(4 2 (:DEFINITION TRUE-LISTP))
)
(UPDATE{PRESERVED}
(875 695 (:REWRITE DEFAULT-CAR))
(440 404 (:REWRITE DEFAULT-CDR))
(311 311 (:REWRITE DEFAULT-<-2))
(311 311 (:REWRITE DEFAULT-<-1))
(108 54 (:REWRITE DEFAULT-+-2))
(54 54 (:REWRITE DEFAULT-+-1))
(3 1 (:DEFINITION UPDATE-NTH))
)
(UPDATE{GUARD-THM})
(MEM$CI-UPDATE-MEM$CI
(18 4 (:DEFINITION UPDATE-NTH))
(14 14 (:REWRITE DEFAULT-CAR))
(12 12 (:REWRITE DEFAULT-CDR))
(10 2 (:DEFINITION LEN))
(9 9 (:REWRITE DEFAULT-<-2))
(9 9 (:REWRITE DEFAULT-<-1))
(8 6 (:REWRITE DEFAULT-+-2))
(6 6 (:REWRITE DEFAULT-+-1))
(6 1 (:DEFINITION MEM$CP))
(4 4 (:REWRITE ZP-OPEN))
(2 1 (:DEFINITION TRUE-LISTP))
)
(MEM$CI-UPDATE-MEM$CI-FAILURE)
(LOOKUP-UPDATE
(10 10 (:REWRITE DEFAULT-CDR))
(10 10 (:REWRITE DEFAULT-CAR))
(10 2 (:DEFINITION ASSOC-EQUAL))
(6 1 (:DEFINITION PUT-ASSOC-EQUAL))
(4 2 (:DEFINITION NTH))
(3 1 (:DEFINITION UPDATE-NTH))
)
(FOO)
|
