YES
TRS:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
DP:
Strict:
{ h#(ok(X)) -> h#(X),
active#(h(d())) -> g#(c()),
active#(g(X)) -> h#(X),
g#(ok(X)) -> g#(X),
proper#(h(X)) -> h#(proper(X)),
proper#(h(X)) -> proper#(X),
proper#(g(X)) -> g#(proper(X)),
proper#(g(X)) -> proper#(X),
top#(mark(X)) -> proper#(X),
top#(mark(X)) -> top#(proper(X)),
top#(ok(X)) -> active#(X),
top#(ok(X)) -> top#(active(X))}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
EDG:
{(h#(ok(X)) -> h#(X), h#(ok(X)) -> h#(X))
(g#(ok(X)) -> g#(X), g#(ok(X)) -> g#(X))
(proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
(proper#(g(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
(proper#(g(X)) -> proper#(X), proper#(h(X)) -> proper#(X))
(proper#(g(X)) -> proper#(X), proper#(h(X)) -> h#(proper(X)))
(top#(ok(X)) -> active#(X), active#(g(X)) -> h#(X))
(top#(ok(X)) -> active#(X), active#(h(d())) -> g#(c()))
(proper#(g(X)) -> g#(proper(X)), g#(ok(X)) -> g#(X))
(top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
(top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
(top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
(top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
(top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
(top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
(top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
(top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
(proper#(h(X)) -> h#(proper(X)), h#(ok(X)) -> h#(X))
(top#(mark(X)) -> proper#(X), proper#(h(X)) -> h#(proper(X)))
(top#(mark(X)) -> proper#(X), proper#(h(X)) -> proper#(X))
(top#(mark(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
(top#(mark(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
(proper#(h(X)) -> proper#(X), proper#(h(X)) -> h#(proper(X)))
(proper#(h(X)) -> proper#(X), proper#(h(X)) -> proper#(X))
(proper#(h(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
(proper#(h(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
(active#(g(X)) -> h#(X), h#(ok(X)) -> h#(X))}
SCCS:
Scc:
{top#(mark(X)) -> top#(proper(X)),
top#(ok(X)) -> top#(active(X))}
Scc:
{proper#(h(X)) -> proper#(X),
proper#(g(X)) -> proper#(X)}
Scc:
{g#(ok(X)) -> g#(X)}
Scc:
{h#(ok(X)) -> h#(X)}
SCC:
Strict:
{top#(mark(X)) -> top#(proper(X)),
top#(ok(X)) -> top#(active(X))}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
BOUND:
Bound: match(-raise)-DP-bounded by 4
Automaton:
{ top#_4(184) -> 185*
top#_3(142) -> 143*
top#_2(59) -> 60*
top#_1(26) -> 27*
top#_0(23) -> 24*
top#_0(22) -> 11*
top_0(22) -> 19*
top_0(21) -> 19*
top_0(20) -> 19*
top_0(19) -> 19*
top_0(18) -> 19*
top_0(16) -> 19*
top_0(15) -> 19*
top_0(14) -> 19*
top_0(13) -> 19*
ok_4(192) -> 193*
ok_4(189) -> 190*
ok_3(176) -> 177*
ok_3(171) -> 172*
ok_3(164) -> 165*
ok_2(145) -> 146*
ok_2(134) -> 135*
ok_2(127) -> 128*
ok_2(109) -> 110*
ok_2(75) -> 76*
ok_1(69) -> 70*
ok_1(62) -> 63*
ok_1(48) -> 49*
ok_1(44) -> 45*
ok_0(22) -> 18*
ok_0(21) -> 18*
ok_0(20) -> 18*
ok_0(19) -> 18*
ok_0(18) -> 18*
ok_0(16) -> 18*
ok_0(15) -> 18*
ok_0(14) -> 18*
ok_0(13) -> 18*
proper_4(186) -> 187*
proper_4(183) -> 184*
proper_3(159) -> 160*
proper_3(149) -> 150*
proper_3(141) -> 142*
proper_2(122) -> 123*
proper_2(120) -> 121*
proper_2(118) -> 119*
proper_2(115) -> 116*
proper_2(113) -> 114*
proper_2(111) -> 112*
proper_2(105) -> 106*
proper_2(102) -> 103*
proper_2(96) -> 97*
proper_2(82) -> 83*
proper_2(58) -> 59*
proper_1(42) -> 43*
proper_1(40) -> 41*
proper_1(38) -> 39*
proper_1(36) -> 37*
proper_1(34) -> 35*
proper_1(32) -> 33*
proper_1(30) -> 31*
proper_1(28) -> 29*
proper_1(25) -> 26*
proper_0(22) -> 22*
proper_0(21) -> 22*
proper_0(20) -> 22*
proper_0(19) -> 22*
proper_0(18) -> 22*
proper_0(16) -> 22*
proper_0(15) -> 22*
proper_0(14) -> 22*
proper_0(13) -> 22*
c_4() -> 189*
c_3() -> 164*
c_2() -> 109*
c_1() -> 48*
c_0() -> 21*
d_2() -> 75*
d_1() -> 44*
d_0() -> 20*
g_3(175) -> 176*
g_3(162) -> 163*
g_2(168) -> 169*
g_2(157) -> 158*
g_2(155) -> 156*
g_2(144) -> 145*
g_2(133) -> 134*
g_2(124) -> 125*
g_2(107) -> 108*
g_1(92) -> 93*
g_1(90) -> 91*
g_1(73) -> 74*
g_1(68) -> 69*
g_1(54) -> 55*
g_0(22) -> 16*
g_0(21) -> 16*
g_0(20) -> 16*
g_0(19) -> 16*
g_0(18) -> 16*
g_0(16) -> 16*
g_0(15) -> 16*
g_0(14) -> 16*
g_0(13) -> 16*
active_4(194) -> 195*
active_3(178) -> 179*
active_3(173) -> 174*
active_2(136) -> 137*
active_2(129) -> 130*
active_2(77) -> 78*
active_1(71) -> 72*
active_1(64) -> 65*
active_1(50) -> 51*
active_1(46) -> 47*
active_0(22) -> 15*
active_0(21) -> 15*
active_0(20) -> 15*
active_0(19) -> 15*
active_0(18) -> 15*
active_0(16) -> 15*
active_0(15) -> 15*
active_0(14) -> 15*
active_0(13) -> 15*
h_4(191) -> 192*
h_4(187) -> 188*
h_3(180) -> 181*
h_3(170) -> 171*
h_3(160) -> 161*
h_2(166) -> 167*
h_2(153) -> 154*
h_2(151) -> 152*
h_2(138) -> 139*
h_2(131) -> 132*
h_2(126) -> 127*
h_2(116) -> 117*
h_2(103) -> 104*
h_1(100) -> 101*
h_1(98) -> 99*
h_1(88) -> 89*
h_1(86) -> 87*
h_1(84) -> 85*
h_1(79) -> 80*
h_1(66) -> 67*
h_1(61) -> 62*
h_1(52) -> 53*
h_0(22) -> 14*
h_0(21) -> 14*
h_0(20) -> 14*
h_0(19) -> 14*
h_0(18) -> 14*
h_0(16) -> 14*
h_0(15) -> 14*
h_0(14) -> 14*
h_0(13) -> 14*
mark_3(181) -> 182*
mark_2(147) -> 148*
mark_2(139) -> 140*
mark_1(94) -> 95*
mark_1(80) -> 81*
mark_1(56) -> 57*
mark_0(22) -> 13*
mark_0(21) -> 13*
mark_0(20) -> 13*
mark_0(19) -> 13*
mark_0(18) -> 13*
mark_0(16) -> 13*
mark_0(15) -> 13*
mark_0(14) -> 13*
mark_0(13) -> 13*
195 -> 184*
193 -> 188*
192 -> 194*
190 -> 187*
189 -> 191*
188 -> 184*
185 -> 143*
182 -> 179*
181 -> 183*
180 -> 186*
179 -> 142*
177 -> 163*
176 -> 178*
175 -> 180*
174 -> 142*
172 -> 161*
171 -> 173*
169 -> 145*
167 -> 127*
165 -> 160*
164 -> 175 | 170
163 -> 150*
161 -> 142*
160 -> 162*
158 -> 145*
156 -> 145*
154 -> 127*
152 -> 127*
150 -> 142*
148 -> 130*
147 -> 149*
146 -> 125*
145 -> 157 | 153
143 -> 60*
140 -> 137*
139 -> 141*
138 -> 159*
137 -> 59*
135 -> 125 | 108
134 -> 155 | 151 | 147 | 136
133 -> 138*
132 -> 127*
130 -> 59*
128 -> 117 | 104
127 -> 168 | 166 | 129
125 -> 123 | 114
123 -> 116*
121 -> 116*
119 -> 116*
117 -> 121 | 112
114 -> 103*
112 -> 103*
110 -> 119 | 106
109 -> 133 | 131
108 -> 97*
106 -> 107 | 103
104 -> 83*
103 -> 124*
101 -> 80*
100 -> 113*
99 -> 80*
98 -> 111*
97 -> 59*
95 -> 65*
94 -> 96*
93 -> 69*
92 -> 100*
91 -> 69*
90 -> 98*
89 -> 62*
88 -> 122*
87 -> 62*
86 -> 120*
85 -> 80*
84 -> 105*
83 -> 59*
81 -> 72*
80 -> 82*
79 -> 102*
78 -> 59*
76 -> 116 | 103 | 59
75 -> 144 | 126 | 77
74 -> 94 | 69
73 -> 84*
72 -> 26*
70 -> 55*
69 -> 92 | 88 | 71
68 -> 79*
67 -> 62*
66 -> 118*
65 -> 26*
63 -> 53*
62 -> 90 | 86 | 64
61 -> 115*
60 -> 27*
57 -> 51*
56 -> 58*
55 -> 43 | 33
53 -> 43 | 29
51 -> 26*
49 -> 41*
48 -> 73 | 66 | 50
47 -> 26*
45 -> 39*
44 -> 68 | 61 | 56 | 46
43 -> 26*
41 -> 26*
39 -> 26*
37 -> 26*
35 -> 26*
33 -> 26*
31 -> 26*
29 -> 26*
27 -> 24*
26 -> 54 | 52
24 -> 11*
22 -> 42*
21 -> 40*
20 -> 38*
19 -> 36*
18 -> 34 | 22 | 16 | 14
16 -> 32 | 22
15 -> 30 | 23
14 -> 28 | 22
13 -> 25 | 15}
Strict:
{top#(ok(X)) -> top#(active(X))}
EDG:
{(top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))}
SCCS:
Scc:
{top#(ok(X)) -> top#(active(X))}
SCC:
Strict:
{top#(ok(X)) -> top#(active(X))}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
POLY:
Argument Filtering:
pi(top#) = 0, pi(top) = [], pi(ok) = [0], pi(proper) = [], pi(c) = [], pi(d) = [], pi(g) = [], pi(active) = [], pi(h) = [], pi(mark) = []
Usable Rules:
{}
Interpretation:
[ok](x0) = x0 + 1,
[active] = 0
Strict:
{}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
Qed
SCC:
Strict:
{proper#(h(X)) -> proper#(X),
proper#(g(X)) -> proper#(X)}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
SPSC:
Simple Projection:
pi(proper#) = 0
Strict:
{proper#(g(X)) -> proper#(X)}
EDG:
{(proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))}
SCCS:
Scc:
{proper#(g(X)) -> proper#(X)}
SCC:
Strict:
{proper#(g(X)) -> proper#(X)}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
SPSC:
Simple Projection:
pi(proper#) = 0
Strict:
{}
Qed
SCC:
Strict:
{g#(ok(X)) -> g#(X)}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
SPSC:
Simple Projection:
pi(g#) = 0
Strict:
{}
Qed
SCC:
Strict:
{h#(ok(X)) -> h#(X)}
Weak:
{ h(ok(X)) -> ok(h(X)),
active(h(d())) -> mark(g(c())),
active(g(X)) -> mark(h(X)),
active(c()) -> mark(d()),
g(ok(X)) -> ok(g(X)),
proper(h(X)) -> h(proper(X)),
proper(g(X)) -> g(proper(X)),
proper(d()) -> ok(d()),
proper(c()) -> ok(c()),
top(mark(X)) -> top(proper(X)),
top(ok(X)) -> top(active(X))}
SPSC:
Simple Projection:
pi(h#) = 0
Strict:
{}
Qed