YES
Time: 0.082026
TRS:
{ u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
din der der X -> u41(din der X, X),
din der plus(X, Y) -> u21(din der X, X, Y),
din der times(X, Y) -> u31(din der X, X, Y),
u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
u41(dout DX, X) -> u42(din der DX, X, DX),
u42(dout DDX, X, DX) -> dout DDX}
DP:
DP:
{ u21#(dout DX, X, Y) -> din# der Y,
u21#(dout DX, X, Y) -> u22#(din der Y, X, Y, DX),
din# der der X -> din# der X,
din# der der X -> u41#(din der X, X),
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X,
din# der times(X, Y) -> din# der X,
din# der times(X, Y) -> u31#(din der X, X, Y),
u31#(dout DX, X, Y) -> din# der Y,
u31#(dout DX, X, Y) -> u32#(din der Y, X, Y, DX),
u41#(dout DX, X) -> din# der DX,
u41#(dout DX, X) -> u42#(din der DX, X, DX)}
TRS:
{ u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
din der der X -> u41(din der X, X),
din der plus(X, Y) -> u21(din der X, X, Y),
din der times(X, Y) -> u31(din der X, X, Y),
u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
u41(dout DX, X) -> u42(din der DX, X, DX),
u42(dout DDX, X, DX) -> dout DDX}
UR:
{ u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
din der der X -> u41(din der X, X),
din der plus(X, Y) -> u21(din der X, X, Y),
din der times(X, Y) -> u31(din der X, X, Y),
u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
u41(dout DX, X) -> u42(din der DX, X, DX),
u42(dout DDX, X, DX) -> dout DDX,
a(x, y) -> x,
a(x, y) -> y}
EDG:
{(din# der times(X, Y) -> u31#(din der X, X, Y), u31#(dout DX, X, Y) -> u32#(din der Y, X, Y, DX))
(din# der times(X, Y) -> u31#(din der X, X, Y), u31#(dout DX, X, Y) -> din# der Y)
(din# der der X -> u41#(din der X, X), u41#(dout DX, X) -> u42#(din der DX, X, DX))
(din# der der X -> u41#(din der X, X), u41#(dout DX, X) -> din# der DX)
(u21#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> u31#(din der X, X, Y))
(u21#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> din# der X)
(u21#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> din# der X)
(u21#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> u21#(din der X, X, Y))
(u21#(dout DX, X, Y) -> din# der Y, din# der der X -> u41#(din der X, X))
(u21#(dout DX, X, Y) -> din# der Y, din# der der X -> din# der X)
(din# der der X -> din# der X, din# der times(X, Y) -> u31#(din der X, X, Y))
(din# der der X -> din# der X, din# der times(X, Y) -> din# der X)
(din# der der X -> din# der X, din# der plus(X, Y) -> din# der X)
(din# der der X -> din# der X, din# der plus(X, Y) -> u21#(din der X, X, Y))
(din# der der X -> din# der X, din# der der X -> u41#(din der X, X))
(din# der der X -> din# der X, din# der der X -> din# der X)
(din# der times(X, Y) -> din# der X, din# der times(X, Y) -> u31#(din der X, X, Y))
(din# der times(X, Y) -> din# der X, din# der times(X, Y) -> din# der X)
(din# der times(X, Y) -> din# der X, din# der plus(X, Y) -> din# der X)
(din# der times(X, Y) -> din# der X, din# der plus(X, Y) -> u21#(din der X, X, Y))
(din# der times(X, Y) -> din# der X, din# der der X -> u41#(din der X, X))
(din# der times(X, Y) -> din# der X, din# der der X -> din# der X)
(din# der plus(X, Y) -> din# der X, din# der der X -> din# der X)
(din# der plus(X, Y) -> din# der X, din# der der X -> u41#(din der X, X))
(din# der plus(X, Y) -> din# der X, din# der plus(X, Y) -> u21#(din der X, X, Y))
(din# der plus(X, Y) -> din# der X, din# der plus(X, Y) -> din# der X)
(din# der plus(X, Y) -> din# der X, din# der times(X, Y) -> din# der X)
(din# der plus(X, Y) -> din# der X, din# der times(X, Y) -> u31#(din der X, X, Y))
(u31#(dout DX, X, Y) -> din# der Y, din# der der X -> din# der X)
(u31#(dout DX, X, Y) -> din# der Y, din# der der X -> u41#(din der X, X))
(u31#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> u21#(din der X, X, Y))
(u31#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> din# der X)
(u31#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> din# der X)
(u31#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> u31#(din der X, X, Y))
(u41#(dout DX, X) -> din# der DX, din# der der X -> din# der X)
(u41#(dout DX, X) -> din# der DX, din# der der X -> u41#(din der X, X))
(u41#(dout DX, X) -> din# der DX, din# der plus(X, Y) -> u21#(din der X, X, Y))
(u41#(dout DX, X) -> din# der DX, din# der plus(X, Y) -> din# der X)
(u41#(dout DX, X) -> din# der DX, din# der times(X, Y) -> din# der X)
(u41#(dout DX, X) -> din# der DX, din# der times(X, Y) -> u31#(din der X, X, Y))
(din# der plus(X, Y) -> u21#(din der X, X, Y), u21#(dout DX, X, Y) -> din# der Y)
(din# der plus(X, Y) -> u21#(din der X, X, Y), u21#(dout DX, X, Y) -> u22#(din der Y, X, Y, DX))}
STATUS:
arrows: 0.708333
SCCS (1):
Scc:
{ u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der der X -> u41#(din der X, X),
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X,
din# der times(X, Y) -> din# der X,
din# der times(X, Y) -> u31#(din der X, X, Y),
u31#(dout DX, X, Y) -> din# der Y,
u41#(dout DX, X) -> din# der DX}
SCC (9):
Strict:
{ u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der der X -> u41#(din der X, X),
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X,
din# der times(X, Y) -> din# der X,
din# der times(X, Y) -> u31#(din der X, X, Y),
u31#(dout DX, X, Y) -> din# der Y,
u41#(dout DX, X) -> din# der DX}
Weak:
{ u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
din der der X -> u41(din der X, X),
din der plus(X, Y) -> u21(din der X, X, Y),
din der times(X, Y) -> u31(din der X, X, Y),
u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
u41(dout DX, X) -> u42(din der DX, X, DX),
u42(dout DDX, X, DX) -> dout DDX}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[u22](x0, x1, x2, x3) = x0,
[u32](x0, x1, x2, x3) = x0,
[u21](x0, x1, x2) = 0,
[u31](x0, x1, x2) = 0,
[u42](x0, x1, x2) = x0,
[plus](x0, x1) = 0,
[times](x0, x1) = 0,
[u41](x0, x1) = 0,
[din](x0) = 0,
[der](x0) = 0,
[dout](x0) = 1,
[u21#](x0, x1, x2) = 1,
[u31#](x0, x1, x2) = 1,
[u41#](x0, x1) = x0 + 1,
[din#](x0) = 1
Strict:
u41#(dout DX, X) -> din# der DX
2 + 0X + 0DX >= 1 + 0DX
u31#(dout DX, X, Y) -> din# der Y
1 + 0X + 0Y + 0DX >= 1 + 0Y
din# der times(X, Y) -> u31#(din der X, X, Y)
1 + 0X + 0Y >= 1 + 0X + 0Y
din# der times(X, Y) -> din# der X
1 + 0X + 0Y >= 1 + 0X
din# der plus(X, Y) -> din# der X
1 + 0X + 0Y >= 1 + 0X
din# der plus(X, Y) -> u21#(din der X, X, Y)
1 + 0X + 0Y >= 1 + 0X + 0Y
din# der der X -> u41#(din der X, X)
1 + 0X >= 1 + 0X
din# der der X -> din# der X
1 + 0X >= 1 + 0X
u21#(dout DX, X, Y) -> din# der Y
1 + 0X + 0Y + 0DX >= 1 + 0Y
Weak:
u42(dout DDX, X, DX) -> dout DDX
1 + 0X + 0DX + 0DDX >= 1 + 0DDX
u41(dout DX, X) -> u42(din der DX, X, DX)
0 + 0X + 0DX >= 0 + 0X + 0DX
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
1 + 0X + 0Y + 0DX + 0DY >= 1 + 0X + 0Y + 0DX + 0DY
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
1 + 0X + 0Y + 0DX + 0DY >= 1 + 0DX + 0DY
din der times(X, Y) -> u31(din der X, X, Y)
0 + 0X + 0Y >= 0 + 0X + 0Y
din der plus(X, Y) -> u21(din der X, X, Y)
0 + 0X + 0Y >= 0 + 0X + 0Y
din der der X -> u41(din der X, X)
0 + 0X >= 0 + 0X
u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
SCCS (1):
Scc:
{ u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X,
din# der times(X, Y) -> din# der X,
din# der times(X, Y) -> u31#(din der X, X, Y),
u31#(dout DX, X, Y) -> din# der Y}
SCC (7):
Strict:
{ u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X,
din# der times(X, Y) -> din# der X,
din# der times(X, Y) -> u31#(din der X, X, Y),
u31#(dout DX, X, Y) -> din# der Y}
Weak:
{ u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
din der der X -> u41(din der X, X),
din der plus(X, Y) -> u21(din der X, X, Y),
din der times(X, Y) -> u31(din der X, X, Y),
u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
u41(dout DX, X) -> u42(din der DX, X, DX),
u42(dout DDX, X, DX) -> dout DDX}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[u22](x0, x1, x2, x3) = x0,
[u32](x0, x1, x2, x3) = x0 + 1,
[u21](x0, x1, x2) = 0,
[u31](x0, x1, x2) = x0,
[u42](x0, x1, x2) = x0,
[plus](x0, x1) = x0,
[times](x0, x1) = 0,
[u41](x0, x1) = 0,
[din](x0) = 0,
[der](x0) = 0,
[dout](x0) = x0 + 1,
[u21#](x0, x1, x2) = 0,
[u31#](x0, x1, x2) = x0,
[din#](x0) = 0
Strict:
u31#(dout DX, X, Y) -> din# der Y
1 + 0X + 0Y + 1DX >= 0 + 0Y
din# der times(X, Y) -> u31#(din der X, X, Y)
0 + 0X + 0Y >= 0 + 0X + 0Y
din# der times(X, Y) -> din# der X
0 + 0X + 0Y >= 0 + 0X
din# der plus(X, Y) -> din# der X
0 + 0X + 0Y >= 0 + 0X
din# der plus(X, Y) -> u21#(din der X, X, Y)
0 + 0X + 0Y >= 0 + 0X + 0Y
din# der der X -> din# der X
0 + 0X >= 0 + 0X
u21#(dout DX, X, Y) -> din# der Y
0 + 0X + 0Y + 0DX >= 0 + 0Y
Weak:
u42(dout DDX, X, DX) -> dout DDX
1 + 0X + 0DX + 1DDX >= 1 + 1DDX
u41(dout DX, X) -> u42(din der DX, X, DX)
0 + 0X + 0DX >= 0 + 0X + 0DX
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
2 + 0X + 0Y + 0DX + 1DY >= 1 + 0X + 0Y + 0DX + 0DY
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
1 + 0X + 0Y + 1DX >= 1 + 0X + 0Y + 0DX
u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
1 + 0X + 0Y + 0DX + 1DY >= 1 + 0DX + 1DY
din der times(X, Y) -> u31(din der X, X, Y)
0 + 0X + 0Y >= 0 + 0X + 0Y
din der plus(X, Y) -> u21(din der X, X, Y)
0 + 0X + 0Y >= 0 + 0X + 0Y
din der der X -> u41(din der X, X)
0 + 0X >= 0 + 0X
u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
SCCS (1):
Scc:
{ u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X,
din# der times(X, Y) -> din# der X}
SCC (5):
Strict:
{ u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X,
din# der times(X, Y) -> din# der X}
Weak:
{ u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
din der der X -> u41(din der X, X),
din der plus(X, Y) -> u21(din der X, X, Y),
din der times(X, Y) -> u31(din der X, X, Y),
u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
u41(dout DX, X) -> u42(din der DX, X, DX),
u42(dout DDX, X, DX) -> dout DDX}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[u22](x0, x1, x2, x3) = x0 + x1,
[u32](x0, x1, x2, x3) = x0 + x1,
[u21](x0, x1, x2) = x0 + x1,
[u31](x0, x1, x2) = x0 + x1,
[u42](x0, x1, x2) = x0 + x1,
[plus](x0, x1) = x0 + x1,
[times](x0, x1) = x0 + 1,
[u41](x0, x1) = x0 + x1,
[din](x0) = x0,
[der](x0) = x0,
[dout](x0) = 0,
[u21#](x0, x1, x2) = x0,
[din#](x0) = x0
Strict:
din# der times(X, Y) -> din# der X
1 + 1X + 0Y >= 0 + 1X
din# der plus(X, Y) -> din# der X
0 + 1X + 1Y >= 0 + 1X
din# der plus(X, Y) -> u21#(din der X, X, Y)
0 + 1X + 1Y >= 0 + 0X + 1Y
din# der der X -> din# der X
0 + 1X >= 0 + 1X
u21#(dout DX, X, Y) -> din# der Y
0 + 0X + 1Y + 0DX >= 0 + 1Y
Weak:
u42(dout DDX, X, DX) -> dout DDX
0 + 0X + 1DX + 0DDX >= 0 + 0DDX
u41(dout DX, X) -> u42(din der DX, X, DX)
0 + 1X + 0DX >= 0 + 0X + 2DX
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
0 + 0X + 1Y + 0DX + 0DY >= 0 + 0X + 0Y + 0DX + 0DY
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
0 + 1X + 0Y + 0DX >= 0 + 0X + 2Y + 0DX
u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
0 + 0X + 1Y + 0DX + 0DY >= 0 + 0DX + 0DY
din der times(X, Y) -> u31(din der X, X, Y)
1 + 1X + 0Y >= 0 + 2X + 0Y
din der plus(X, Y) -> u21(din der X, X, Y)
0 + 1X + 1Y >= 0 + 2X + 0Y
din der der X -> u41(din der X, X)
0 + 1X >= 0 + 2X
u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
0 + 1X + 0Y + 0DX >= 0 + 0X + 2Y + 0DX
SCCS (1):
Scc:
{u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X}
SCC (4):
Strict:
{u21#(dout DX, X, Y) -> din# der Y,
din# der der X -> din# der X,
din# der plus(X, Y) -> u21#(din der X, X, Y),
din# der plus(X, Y) -> din# der X}
Weak:
{ u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
din der der X -> u41(din der X, X),
din der plus(X, Y) -> u21(din der X, X, Y),
din der times(X, Y) -> u31(din der X, X, Y),
u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
u41(dout DX, X) -> u42(din der DX, X, DX),
u42(dout DDX, X, DX) -> dout DDX}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[u22](x0, x1, x2, x3) = 0,
[u32](x0, x1, x2, x3) = 0,
[u21](x0, x1, x2) = x0 + 1,
[u31](x0, x1, x2) = 0,
[u42](x0, x1, x2) = 0,
[plus](x0, x1) = x0 + x1 + 1,
[times](x0, x1) = 0,
[u41](x0, x1) = 0,
[din](x0) = 0,
[der](x0) = x0 + 1,
[dout](x0) = 1,
[u21#](x0, x1, x2) = x0 + 1,
[din#](x0) = x0
Strict:
din# der plus(X, Y) -> din# der X
2 + 1X + 1Y >= 1 + 1X
din# der plus(X, Y) -> u21#(din der X, X, Y)
2 + 1X + 1Y >= 1 + 0X + 1Y
din# der der X -> din# der X
2 + 1X >= 1 + 1X
u21#(dout DX, X, Y) -> din# der Y
1 + 0X + 1Y + 0DX >= 1 + 1Y
Weak:
u42(dout DDX, X, DX) -> dout DDX
0 + 0X + 0DX + 0DDX >= 1 + 0DDX
u41(dout DX, X) -> u42(din der DX, X, DX)
0 + 0X + 0DX >= 0 + 0X + 0DX
u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
0 + 0X + 0Y + 0DX + 0DY >= 1 + 0X + 0Y + 0DX + 0DY
u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
0 + 0X + 0Y + 0DX + 0DY >= 1 + 0DX + 0DY
din der times(X, Y) -> u31(din der X, X, Y)
0 + 0X + 0Y >= 0 + 0X + 0Y
din der plus(X, Y) -> u21(din der X, X, Y)
0 + 0X + 0Y >= 1 + 0X + 0Y
din der der X -> u41(din der X, X)
0 + 0X >= 0 + 0X
u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
2 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
SCCS (0):