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
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
|
(INSERT-TEXT
(42 1 (:DEFINITION MAKE-CHARACTER-LIST))
(32 2 (:REWRITE TAKE-OF-LEN-FREE))
(25 5 (:DEFINITION LEN))
(23 1 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(22 4 (:DEFINITION CHARACTER-LISTP))
(22 1 (:DEFINITION TAKE))
(18 12 (:REWRITE DEFAULT-CDR))
(13 7 (:REWRITE DEFAULT-+-2))
(10 7 (:REWRITE DEFAULT-CAR))
(9 6 (:REWRITE DEFAULT-<-1))
(9 3 (:REWRITE NFIX-WHEN-ZP))
(7 7 (:REWRITE DEFAULT-+-1))
(6 6 (:REWRITE DEFAULT-<-2))
(6 4 (:REWRITE CONSP-OF-TAKE))
(5 5 (:LINEAR POSITION-WHEN-MEMBER))
(5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(4 4 (:TYPE-PRESCRIPTION ZP))
(4 4 (:REWRITE ZP-OPEN))
(3 3 (:REWRITE DEFAULT-COERCE-2))
(3 3 (:REWRITE DEFAULT-COERCE-1))
(2 2 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
)
(INSERT-TEXT-CORRECTNESS-1
(271 6 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(185 3 (:DEFINITION NTHCDR))
(161 15 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(134 5 (:DEFINITION MAKE-CHARACTER-LIST))
(132 13 (:REWRITE ZP-OPEN))
(124 8 (:REWRITE NFIX-WHEN-ZP))
(107 15 (:DEFINITION CHARACTER-LISTP))
(98 18 (:DEFINITION LEN))
(69 51 (:REWRITE DEFAULT-CDR))
(63 4 (:REWRITE TAKE-OF-LEN-FREE))
(52 28 (:REWRITE DEFAULT-<-2))
(52 28 (:REWRITE DEFAULT-+-2))
(38 28 (:REWRITE DEFAULT-<-1))
(36 30 (:REWRITE DEFAULT-CAR))
(30 5 (:REWRITE LEN-OF-MAKE-CHARACTER-LIST))
(29 1 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(28 28 (:REWRITE DEFAULT-+-1))
(18 8 (:REWRITE NFIX-WHEN-NATP))
(16 6 (:DEFINITION BINARY-APPEND))
(14 14 (:LINEAR POSITION-WHEN-MEMBER))
(14 14 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(13 13 (:TYPE-PRESCRIPTION TAKE))
(10 10 (:TYPE-PRESCRIPTION ZP))
(10 4 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(10 3 (:REWRITE COMMUTATIVITY-OF-+))
(6 6 (:REWRITE DEFAULT-COERCE-2))
(6 6 (:REWRITE DEFAULT-COERCE-1))
(6 4 (:REWRITE CONSP-OF-TAKE))
(4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
(3 3 (:REWRITE LENGTH-WHEN-STRINGP))
(3 1 (:DEFINITION NATP))
(2 2 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(2 2 (:TYPE-PRESCRIPTION LENGTH))
(1 1 (:TYPE-PRESCRIPTION NATP))
(1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(1 1 (:REWRITE FOLD-CONSTS-IN-+))
)
(INSERT-TEXT-CORRECTNESS-2
(1029 9 (:REWRITE LEN-OF-NTHCDR))
(619 45 (:REWRITE ZP-OPEN))
(581 70 (:DEFINITION LEN))
(536 7 (:REWRITE LEN-OF-APPEND))
(341 128 (:REWRITE DEFAULT-CDR))
(289 146 (:REWRITE DEFAULT-+-2))
(249 131 (:REWRITE DEFAULT-<-2))
(237 85 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(234 24 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(203 8 (:DEFINITION MAKE-CHARACTER-LIST))
(195 131 (:REWRITE DEFAULT-<-1))
(195 12 (:DEFINITION NATP))
(171 146 (:REWRITE DEFAULT-+-1))
(136 22 (:DEFINITION CHARACTER-LISTP))
(122 49 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(92 1 (:REWRITE CAR-OF-NTHCDR))
(85 85 (:TYPE-PRESCRIPTION BINARY-APPEND))
(80 48 (:REWRITE DEFAULT-CAR))
(77 2 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
(69 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
(61 61 (:LINEAR POSITION-WHEN-MEMBER))
(61 61 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(54 28 (:REWRITE DEFAULT-UNARY-MINUS))
(47 1 (:DEFINITION NTH))
(44 4 (:REWRITE COMMUTATIVITY-2-OF-+))
(41 41 (:REWRITE DEFAULT-COERCE-2))
(38 38 (:TYPE-PRESCRIPTION ZP))
(35 1 (:REWRITE CONSP-OF-NTHCDR))
(32 4 (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+))
(29 1 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(28 28 (:TYPE-PRESCRIPTION LENGTH))
(21 21 (:REWRITE FOLD-CONSTS-IN-+))
(12 12 (:TYPE-PRESCRIPTION NATP))
(8 8 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
(7 7 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(6 4 (:REWRITE CONSP-OF-TAKE))
(3 3 (:REWRITE LENGTH-WHEN-STRINGP))
(1 1 (:REWRITE MAKE-CHARACTER-LIST-MAKES-CHARACTER-LIST))
)
(INSERT-TEXT-CORRECTNESS-3
(271 6 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(253 17 (:REWRITE NFIX-WHEN-ZP))
(229 17 (:REWRITE ZP-OPEN))
(185 3 (:DEFINITION NTHCDR))
(181 31 (:DEFINITION LEN))
(161 15 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(134 5 (:DEFINITION MAKE-CHARACTER-LIST))
(126 62 (:REWRITE DEFAULT-+-2))
(92 46 (:REWRITE DEFAULT-<-2))
(88 14 (:DEFINITION CHARACTER-LISTP))
(82 46 (:REWRITE DEFAULT-<-1))
(81 63 (:REWRITE DEFAULT-CDR))
(73 62 (:REWRITE DEFAULT-+-1))
(63 4 (:REWRITE TAKE-OF-LEN-FREE))
(35 35 (:TYPE-PRESCRIPTION MAKE-CHARACTER-LIST))
(35 29 (:REWRITE DEFAULT-CAR))
(29 1 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(27 27 (:LINEAR POSITION-WHEN-MEMBER))
(27 27 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(16 6 (:DEFINITION BINARY-APPEND))
(15 15 (:TYPE-PRESCRIPTION ZP))
(13 13 (:TYPE-PRESCRIPTION TAKE))
(13 5 (:REWRITE DEFAULT-UNARY-MINUS))
(11 11 (:REWRITE DEFAULT-COERCE-2))
(11 11 (:REWRITE DEFAULT-COERCE-1))
(10 4 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(6 6 (:REWRITE FOLD-CONSTS-IN-+))
(6 4 (:REWRITE CONSP-OF-TAKE))
(4 4 (:TYPE-PRESCRIPTION NATP))
(4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
(3 3 (:REWRITE LENGTH-WHEN-STRINGP))
(2 2 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(2 2 (:TYPE-PRESCRIPTION LENGTH))
(2 2 (:TYPE-PRESCRIPTION INSERT-TEXT))
(1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(1 1 (:REWRITE MAKE-CHARACTER-LIST-MAKES-CHARACTER-LIST))
(1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
)
(LEN-OF-INSERT-TEXT
(235 6 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(208 18 (:REWRITE NFIX-WHEN-ZP))
(200 32 (:DEFINITION LEN))
(188 18 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(183 17 (:REWRITE ZP-OPEN))
(161 3 (:DEFINITION NTHCDR))
(157 6 (:DEFINITION MAKE-CHARACTER-LIST))
(138 64 (:REWRITE DEFAULT-+-2))
(106 17 (:DEFINITION CHARACTER-LISTP))
(87 69 (:REWRITE DEFAULT-CDR))
(80 49 (:REWRITE DEFAULT-<-2))
(76 64 (:REWRITE DEFAULT-+-1))
(72 49 (:REWRITE DEFAULT-<-1))
(63 6 (:DEFINITION NATP))
(63 4 (:REWRITE TAKE-OF-LEN-FREE))
(40 34 (:REWRITE DEFAULT-CAR))
(39 39 (:TYPE-PRESCRIPTION MAKE-CHARACTER-LIST))
(37 37 (:LINEAR POSITION-WHEN-MEMBER))
(37 37 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(29 1 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(20 8 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(16 6 (:DEFINITION BINARY-APPEND))
(15 15 (:TYPE-PRESCRIPTION ZP))
(13 13 (:TYPE-PRESCRIPTION TAKE))
(11 11 (:REWRITE DEFAULT-COERCE-2))
(11 11 (:REWRITE DEFAULT-COERCE-1))
(9 5 (:REWRITE DEFAULT-UNARY-MINUS))
(8 8 (:TYPE-PRESCRIPTION BINARY-APPEND))
(6 6 (:TYPE-PRESCRIPTION NATP))
(6 6 (:REWRITE FOLD-CONSTS-IN-+))
(6 4 (:REWRITE CONSP-OF-TAKE))
(5 1 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
(4 4 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(4 4 (:TYPE-PRESCRIPTION LENGTH))
(1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(1 1 (:REWRITE MAKE-CHARACTER-LIST-MAKES-CHARACTER-LIST))
)
(INSERT-TEXT-CORRECTNESS-4
(523 12 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(426 18 (:REWRITE TAKE-OF-LEN-FREE))
(382 59 (:DEFINITION CHARACTER-LISTP))
(279 31 (:REWRITE ZP-OPEN))
(273 114 (:REWRITE DEFAULT-+-2))
(260 182 (:REWRITE DEFAULT-CDR))
(166 80 (:REWRITE DEFAULT-<-2))
(149 7 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(145 103 (:REWRITE DEFAULT-CAR))
(125 80 (:REWRITE DEFAULT-<-1))
(119 114 (:REWRITE DEFAULT-+-1))
(94 94 (:LINEAR POSITION-WHEN-MEMBER))
(94 94 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(49 49 (:REWRITE DEFAULT-COERCE-2))
(49 49 (:REWRITE DEFAULT-COERCE-1))
(34 3 (:DEFINITION NATP))
(3 3 (:TYPE-PRESCRIPTION NATP))
(2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(2 2 (:REWRITE DEFAULT-UNARY-MINUS))
(1 1 (:REWRITE FOLD-CONSTS-IN-+))
)
(TRUE-LISTP-OF-INSERT-TEXT)
|
