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
|
(GENERATE-INDEX-LIST)
(GENERATE-INDEX-LIST-CORRECTNESS-1
(9 3 (:DEFINITION NATP))
(6 6 (:REWRITE DEFAULT-<-2))
(6 6 (:REWRITE DEFAULT-<-1))
(6 4 (:REWRITE DEFAULT-+-2))
(5 4 (:REWRITE DEFAULT-CDR))
(5 4 (:REWRITE DEFAULT-CAR))
(4 4 (:REWRITE ZP-OPEN))
(4 4 (:REWRITE DEFAULT-+-1))
(2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
)
(GENERATE-INDEX-LIST-CORRECTNESS-2
(20 13 (:REWRITE DEFAULT-+-2))
(13 13 (:REWRITE DEFAULT-+-1))
(10 9 (:REWRITE DEFAULT-<-1))
(9 9 (:REWRITE DEFAULT-<-2))
(6 5 (:REWRITE DEFAULT-CDR))
(4 4 (:REWRITE ZP-OPEN))
(4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
)
(MEMBER-OF-GENERATE-INDEX-LIST
(513 315 (:REWRITE DEFAULT-+-2))
(419 398 (:REWRITE DEFAULT-<-1))
(404 398 (:REWRITE DEFAULT-<-2))
(361 315 (:REWRITE DEFAULT-+-1))
(273 273 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(79 52 (:REWRITE DEFAULT-CAR))
(75 50 (:REWRITE DEFAULT-CDR))
)
(REMOVE-WHEN-ABSENT
(13 13 (:REWRITE DEFAULT-CAR))
(8 8 (:REWRITE DEFAULT-CDR))
)
(LEN-OF-TRUE-LIST-FIX
(14 7 (:REWRITE DEFAULT-+-2))
(9 8 (:REWRITE DEFAULT-CDR))
(7 7 (:REWRITE DEFAULT-+-1))
(3 3 (:REWRITE DEFAULT-CAR))
)
(GENERATE-INDEX-LIST-CORRECTNESS-4
(168 18 (:DEFINITION MEMBER-EQUAL))
(126 12 (:REWRITE COMMUTATIVITY-2-OF-+))
(116 109 (:REWRITE DEFAULT-+-2))
(109 109 (:REWRITE DEFAULT-<-2))
(109 109 (:REWRITE DEFAULT-<-1))
(109 109 (:REWRITE DEFAULT-+-1))
(53 48 (:REWRITE DEFAULT-CDR))
(46 41 (:REWRITE DEFAULT-CAR))
(32 23 (:REWRITE ZP-OPEN))
(20 4 (:DEFINITION TRUE-LIST-FIX))
(12 6 (:REWRITE UNICITY-OF-0))
(6 6 (:DEFINITION FIX))
(2 2 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
)
|
