YES Time: 0.232551 TRS: { plus(0(), Y) -> Y, plus(s X, Y) -> s plus(X, Y), min(X, 0()) -> X, min(s X, s Y) -> min(X, Y), min(min(X, Y), Z()) -> min(X, plus(Y, Z())), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(min(X, Y), s Y)} DP: DP: { plus#(s X, Y) -> plus#(X, Y), min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z()), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), quot#(s X, s Y) -> min#(X, Y), quot#(s X, s Y) -> quot#(min(X, Y), s Y)} TRS: { plus(0(), Y) -> Y, plus(s X, Y) -> s plus(X, Y), min(X, 0()) -> X, min(s X, s Y) -> min(X, Y), min(min(X, Y), Z()) -> min(X, plus(Y, Z())), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(min(X, Y), s Y)} EDG: {(min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))) (min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z())) (min#(s X, s Y) -> min#(X, Y), min#(s X, s Y) -> min#(X, Y)) (quot#(s X, s Y) -> quot#(min(X, Y), s Y), quot#(s X, s Y) -> quot#(min(X, Y), s Y)) (quot#(s X, s Y) -> quot#(min(X, Y), s Y), quot#(s X, s Y) -> min#(X, Y)) (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))) (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> plus#(Y, Z())) (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(s X, s Y) -> min#(X, Y)) (min#(min(X, Y), Z()) -> plus#(Y, Z()), plus#(s X, Y) -> plus#(X, Y)) (quot#(s X, s Y) -> min#(X, Y), min#(s X, s Y) -> min#(X, Y)) (quot#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z())) (quot#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))) (plus#(s X, Y) -> plus#(X, Y), plus#(s X, Y) -> plus#(X, Y))} STATUS: arrows: 0.638889 SCCS (3): Scc: {quot#(s X, s Y) -> quot#(min(X, Y), s Y)} Scc: { min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))} Scc: {plus#(s X, Y) -> plus#(X, Y)} SCC (1): Strict: {quot#(s X, s Y) -> quot#(min(X, Y), s Y)} Weak: { plus(0(), Y) -> Y, plus(s X, Y) -> s plus(X, Y), min(X, 0()) -> X, min(s X, s Y) -> min(X, Y), min(min(X, Y), Z()) -> min(X, plus(Y, Z())), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(min(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = 0, [min](x0, x1) = x0, [quot](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 0, [Z] = 0, [quot#](x0, x1) = x0 + 1 Strict: quot#(s X, s Y) -> quot#(min(X, Y), s Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: quot(s X, s Y) -> s quot(min(X, Y), s Y) 2 + 1Y + 0X >= 3 + 1Y + 0X quot(0(), s Y) -> 0() 2 + 1Y >= 0 min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 0 + 0Y + 1X >= 0 + 0Y + 1X min(s X, s Y) -> min(X, Y) 1 + 0Y + 1X >= 0 + 0Y + 1X min(X, 0()) -> X 0 + 1X >= 1X plus(s X, Y) -> s plus(X, Y) 0 + 0Y + 0X >= 1 + 0Y + 0X plus(0(), Y) -> Y 0 + 0Y >= 1Y Qed SCC (2): Strict: { min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))} Weak: { plus(0(), Y) -> Y, plus(s X, Y) -> s plus(X, Y), min(X, 0()) -> X, min(s X, s Y) -> min(X, Y), min(min(X, Y), Z()) -> min(X, plus(Y, Z())), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(min(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = 0, [min](x0, x1) = x0 + x1 + 1, [quot](x0, x1) = 0, [s](x0) = x0, [0] = 1, [Z] = 0, [min#](x0, x1) = x0 Strict: min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())) 1 + 1Y + 1X >= 0 + 0Y + 1X min#(s X, s Y) -> min#(X, Y) 0 + 0Y + 1X >= 0 + 0Y + 1X Weak: quot(s X, s Y) -> s quot(min(X, Y), s Y) 0 + 0Y + 0X >= 0 + 0Y + 0X quot(0(), s Y) -> 0() 0 + 0Y >= 1 min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 2 + 1Y + 1X >= 1 + 0Y + 1X min(s X, s Y) -> min(X, Y) 1 + 1Y + 1X >= 1 + 1Y + 1X min(X, 0()) -> X 2 + 1X >= 1X plus(s X, Y) -> s plus(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X plus(0(), Y) -> Y 0 + 0Y >= 1Y SCCS (1): Scc: {min#(s X, s Y) -> min#(X, Y)} SCC (1): Strict: {min#(s X, s Y) -> min#(X, Y)} Weak: { plus(0(), Y) -> Y, plus(s X, Y) -> s plus(X, Y), min(X, 0()) -> X, min(s X, s Y) -> min(X, Y), min(min(X, Y), Z()) -> min(X, plus(Y, Z())), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(min(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + 1, [min](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [Z] = 1, [min#](x0, x1) = x0 + 1 Strict: min#(s X, s Y) -> min#(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: quot(s X, s Y) -> s quot(min(X, Y), s Y) 2 + 1Y + 0X >= 3 + 1Y + 0X quot(0(), s Y) -> 0() 2 + 1Y >= 1 min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 2 + 0Y + 0X >= 2 + 1Y + 0X min(s X, s Y) -> min(X, Y) 2 + 1Y + 0X >= 1 + 1Y + 0X min(X, 0()) -> X 2 + 0X >= 1X plus(s X, Y) -> s plus(X, Y) 2 + 0Y + 1X >= 2 + 0Y + 1X plus(0(), Y) -> Y 2 + 0Y >= 1Y Qed SCC (1): Strict: {plus#(s X, Y) -> plus#(X, Y)} Weak: { plus(0(), Y) -> Y, plus(s X, Y) -> s plus(X, Y), min(X, 0()) -> X, min(s X, s Y) -> min(X, Y), min(min(X, Y), Z()) -> min(X, plus(Y, Z())), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(min(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + 1, [min](x0, x1) = 0, [quot](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [Z] = 0, [plus#](x0, x1) = x0 Strict: plus#(s X, Y) -> plus#(X, Y) 1 + 0Y + 1X >= 0 + 0Y + 1X Weak: quot(s X, s Y) -> s quot(min(X, Y), s Y) 2 + 1Y + 0X >= 3 + 1Y + 0X quot(0(), s Y) -> 0() 2 + 1Y >= 1 min(min(X, Y), Z()) -> min(X, plus(Y, Z())) 0 + 0Y + 0X >= 0 + 0Y + 0X min(s X, s Y) -> min(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X min(X, 0()) -> X 0 + 0X >= 1X plus(s X, Y) -> s plus(X, Y) 2 + 0Y + 1X >= 2 + 0Y + 1X plus(0(), Y) -> Y 2 + 0Y >= 1Y Qed