YES
Time: 4.209611
TRS:
{ f(x, f(y, z)) -> f(f(x, y), z),
f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
DP:
DP:
{ f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z),
f#(f(a(), a()), x) -> f#(a(), x),
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
TRS:
{ f(x, f(y, z)) -> f(f(x, y), z),
f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
EDG:
{(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), x))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), x))
(f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
(f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))}
SCCS (1):
Scc:
{ f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z),
f#(f(a(), a()), x) -> f#(a(), x),
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
SCC (5):
Strict:
{ f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z),
f#(f(a(), a()), x) -> f#(a(), x),
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
Weak:
{ f(x, f(y, z)) -> f(f(x, y), z),
f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1) = x0,
[a] = 1,
[b] = 0,
[f#](x0, x1) = x0
Strict:
f#(f(a(), a()), x) -> f#(b(), f(a(), x))
1 + 0x >= 0 + 0x
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))
1 + 0x >= 1 + 0x
f#(f(a(), a()), x) -> f#(a(), x)
1 + 0x >= 1 + 0x
f#(x, f(y, z)) -> f#(f(x, y), z)
0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
f#(x, f(y, z)) -> f#(x, y)
0 + 1x + 0y + 0z >= 0 + 1x + 0y
Weak:
EDG:
{(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), x))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), x))
(f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))}
SCCS (1):
Scc:
{ f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z),
f#(f(a(), a()), x) -> f#(a(), x),
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
SCC (4):
Strict:
{ f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z),
f#(f(a(), a()), x) -> f#(a(), x),
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
Weak:
{ f(x, f(y, z)) -> f(f(x, y), z),
f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1) = x0 + x1,
[a] = 1,
[b] = 0,
[f#](x0, x1) = x0 + x1
Strict:
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))
2 + 1x >= 2 + 1x
f#(f(a(), a()), x) -> f#(a(), x)
2 + 1x >= 1 + 1x
f#(x, f(y, z)) -> f#(f(x, y), z)
0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
f#(x, f(y, z)) -> f#(x, y)
0 + 1x + 1y + 1z >= 0 + 1x + 1y
Weak:
EDG:
{(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
(f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))}
SCCS (1):
Scc:
{ f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z),
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
SCC (3):
Strict:
{ f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z),
f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
Weak:
{ f(x, f(y, z)) -> f(f(x, y), z),
f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
BOUND:
Bound: match(-raise)-DP-bounded by 1
Automaton:
{ b_1() -> 14*
b_0() -> 10*
a_1() -> 13*
a_0() -> 9*
f#_1(19, 21) -> 5*
f#_1(19, 20) -> 5*
f#_1(19, 16) -> 5*
f#_1(19, 14) -> 5*
f#_1(19, 12) -> 5*
f#_1(19, 11) -> 5*
f#_1(19, 10) -> 5*
f#_1(19, 9) -> 5*
f#_1(19, 8) -> 5*
f#_1(18, 21) -> 5*
f#_1(18, 20) -> 5*
f#_1(18, 16) -> 5*
f#_1(18, 14) -> 5*
f#_1(18, 12) -> 5*
f#_1(18, 11) -> 5*
f#_1(18, 10) -> 5*
f#_1(18, 9) -> 5*
f#_1(18, 8) -> 5*
f#_1(17, 19) -> 5*
f#_1(17, 18) -> 5*
f#_1(17, 17) -> 5*
f#_1(17, 15) -> 5*
f#_1(17, 13) -> 5*
f#_1(13, 21) -> 5*
f#_1(13, 20) -> 5*
f#_1(13, 16) -> 5*
f#_1(13, 14) -> 5*
f#_0(11, 12) -> 5*
f#_0(11, 11) -> 5*
f#_0(11, 10) -> 5*
f#_0(11, 9) -> 5*
f#_0(11, 8) -> 5*
f#_0(9, 12) -> 5*
f#_0(9, 11) -> 5*
f#_0(9, 10) -> 5*
f#_0(9, 9) -> 5*
f#_0(9, 8) -> 5*
f#_0(8, 12) -> 5*
f#_0(8, 11) -> 5*
f#_0(8, 10) -> 5*
f#_0(8, 9) -> 5*
f#_0(8, 8) -> 5*
f_1(21, 21) -> 20*
f_1(21, 20) -> 20*
f_1(21, 16) -> 20*
f_1(21, 14) -> 14*
f_1(21, 12) -> 20*
f_1(21, 11) -> 20*
f_1(21, 10) -> 20*
f_1(21, 9) -> 20*
f_1(21, 8) -> 20*
f_1(20, 21) -> 20*
f_1(20, 20) -> 20*
f_1(20, 16) -> 20 | 16
f_1(20, 14) -> 14*
f_1(20, 12) -> 20 | 16
f_1(20, 11) -> 20 | 16
f_1(20, 10) -> 20 | 16
f_1(20, 9) -> 20 | 16
f_1(20, 8) -> 20 | 16
f_1(19, 21) -> 19*
f_1(19, 20) -> 19*
f_1(19, 16) -> 19 | 15
f_1(19, 14) -> 17*
f_1(19, 12) -> 19 | 15
f_1(19, 11) -> 19 | 15
f_1(19, 10) -> 19 | 15
f_1(19, 9) -> 19 | 15
f_1(19, 8) -> 19 | 15
f_1(18, 21) -> 19*
f_1(18, 20) -> 19*
f_1(18, 16) -> 19*
f_1(18, 14) -> 17*
f_1(18, 12) -> 19*
f_1(18, 11) -> 19*
f_1(18, 10) -> 19*
f_1(18, 9) -> 19*
f_1(18, 8) -> 19*
f_1(17, 19) -> 19*
f_1(17, 18) -> 19 | 18
f_1(17, 17) -> 17*
f_1(17, 15) -> 19 | 15
f_1(17, 13) -> 19 | 18
f_1(16, 12) -> 16*
f_1(16, 11) -> 16*
f_1(16, 10) -> 16*
f_1(16, 9) -> 16*
f_1(16, 8) -> 16*
f_1(15, 12) -> 15*
f_1(15, 11) -> 15*
f_1(15, 10) -> 15*
f_1(15, 9) -> 15*
f_1(15, 8) -> 15*
f_1(14, 19) -> 20*
f_1(14, 18) -> 21 | 20
f_1(14, 17) -> 14*
f_1(14, 15) -> 20 | 16
f_1(14, 13) -> 21 | 20
f_1(13, 21) -> 19*
f_1(13, 20) -> 19*
f_1(13, 16) -> 19 | 15
f_1(13, 14) -> 17*
f_1(13, 12) -> 15*
f_1(13, 11) -> 15*
f_1(13, 10) -> 15*
f_1(13, 9) -> 15*
f_1(13, 8) -> 15*
f_0(12, 12) -> 12 | 8
f_0(12, 11) -> 12 | 8
f_0(12, 10) -> 12 | 8
f_0(12, 9) -> 12 | 8
f_0(12, 8) -> 12 | 8
f_0(11, 12) -> 11 | 8
f_0(11, 11) -> 11 | 8
f_0(11, 10) -> 11 | 8
f_0(11, 9) -> 11 | 8
f_0(11, 8) -> 11 | 8
f_0(10, 12) -> 8*
f_0(10, 11) -> 12*
f_0(10, 10) -> 8*
f_0(10, 9) -> 8*
f_0(10, 8) -> 8*
f_0(9, 12) -> 11 | 8
f_0(9, 11) -> 11*
f_0(9, 10) -> 11*
f_0(9, 9) -> 11*
f_0(9, 8) -> 11*
f_0(8, 12) -> 12 | 8
f_0(8, 11) -> 12 | 8
f_0(8, 10) -> 12 | 8
f_0(8, 9) -> 12 | 8
f_0(8, 8) -> 12 | 8}
Strict:
{f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z)}
EDG:
{(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
(f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))}
SCCS (1):
Scc:
{f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z)}
SCC (2):
Strict:
{f#(x, f(y, z)) -> f#(x, y),
f#(x, f(y, z)) -> f#(f(x, y), z)}
Weak:
{ f(x, f(y, z)) -> f(f(x, y), z),
f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
SPSC:
Simple Projection:
pi(f#) = 1
Strict:
{f#(x, f(y, z)) -> f#(f(x, y), z)}
EDG:
{(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))}
SCCS (1):
Scc:
{f#(x, f(y, z)) -> f#(f(x, y), z)}
SCC (1):
Strict:
{f#(x, f(y, z)) -> f#(f(x, y), z)}
Weak:
{ f(x, f(y, z)) -> f(f(x, y), z),
f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
SPSC:
Simple Projection:
pi(f#) = 1
Strict:
{}
Qed