YES
Time: 0.100298
TRS:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
DP:
DP:
{ f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)),
f#(s x, s y, s z) -> f#(s x, s y, z),
f#(s x, s y, 0()) -> f#(x, y, s 0()),
f#(s x, 0(), s z) -> f#(x, s 0(), z),
f#(s 0(), y, z) -> f#(0(), s y, s z),
f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)),
f#(0(), s s y, s s z) -> f#(0(), s s y, s z),
f#(0(), s s y, s 0()) -> f#(0(), y, s 0()),
f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)}
TRS:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
UR:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z,
a(w, v) -> w,
a(w, v) -> v}
EDG:
{(f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
(f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s 0(), y, z) -> f#(0(), s y, s z))
(f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, 0()) -> f#(x, y, s 0()))
(f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, s z) -> f#(s x, s y, z))
(f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
(f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
(f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s 0(), y, z) -> f#(0(), s y, s z))
(f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, 0(), s z) -> f#(x, s 0(), z))
(f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, s y, s z) -> f#(s x, s y, z))
(f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s 0(), y, z) -> f#(0(), s y, s z))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, 0(), s z) -> f#(x, s 0(), z))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, 0()) -> f#(x, y, s 0()))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(s x, s y, z))
(f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
(f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
(f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
(f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
(f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
(f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
(f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
(f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
(f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)))
(f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s s z) -> f#(0(), s s y, s z))
(f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
(f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
(f#(0(), s s y, s 0()) -> f#(0(), y, s 0()), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()))
(f#(0(), s 0(), s s z) -> f#(0(), s 0(), z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z))
(f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)))
(f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, s z) -> f#(s x, s y, z))
(f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, 0()) -> f#(x, y, s 0()))
(f#(s x, s y, s z) -> f#(s x, s y, z), f#(s 0(), y, z) -> f#(0(), s y, s z))}
STATUS:
arrows: 0.555556
SCCS (4):
Scc:
{f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)),
f#(s x, s y, s z) -> f#(s x, s y, z),
f#(s x, s y, 0()) -> f#(x, y, s 0()),
f#(s x, 0(), s z) -> f#(x, s 0(), z)}
Scc:
{f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)),
f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
Scc:
{f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)}
Scc:
{f#(0(), s s y, s 0()) -> f#(0(), y, s 0())}
SCC (4):
Strict:
{f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)),
f#(s x, s y, s z) -> f#(s x, s y, z),
f#(s x, s y, 0()) -> f#(x, y, s 0()),
f#(s x, 0(), s z) -> f#(x, s 0(), z)}
Weak:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1, x2) = 0,
[s](x0) = x0 + 1,
[0] = 0,
[f#](x0, x1, x2) = x0 + 1
Strict:
f#(s x, 0(), s z) -> f#(x, s 0(), z)
2 + 1x + 0z >= 1 + 1x + 0z
f#(s x, s y, 0()) -> f#(x, y, s 0())
2 + 1x + 0y >= 1 + 1x + 0y
f#(s x, s y, s z) -> f#(s x, s y, z)
2 + 1x + 0y + 0z >= 2 + 1x + 0y + 0z
f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z))
2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z
Weak:
f(0(), 0(), z) -> s z
0 + 0z >= 1 + 1z
f(0(), s 0(), s 0()) -> s s 0()
0 >= 2
f(0(), s 0(), s s z) -> f(0(), s 0(), z)
0 + 0z >= 0 + 0z
f(0(), s s y, s 0()) -> f(0(), y, s 0())
0 + 0y >= 0 + 0y
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z))
0 + 0y + 0z >= 0 + 0y + 0z
f(0(), y, 0()) -> s y
0 + 0y >= 1 + 1y
f(s 0(), y, z) -> f(0(), s y, s z)
0 + 0y + 0z >= 0 + 0y + 0z
f(s x, 0(), s z) -> f(x, s 0(), z)
0 + 0x + 0z >= 0 + 0x + 0z
f(s x, s y, 0()) -> f(x, y, s 0())
0 + 0x + 0y >= 0 + 0x + 0y
f(s x, s y, s z) -> f(x, y, f(s x, s y, z))
0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
f(x, 0(), 0()) -> s x
0 + 0x >= 1 + 1x
SCCS (1):
Scc:
{f#(s x, s y, s z) -> f#(s x, s y, z)}
SCC (1):
Strict:
{f#(s x, s y, s z) -> f#(s x, s y, z)}
Weak:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1, x2) = x0 + x1 + 1,
[s](x0) = x0 + 1,
[0] = 1,
[f#](x0, x1, x2) = x0 + 1
Strict:
f#(s x, s y, s z) -> f#(s x, s y, z)
2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z
Weak:
f(0(), 0(), z) -> s z
2 + 1z >= 1 + 1z
f(0(), s 0(), s 0()) -> s s 0()
4 >= 3
f(0(), s 0(), s s z) -> f(0(), s 0(), z)
4 + 1z >= 2 + 1z
f(0(), s s y, s 0()) -> f(0(), y, s 0())
4 + 0y >= 4 + 0y
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z))
4 + 0y + 1z >= 5 + 0y + 1z
f(0(), y, 0()) -> s y
3 + 0y >= 1 + 1y
f(s 0(), y, z) -> f(0(), s y, s z)
3 + 0y + 1z >= 3 + 0y + 1z
f(s x, 0(), s z) -> f(x, s 0(), z)
3 + 1x + 1z >= 1 + 1x + 1z
f(s x, s y, 0()) -> f(x, y, s 0())
3 + 1x + 0y >= 3 + 1x + 0y
f(s x, s y, s z) -> f(x, y, f(s x, s y, z))
3 + 1x + 0y + 1z >= 3 + 2x + 0y + 1z
f(x, 0(), 0()) -> s x
2 + 1x >= 1 + 1x
Qed
SCC (2):
Strict:
{f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)),
f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
Weak:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1, x2) = 0,
[s](x0) = x0 + 1,
[0] = 0,
[f#](x0, x1, x2) = x0
Strict:
f#(0(), s s y, s s z) -> f#(0(), s s y, s z)
2 + 1y + 0z >= 2 + 1y + 0z
f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z))
2 + 1y + 0z >= 0 + 1y + 0z
Weak:
f(0(), 0(), z) -> s z
0 + 0z >= 1 + 1z
f(0(), s 0(), s 0()) -> s s 0()
0 >= 2
f(0(), s 0(), s s z) -> f(0(), s 0(), z)
0 + 0z >= 0 + 0z
f(0(), s s y, s 0()) -> f(0(), y, s 0())
0 + 0y >= 0 + 0y
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z))
0 + 0y + 0z >= 0 + 0y + 0z
f(0(), y, 0()) -> s y
0 + 0y >= 1 + 1y
f(s 0(), y, z) -> f(0(), s y, s z)
0 + 0y + 0z >= 0 + 0y + 0z
f(s x, 0(), s z) -> f(x, s 0(), z)
0 + 0x + 0z >= 0 + 0x + 0z
f(s x, s y, 0()) -> f(x, y, s 0())
0 + 0x + 0y >= 0 + 0x + 0y
f(s x, s y, s z) -> f(x, y, f(s x, s y, z))
0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
f(x, 0(), 0()) -> s x
0 + 0x >= 1 + 1x
SCCS (1):
Scc:
{f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
SCC (1):
Strict:
{f#(0(), s s y, s s z) -> f#(0(), s s y, s z)}
Weak:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1, x2) = x0 + x1,
[s](x0) = x0 + 1,
[0] = 1,
[f#](x0, x1, x2) = x0 + x1 + x2 + 1
Strict:
f#(0(), s s y, s s z) -> f#(0(), s s y, s z)
6 + 1y + 1z >= 5 + 1y + 1z
Weak:
f(0(), 0(), z) -> s z
1 + 1z >= 1 + 1z
f(0(), s 0(), s 0()) -> s s 0()
3 >= 3
f(0(), s 0(), s s z) -> f(0(), s 0(), z)
3 + 1z >= 1 + 1z
f(0(), s s y, s 0()) -> f(0(), y, s 0())
3 + 0y >= 3 + 0y
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z))
3 + 0y + 1z >= 3 + 0y + 1z
f(0(), y, 0()) -> s y
2 + 0y >= 1 + 1y
f(s 0(), y, z) -> f(0(), s y, s z)
2 + 0y + 1z >= 2 + 0y + 1z
f(s x, 0(), s z) -> f(x, s 0(), z)
2 + 1x + 1z >= 0 + 1x + 1z
f(s x, s y, 0()) -> f(x, y, s 0())
2 + 1x + 0y >= 2 + 1x + 0y
f(s x, s y, s z) -> f(x, y, f(s x, s y, z))
2 + 1x + 0y + 1z >= 1 + 2x + 0y + 1z
f(x, 0(), 0()) -> s x
1 + 1x >= 1 + 1x
Qed
SCC (1):
Strict:
{f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)}
Weak:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1, x2) = x0 + x1 + 1,
[s](x0) = x0 + 1,
[0] = 1,
[f#](x0, x1, x2) = x0 + x1
Strict:
f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)
3 + 1z >= 1 + 1z
Weak:
f(0(), 0(), z) -> s z
2 + 1z >= 1 + 1z
f(0(), s 0(), s 0()) -> s s 0()
4 >= 3
f(0(), s 0(), s s z) -> f(0(), s 0(), z)
4 + 1z >= 2 + 1z
f(0(), s s y, s 0()) -> f(0(), y, s 0())
4 + 0y >= 4 + 0y
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z))
4 + 0y + 1z >= 5 + 0y + 1z
f(0(), y, 0()) -> s y
3 + 0y >= 1 + 1y
f(s 0(), y, z) -> f(0(), s y, s z)
3 + 0y + 1z >= 3 + 0y + 1z
f(s x, 0(), s z) -> f(x, s 0(), z)
3 + 1x + 1z >= 1 + 1x + 1z
f(s x, s y, 0()) -> f(x, y, s 0())
3 + 1x + 0y >= 3 + 1x + 0y
f(s x, s y, s z) -> f(x, y, f(s x, s y, z))
3 + 1x + 0y + 1z >= 3 + 2x + 0y + 1z
f(x, 0(), 0()) -> s x
2 + 1x >= 1 + 1x
Qed
SCC (1):
Strict:
{f#(0(), s s y, s 0()) -> f#(0(), y, s 0())}
Weak:
{ f(x, 0(), 0()) -> s x,
f(s x, s y, s z) -> f(x, y, f(s x, s y, z)),
f(s x, s y, 0()) -> f(x, y, s 0()),
f(s x, 0(), s z) -> f(x, s 0(), z),
f(s 0(), y, z) -> f(0(), s y, s z),
f(0(), y, 0()) -> s y,
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)),
f(0(), s s y, s 0()) -> f(0(), y, s 0()),
f(0(), s 0(), s s z) -> f(0(), s 0(), z),
f(0(), s 0(), s 0()) -> s s 0(),
f(0(), 0(), z) -> s z}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[f](x0, x1, x2) = x0 + x1 + x2 + 1,
[s](x0) = x0 + 1,
[0] = 1,
[f#](x0, x1, x2) = x0
Strict:
f#(0(), s s y, s 0()) -> f#(0(), y, s 0())
2 + 1y >= 0 + 1y
Weak:
f(0(), 0(), z) -> s z
3 + 1z >= 1 + 1z
f(0(), s 0(), s 0()) -> s s 0()
6 >= 3
f(0(), s 0(), s s z) -> f(0(), s 0(), z)
6 + 1z >= 4 + 1z
f(0(), s s y, s 0()) -> f(0(), y, s 0())
6 + 1y >= 4 + 1y
f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z))
6 + 1y + 1z >= 7 + 2y + 1z
f(0(), y, 0()) -> s y
3 + 1y >= 1 + 1y
f(s 0(), y, z) -> f(0(), s y, s z)
3 + 1y + 1z >= 4 + 1y + 1z
f(s x, 0(), s z) -> f(x, s 0(), z)
4 + 1x + 1z >= 3 + 1x + 1z
f(s x, s y, 0()) -> f(x, y, s 0())
4 + 1x + 1y >= 3 + 1x + 1y
f(s x, s y, s z) -> f(x, y, f(s x, s y, z))
4 + 1x + 1y + 1z >= 4 + 2x + 2y + 1z
f(x, 0(), 0()) -> s x
3 + 1x >= 1 + 1x
Qed