YES Time: 0.080187 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} 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))} 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: EDG: {(din# der times(X, Y) -> u31#(din der X, X, Y), u31#(dout DX, X, Y) -> din# der Y) (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)) (din# der plus(X, Y) -> u21#(din der X, X, Y), u21#(dout DX, X, Y) -> din# der Y)} 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: EDG: {(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 -> 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 -> 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 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)) (u21#(dout DX, X, Y) -> din# der Y, din# der der X -> 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 plus(X, Y) -> din# der X) (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 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)} 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: EDG: {(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 -> din# der X) (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 plus(X, Y) -> u21#(din der X, X, Y)) (din# der plus(X, Y) -> din# der X, din# der der X -> din# der X) (din# der der X -> din# der X, din# der der X -> 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 plus(X, Y) -> din# der X) (din# der plus(X, Y) -> u21#(din der X, X, Y), u21#(dout DX, X, Y) -> din# der Y)} 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: EDG: {} SCCS (0): Qed