MAYBE Time: 0.098181 TRS: { from X -> cons(X, from s X), sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(s X, s Y) -> s quot(minus(X, Y), s Y), quot(0(), s Y) -> 0(), zWquot(XS, nil()) -> nil(), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)), zWquot(nil(), XS) -> nil()} DP: DP: { from# X -> from# s X, sel#(s N, cons(X, XS)) -> sel#(N, XS), minus#(s X, s Y) -> minus#(X, Y), quot#(s X, s Y) -> minus#(X, Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y), zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), zWquot#(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)} TRS: { from X -> cons(X, from s X), sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(s X, s Y) -> s quot(minus(X, Y), s Y), quot(0(), s Y) -> 0(), zWquot(XS, nil()) -> nil(), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)), zWquot(nil(), XS) -> nil()} UR: { minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), a(x, y) -> x, a(x, y) -> y} EDG: {(from# X -> from# s X, from# X -> from# s X) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y)) (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s X, s Y) -> minus#(X, Y)) (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y)) (minus#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y)) (sel#(s N, cons(X, XS)) -> sel#(N, XS), sel#(s N, cons(X, XS)) -> sel#(N, XS)) (zWquot#(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS), zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (zWquot#(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS), zWquot#(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS))} STATUS: arrows: 0.836735 SCCS (4): Scc: {from# X -> from# s X} Scc: {sel#(s N, cons(X, XS)) -> sel#(N, XS)} Scc: {zWquot#(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)} Scc: {minus#(s X, s Y) -> minus#(X, Y)} SCC (1): Strict: {from# X -> from# s X} Weak: { from X -> cons(X, from s X), sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(s X, s Y) -> s quot(minus(X, Y), s Y), quot(0(), s Y) -> 0(), zWquot(XS, nil()) -> nil(), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)), zWquot(nil(), XS) -> nil()} Fail SCC (1): Strict: {sel#(s N, cons(X, XS)) -> sel#(N, XS)} Weak: { from X -> cons(X, from s X), sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(s X, s Y) -> s quot(minus(X, Y), s Y), quot(0(), s Y) -> 0(), zWquot(XS, nil()) -> nil(), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)), zWquot(nil(), XS) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [sel](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [zWquot](x0, x1) = x0 + x1, [from](x0) = 0, [s](x0) = 1, [0] = 1, [nil] = 0, [sel#](x0, x1) = x0 Strict: sel#(s N, cons(X, XS)) -> sel#(N, XS) 1 + 0X + 1XS + 0N >= 0 + 1XS + 0N Weak: zWquot(nil(), XS) -> nil() 0 + 1XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) 2 + 0X + 1XS + 0Y + 1YS >= 1 + 0X + 1XS + 0Y + 1YS zWquot(XS, nil()) -> nil() 0 + 1XS >= 0 quot(0(), s Y) -> 0() 2 + 0Y >= 1 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 0X + 0Y >= 1 + 0X + 0Y minus(s X, s Y) -> minus(X, Y) 2 + 0X + 0Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, XS) 2 + 0X + 0XS + 0N >= 1 + 0XS + 1N from X -> cons(X, from s X) 0 + 0X >= 1 + 0X Qed SCC (1): Strict: {zWquot#(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)} Weak: { from X -> cons(X, from s X), sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(s X, s Y) -> s quot(minus(X, Y), s Y), quot(0(), s Y) -> 0(), zWquot(XS, nil()) -> nil(), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)), zWquot(nil(), XS) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [sel](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [zWquot](x0, x1) = x0 + x1, [from](x0) = 0, [s](x0) = 1, [0] = 1, [nil] = 0, [zWquot#](x0, x1) = x0 Strict: zWquot#(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS) 1 + 0X + 0XS + 0Y + 1YS >= 0 + 0XS + 1YS Weak: zWquot(nil(), XS) -> nil() 0 + 1XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) 2 + 0X + 1XS + 0Y + 1YS >= 1 + 0X + 1XS + 0Y + 1YS zWquot(XS, nil()) -> nil() 0 + 1XS >= 0 quot(0(), s Y) -> 0() 2 + 0Y >= 1 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 0X + 0Y >= 1 + 0X + 0Y minus(s X, s Y) -> minus(X, Y) 2 + 0X + 0Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 sel(0(), cons(X, XS)) -> X 2 + 0X + 1XS >= 1X sel(s N, cons(X, XS)) -> sel(N, XS) 2 + 0X + 1XS + 0N >= 1 + 1XS + 0N from X -> cons(X, from s X) 0 + 0X >= 1 + 0X Qed SCC (1): Strict: {minus#(s X, s Y) -> minus#(X, Y)} Weak: { from X -> cons(X, from s X), sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(s X, s Y) -> s quot(minus(X, Y), s Y), quot(0(), s Y) -> 0(), zWquot(XS, nil()) -> nil(), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)), zWquot(nil(), XS) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 1, [sel](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [zWquot](x0, x1) = x0 + x1, [from](x0) = 0, [s](x0) = x0 + 1, [0] = 1, [nil] = 0, [minus#](x0, x1) = x0 Strict: minus#(s X, s Y) -> minus#(X, Y) 1 + 0X + 1Y >= 0 + 0X + 1Y Weak: zWquot(nil(), XS) -> nil() 0 + 1XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) 2 + 0X + 0XS + 0Y + 0YS >= 1 + 0X + 0XS + 0Y + 0YS zWquot(XS, nil()) -> nil() 0 + 1XS >= 0 quot(0(), s Y) -> 0() 2 + 0Y >= 1 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 1X + 0Y >= 3 + 0X + 1Y minus(s X, s Y) -> minus(X, Y) 2 + 0X + 1Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, XS) 2 + 0X + 0XS + 0N >= 1 + 1XS + 0N from X -> cons(X, from s X) 0 + 0X >= 1 + 0X Qed