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
|
(ADE::HALF-ADDER&)
(ADE::CHECK-HALF-ADDER)
(ADE::HALF-ADDER$OUTPUTS
(1 1 (:TYPE-PRESCRIPTION ADE::F-XOR))
)
(ADE::HALF-ADDER$VALUE
(48 46 (:REWRITE DEFAULT-CAR))
(28 28 (:REWRITE DEFAULT-CDR))
(15 3 (:DEFINITION ADE::DELETE-TO-EQ))
(13 7 (:REWRITE ADE::F-GATES=B-GATES))
(6 6 (:TYPE-PRESCRIPTION BOOLEANP))
(4 4 (:TYPE-PRESCRIPTION ADE::F-XOR))
)
(ADE::FULL-ADDER&)
(ADE::CHECK-FULL-ADDER)
(ADE::FULL-ADDER$OUTPUTS
(1 1 (:TYPE-PRESCRIPTION ADE::F-XOR))
)
(ADE::FULL-ADDER$VALUE
(585 585 (:REWRITE DEFAULT-CDR))
(551 551 (:REWRITE DEFAULT-CAR))
(160 32 (:DEFINITION ADE::DELETE-TO-EQ))
(65 31 (:REWRITE ADE::F-GATES=B-GATES))
(1 1 (:TYPE-PRESCRIPTION ADE::3VP))
)
(ADE::RIPPLE-ADD-BODY)
(ADE::RIPPLE-ADD*
(20 10 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(10 10 (:TYPE-PRESCRIPTION POSP))
)
(ADE::RIPPLE-ADD*$DESTRUCTURE
(210 105 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(132 24 (:REWRITE APPEND-WHEN-NOT-CONSP))
(120 12 (:DEFINITION BINARY-APPEND))
(105 105 (:TYPE-PRESCRIPTION POSP))
(24 6 (:DEFINITION ADE::RIPPLE-ADD-BODY))
(22 22 (:REWRITE DEFAULT-CDR))
(17 17 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE ZP-OPEN))
(6 6 (:REWRITE DEFAULT-+-2))
(6 6 (:REWRITE DEFAULT-+-1))
)
(ADE::NOT-PRIMP-RIPPLE-ADD)
(ADE::RIPPLE-ADD$NETLIST)
(ADE::RIPPLE-ADD&)
(ADE::CHECK-RIPPLE-ADD$NETLIST-64)
(ADE::RIPPLE-ADD-BODY-INDUCT)
(ADE::RIPPLE-ADD$UNBOUND-IN-BODY-SUM
(12 12 (:TYPE-PRESCRIPTION ADE::RIPPLE-ADD-BODY))
(12 12 (:REWRITE DEFAULT-<-2))
(12 12 (:REWRITE DEFAULT-<-1))
(8 8 (:REWRITE DEFAULT-+-2))
(8 8 (:REWRITE DEFAULT-+-1))
(4 4 (:REWRITE ZP-OPEN))
(3 3 (:REWRITE DEFAULT-CDR))
(3 3 (:REWRITE DEFAULT-CAR))
)
(ADE::RIPPLE-ADD-BODY$VALUE
(341 85 (:REWRITE ADE::F-GATES=B-GATES))
(210 149 (:REWRITE DEFAULT-CDR))
(203 194 (:REWRITE DEFAULT-+-2))
(195 138 (:REWRITE DEFAULT-CAR))
(194 194 (:REWRITE DEFAULT-+-1))
(150 150 (:TYPE-PRESCRIPTION BOOLEANP))
(139 7 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-SE-OCC))
(75 6 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-CONS))
(75 3 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-APPEND))
(69 18 (:REWRITE ZP-OPEN))
(57 51 (:TYPE-PRESCRIPTION ADE::F-XOR))
(57 19 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
(51 51 (:TYPE-PRESCRIPTION ADE::F-AND))
(48 3 (:REWRITE LEN-OF-APPEND))
(36 7 (:REWRITE ADE::FV-ADDER=V-ADDER))
(26 2 (:DEFINITION MEMBER-EQUAL))
(22 11 (:REWRITE ADE::LEN-SIS))
(21 12 (:REWRITE ADE::UNBOUND-IN-BODY-ATOM))
(20 20 (:REWRITE DEFAULT-<-2))
(20 20 (:REWRITE DEFAULT-<-1))
(15 15 (:TYPE-PRESCRIPTION ADE::ALL-UNBOUND-IN-BODY))
(12 12 (:TYPE-PRESCRIPTION ADE::SE))
(11 11 (:REWRITE ADE::NFIX-OF-NAT))
(11 5 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM))
(10 10 (:TYPE-PRESCRIPTION PAIRLIS$))
(10 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(8 2 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(4 4 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
(2 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
)
(ADE::RIPPLE-ADD-BODY$VALUE-M=0
(45 1 (:DEFINITION ADE::SE-OCC))
(28 5 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
(23 5 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(22 11 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(16 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
(16 2 (:DEFINITION BINARY-APPEND))
(11 11 (:TYPE-PRESCRIPTION ADE::SIS))
(11 11 (:TYPE-PRESCRIPTION POSP))
(11 1 (:DEFINITION PAIRLIS$))
(9 9 (:TYPE-PRESCRIPTION LEN))
(9 6 (:REWRITE DEFAULT-CDR))
(8 5 (:REWRITE DEFAULT-CAR))
(6 6 (:TYPE-PRESCRIPTION ADE::SE))
(5 5 (:TYPE-PRESCRIPTION PAIRLIS$))
(5 1 (:DEFINITION LEN))
(4 4 (:LINEAR LEN-WHEN-PREFIXP))
(4 3 (:REWRITE DEFAULT-+-2))
(4 2 (:REWRITE ADE::LEN-SIS))
(4 2 (:REWRITE ADE::FV-ADDER=V-ADDER))
(4 1 (:DEFINITION ADE::RIPPLE-ADD-BODY))
(3 3 (:REWRITE DEFAULT-+-1))
(2 2 (:TYPE-PRESCRIPTION ADE::RIPPLE-ADD-BODY))
(2 2 (:TYPE-PRESCRIPTION BOOLEANP))
(2 2 (:REWRITE ADE::NFIX-OF-NAT))
(2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(1 1 (:REWRITE ZP-OPEN))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(ADE::RIPPLE-ADD$VALUE
(64 4 (:REWRITE ADE::DISJOINT-ATOM))
(49 25 (:REWRITE DEFAULT-+-2))
(49 1 (:DEFINITION ADE::SE-OCC))
(48 14 (:REWRITE APPEND-WHEN-NOT-CONSP))
(48 7 (:DEFINITION BINARY-APPEND))
(41 4 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
(39 5 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
(31 3 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(30 4 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
(30 4 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
(30 2 (:DEFINITION ATOM))
(25 25 (:REWRITE DEFAULT-+-1))
(14 1 (:DEFINITION ADE::RIPPLE-ADD-BODY))
(12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
(12 3 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(11 6 (:REWRITE DEFAULT-<-2))
(11 1 (:DEFINITION MEMBER-EQUAL))
(10 10 (:TYPE-PRESCRIPTION PAIRLIS$))
(8 8 (:TYPE-PRESCRIPTION ADE::BVP))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(8 2 (:DEFINITION TRUE-LISTP))
(8 1 (:REWRITE ZP-OPEN))
(7 6 (:REWRITE DEFAULT-<-1))
(6 6 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(4 2 (:REWRITE ADE::FV-ADDER=V-ADDER))
(4 2 (:REWRITE ADE::ASSOC-EQ-VALUE-CONS-2))
(3 3 (:TYPE-PRESCRIPTION ADE::RIPPLE-ADD-BODY))
(3 3 (:REWRITE DEFAULT-SYMBOL-NAME))
(2 2 (:TYPE-PRESCRIPTION BOOLEANP))
(2 2 (:REWRITE TAKE-WHEN-ATOM))
(2 2 (:REWRITE ADE::NTHCDR-OF-POS-CONST-IDX))
(1 1 (:DEFINITION ADE::OCC-OUTS$INLINE))
(1 1 (:DEFINITION ADE::OCC-NAME$INLINE))
(1 1 (:DEFINITION ADE::OCC-INS$INLINE))
(1 1 (:DEFINITION ADE::OCC-FN$INLINE))
)
(ADE::RIPPLE-ADD$VALUE-CORRECT
(75 37 (:REWRITE DEFAULT-+-2))
(47 37 (:REWRITE DEFAULT-+-1))
(23 23 (:REWRITE DEFAULT-CDR))
(12 12 (:LINEAR LEN-WHEN-PREFIXP))
(12 3 (:DEFINITION BINARY-APPEND))
(6 6 (:REWRITE FOLD-CONSTS-IN-+))
(6 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
(6 6 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(6 3 (:REWRITE DEFAULT-<-1))
(3 3 (:REWRITE DEFAULT-CAR))
(3 3 (:REWRITE DEFAULT-<-2))
)
|
