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
|
(UPDATE-MISC1)
(UPDATE-MISC2)
(UPDATE-MISC3)
(UPDATE-MISC4)
(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
(954 954 (:REWRITE DEFAULT-+-2))
(954 954 (:REWRITE DEFAULT-+-1))
(287 287 (:REWRITE DEFAULT-<-2))
(287 287 (:REWRITE DEFAULT-<-1))
(276 138 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
(138 138 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(UPDATE-MISC{CORRESPONDENCE}
(241 237 (:REWRITE DEFAULT-CAR))
(199 199 (:REWRITE DEFAULT-CDR))
(100 50 (:REWRITE DEFAULT-+-2))
(70 14 (:DEFINITION ASSOC-EQUAL))
(50 50 (:REWRITE DEFAULT-+-1))
(36 36 (:REWRITE DEFAULT-<-2))
(36 36 (: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})
|
