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
|
(ADE::LIST-REWRITE-1
(45 45 (:REWRITE DEFAULT-CDR))
(37 19 (:REWRITE DEFAULT-+-2))
(21 21 (:REWRITE DEFAULT-CAR))
(19 19 (:REWRITE DEFAULT-+-1))
(18 18 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
(ADE::LIST-REWRITE-2
(116 116 (:REWRITE DEFAULT-CDR))
(83 42 (:REWRITE DEFAULT-+-2))
(68 68 (:REWRITE DEFAULT-CAR))
(42 42 (:REWRITE DEFAULT-+-1))
(22 22 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
(ADE::LIST-REWRITE-4
(465 465 (:REWRITE DEFAULT-CDR))
(202 202 (:REWRITE DEFAULT-CAR))
(174 88 (:REWRITE DEFAULT-+-2))
(88 88 (:REWRITE DEFAULT-+-1))
(26 26 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
(ADE::LIST-REWRITE-5
(700 700 (:REWRITE DEFAULT-CDR))
(270 270 (:REWRITE DEFAULT-CAR))
(212 108 (:REWRITE DEFAULT-+-2))
(108 108 (:REWRITE DEFAULT-+-1))
(27 27 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
(ADE::LIST-REWRITE-10
(2610 2610 (:REWRITE DEFAULT-CDR))
(650 650 (:REWRITE DEFAULT-CAR))
(437 233 (:REWRITE DEFAULT-+-2))
(233 233 (:REWRITE DEFAULT-+-1))
(27 27 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
(ADE::LIST-AS-COLLECTED-NTH)
(ADE::OPEN-LIST-AS-COLLECTED-NTH
(90 7 (:DEFINITION NTH))
(38 27 (:REWRITE DEFAULT-+-2))
(29 11 (:REWRITE ZP-OPEN))
(28 6 (:REWRITE FOLD-CONSTS-IN-+))
(27 27 (:REWRITE DEFAULT-+-1))
(15 15 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(9 9 (:REWRITE DEFAULT-CDR))
(9 9 (:REWRITE DEFAULT-CAR))
(8 8 (:REWRITE DEFAULT-<-2))
(8 8 (:REWRITE DEFAULT-<-1))
(6 2 (:REWRITE UNICITY-OF-0))
(4 2 (:DEFINITION FIX))
)
(ADE::EQUAL-LEN-4-AS-COLLECTED-NTH
(136 136 (:REWRITE DEFAULT-CDR))
(64 64 (:REWRITE DEFAULT-CAR))
(52 26 (:REWRITE DEFAULT-+-2))
(26 26 (:REWRITE DEFAULT-+-1))
(8 8 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
(ADE::EQUAL-LEN-32-AS-COLLECTED-NTH
(6898 6898 (:REWRITE DEFAULT-CDR))
(1464 1464 (:REWRITE DEFAULT-CAR))
(276 138 (:REWRITE DEFAULT-+-2))
(138 138 (:REWRITE DEFAULT-+-1))
(8 8 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
|
