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
|
(ADE::BRANCH$DATA-INS-LEN
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(ADE::BRANCH$INS-LEN)
(ADE::BRANCH*
(13 13 (:TYPE-PRESCRIPTION POSP))
)
(ADE::BRANCH*$DESTRUCTURE
(66 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
(60 60 (:TYPE-PRESCRIPTION POSP))
(60 6 (:DEFINITION BINARY-APPEND))
(16 16 (:REWRITE DEFAULT-CDR))
(11 11 (:REWRITE DEFAULT-CAR))
)
(ADE::NOT-PRIMP-BRANCH)
(ADE::BRANCH$NETLIST)
(ADE::BRANCH&)
(ADE::CHECK-BRANCH$NETLIST-64)
(ADE::BRANCH$DATA-IN
(6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
(5 1 (:DEFINITION TRUE-LISTP))
(4 4 (:TYPE-PRESCRIPTION ADE::BVP))
(1 1 (:REWRITE DEFAULT-CDR))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(ADE::LEN-BRANCH$DATA-IN)
(ADE::BRANCH$ACT0
(10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
(5 5 (:TYPE-PRESCRIPTION BOOLEANP))
)
(ADE::BRANCH$ACT0-INACTIVE
(15 3 (:REWRITE ADE::NFIX-OF-NAT))
(14 14 (:REWRITE NTH-WHEN-PREFIXP))
(12 12 (:REWRITE DEFAULT-+-2))
(12 12 (:REWRITE DEFAULT-+-1))
(9 3 (:DEFINITION NATP))
(6 6 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE DEFAULT-<-2))
(6 6 (:REWRITE DEFAULT-<-1))
(6 2 (:REWRITE ADE::F-GATES=B-GATES))
(4 4 (:TYPE-PRESCRIPTION BOOLEANP))
(3 3 (:TYPE-PRESCRIPTION NATP))
)
(ADE::BRANCH$ACT1
(10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
(5 5 (:TYPE-PRESCRIPTION BOOLEANP))
)
(ADE::BRANCH$ACT1-INACTIVE
(15 4 (:REWRITE ADE::F-GATES=B-GATES))
(15 3 (:REWRITE ADE::NFIX-OF-NAT))
(14 14 (:REWRITE NTH-WHEN-PREFIXP))
(12 12 (:REWRITE DEFAULT-+-2))
(12 12 (:REWRITE DEFAULT-+-1))
(9 3 (:DEFINITION NATP))
(8 8 (:TYPE-PRESCRIPTION BOOLEANP))
(6 6 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE DEFAULT-<-2))
(6 6 (:REWRITE DEFAULT-<-1))
(3 3 (:TYPE-PRESCRIPTION NATP))
(3 3 (:TYPE-PRESCRIPTION ADE::F-NOT))
)
(ADE::BRANCH$ACT)
(ADE::BRANCH$ACT-INACTIVE
(8 8 (:REWRITE NTH-WHEN-PREFIXP))
(4 4 (:REWRITE DEFAULT-CAR))
(2 2 (:REWRITE DEFAULT-CDR))
)
(ADE::BRANCH$VALUE
(308 2 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-DISJOINT))
(274 137 (:REWRITE DEFAULT-+-2))
(141 137 (:REWRITE DEFAULT-+-1))
(128 8 (:REWRITE ADE::DISJOINT-ATOM))
(116 23 (:DEFINITION BINARY-APPEND))
(82 8 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
(72 8 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
(72 8 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
(60 4 (:DEFINITION ATOM))
(59 59 (:REWRITE NTH-WHEN-PREFIXP))
(40 2 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
(34 2 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
(32 32 (:TYPE-PRESCRIPTION PAIRLIS$))
(28 28 (:LINEAR LEN-WHEN-PREFIXP))
(27 1 (:REWRITE ADE::BRANCH$ACT-INACTIVE))
(24 10 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(18 18 (:TYPE-PRESCRIPTION ADE::DISJOINT))
(16 8 (:REWRITE DEFAULT-<-2))
(14 14 (:TYPE-PRESCRIPTION ADE::BVP))
(14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
(11 5 (:REWRITE ADE::V-THREEFIX-BVP))
(9 3 (:REWRITE ADE::CAR-V-THREEFIX))
(8 8 (:REWRITE ADE::DISJOINT-SIS-DIFF-SYMS))
(8 8 (:REWRITE DEFAULT-<-1))
(8 4 (:REWRITE DEFAULT-UNARY-MINUS))
(8 2 (:DEFINITION TRUE-LISTP))
(6 6 (:REWRITE ADE::NTHCDR-OF-POS-CONST-IDX))
(6 3 (:DEFINITION ADE::3V-FIX))
(4 2 (:REWRITE PREFIXP-WHEN-PREFIXP))
(3 3 (:TYPE-PRESCRIPTION ADE::3VP))
(2 2 (:REWRITE TAKE-WHEN-ATOM))
(2 2 (:REWRITE PREFIXP-TRANSITIVE . 2))
(2 2 (:REWRITE PREFIXP-TRANSITIVE . 1))
(2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
)
|
