YES Time: 0.088300 TRS: { from X -> cons(X, n__from n__s X), from X -> n__from X, sel(0(), cons(X, XS)) -> X, sel(s N, cons(X, XS)) -> sel(N, activate XS), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)), zWquot(nil(), XS) -> nil()} DP: DP: { sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# activate X, activate# n__from X -> activate# X, activate# n__s X -> activate# X, activate# n__s X -> s# activate X, activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), minus#(s X, s Y) -> minus#(X, Y), quot#(s X, s Y) -> s# quot(minus(X, Y), s 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)) -> activate# XS, zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)} TRS: { from X -> cons(X, n__from n__s X), from X -> n__from X, sel(0(), cons(X, XS)) -> X, sel(s N, cons(X, XS)) -> sel(N, activate XS), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)), zWquot(nil(), XS) -> nil()} UR: { from X -> cons(X, n__from n__s X), from X -> n__from X, activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)), zWquot(nil(), XS) -> nil(), a(x, y) -> x, a(x, y) -> y} EDG: {(activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2)) (activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X2) (activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__s X -> s# activate X) (activate# n__s X -> activate# X, activate# n__s X -> activate# X) (activate# n__s X -> activate# X, activate# n__from X -> activate# X) (activate# n__s X -> activate# X, activate# n__from X -> from# activate X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2)) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X2) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X1) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> s# activate X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> activate# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> activate# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# activate X) (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS) (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> sel#(N, activate XS)) (minus#(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) -> quot#(minus(X, Y), s 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) -> s# quot(minus(X, Y), s Y)) (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__from X -> from# activate X) (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__from X -> activate# X) (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__s X -> activate# X) (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__s X -> s# activate X) (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> activate# X1) (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> activate# X2) (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y)) (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__from X -> from# activate X) (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__from X -> activate# X) (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__s X -> activate# X) (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> activate# X1) (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> activate# X2) (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2)) (activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS) (activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS) (activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__from X -> from# activate X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__from X -> activate# X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__s X -> activate# X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__s X -> s# activate X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X1) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X2) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2)) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__from X -> from# activate X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__from X -> activate# X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__s X -> activate# X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__s X -> s# activate X) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__zWquot(X1, X2) -> activate# X1) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__zWquot(X1, X2) -> activate# X2) (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2)) (activate# n__from X -> activate# X, activate# n__from X -> from# activate X) (activate# n__from X -> activate# X, activate# n__from X -> activate# X) (activate# n__from X -> activate# X, activate# n__s X -> activate# X) (activate# n__from X -> activate# X, activate# n__s X -> s# activate X) (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X1) (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X2) (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))} STATUS: arrows: 0.769531 SCCS (3): Scc: {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)} Scc: { activate# n__from X -> activate# X, activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS} Scc: {minus#(s X, s Y) -> minus#(X, Y)} SCC (1): Strict: {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, sel(0(), cons(X, XS)) -> X, sel(s N, cons(X, XS)) -> sel(N, activate XS), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)), zWquot(nil(), XS) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = x0 + x1 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [zWquot](x0, x1) = 0, [n__zWquot](x0, x1) = x0 + 1, [n__from](x0) = 0, [n__s](x0) = 0, [from](x0) = x0 + 1, [activate](x0) = 1, [s](x0) = x0 + 1, [0] = 1, [nil] = 0, [sel#](x0, x1) = x0 Strict: sel#(s N, cons(X, XS)) -> sel#(N, activate XS) 1 + 0X + 0XS + 1N >= 0 + 0XS + 1N Weak: zWquot(nil(), XS) -> nil() 0 + 0XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)) 0 + 0X + 0XS + 0Y + 0YS >= 0 + 0X + 0XS + 0Y + 0YS zWquot(X1, X2) -> n__zWquot(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 zWquot(XS, nil()) -> nil() 0 + 0XS >= 0 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 0X + 1Y >= 3 + 0X + 1Y quot(0(), s Y) -> 0() 2 + 1Y >= 1 minus(s X, s Y) -> minus(X, Y) 2 + 0X + 1Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 s X -> n__s X 1 + 1X >= 0 + 0X activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__s X -> s activate X 1 + 0X >= 2 + 0X activate n__from X -> from activate X 1 + 0X >= 2 + 0X activate X -> X 1 + 0X >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0X + 0XS + 1N >= 2 + 0XS + 1N sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X from X -> n__from X 1 + 1X >= 0 + 0X from X -> cons(X, n__from n__s X) 1 + 1X >= 0 + 0X Qed SCC (7): Strict: { activate# n__from X -> activate# X, activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, sel(0(), cons(X, XS)) -> X, sel(s N, cons(X, XS)) -> sel(N, activate XS), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)), zWquot(nil(), XS) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [sel](x0, x1) = 0, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = 0, [zWquot](x0, x1) = x0 + x1 + 1, [n__zWquot](x0, x1) = x0 + x1 + 1, [n__from](x0) = x0, [n__s](x0) = x0, [from](x0) = x0, [activate](x0) = x0, [s](x0) = x0, [0] = 1, [nil] = 0, [zWquot#](x0, x1) = x0 + x1 + 1, [activate#](x0) = x0 Strict: zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS 1 + 0X + 1XS + 0Y + 1YS >= 0 + 1YS zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS 1 + 0X + 1XS + 0Y + 1YS >= 0 + 1XS activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate# n__zWquot(X1, X2) -> activate# X2 1 + 1X1 + 1X2 >= 0 + 1X2 activate# n__zWquot(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 0 + 1X1 activate# n__s X -> activate# X 0 + 1X >= 0 + 1X activate# n__from X -> activate# X 0 + 1X >= 0 + 1X Weak: zWquot(nil(), XS) -> nil() 1 + 1XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)) 1 + 0X + 1XS + 0Y + 1YS >= 1 + 0X + 1XS + 0Y + 1YS zWquot(X1, X2) -> n__zWquot(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 zWquot(XS, nil()) -> nil() 1 + 1XS >= 0 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 0 + 0X + 0Y >= 0 + 0X + 0Y quot(0(), s Y) -> 0() 0 + 0Y >= 1 minus(s X, s Y) -> minus(X, Y) 1 + 0X + 1Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 s X -> n__s X 0 + 1X >= 0 + 1X activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate n__s X -> s activate X 0 + 1X >= 0 + 1X activate n__from X -> from activate X 0 + 1X >= 0 + 1X activate X -> X 0 + 1X >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 0 + 0X + 0XS + 0N >= 0 + 0XS + 0N sel(0(), cons(X, XS)) -> X 0 + 0X + 0XS >= 1X from X -> n__from X 0 + 1X >= 0 + 1X from X -> cons(X, n__from n__s X) 0 + 1X >= 0 + 1X SCCS (1): Scc: {activate# n__from X -> activate# X, activate# n__s X -> activate# X} SCC (2): Strict: {activate# n__from X -> activate# X, activate# n__s X -> activate# X} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, sel(0(), cons(X, XS)) -> X, sel(s N, cons(X, XS)) -> sel(N, activate XS), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)), zWquot(nil(), XS) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = x0 + x1 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [zWquot](x0, x1) = 0, [n__zWquot](x0, x1) = x0 + 1, [n__from](x0) = x0, [n__s](x0) = x0 + 1, [from](x0) = x0 + 1, [activate](x0) = 1, [s](x0) = 1, [0] = 1, [nil] = 0, [activate#](x0) = x0 Strict: activate# n__s X -> activate# X 1 + 1X >= 0 + 1X activate# n__from X -> activate# X 0 + 1X >= 0 + 1X Weak: zWquot(nil(), XS) -> nil() 0 + 0XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)) 0 + 0X + 0XS + 0Y + 0YS >= 0 + 0X + 0XS + 0Y + 0YS zWquot(X1, X2) -> n__zWquot(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 zWquot(XS, nil()) -> nil() 0 + 0XS >= 0 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 0X + 0Y >= 1 + 0X + 0Y quot(0(), s Y) -> 0() 2 + 0Y >= 1 minus(s X, s Y) -> minus(X, Y) 2 + 0X + 0Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 s X -> n__s X 1 + 0X >= 1 + 1X activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__s X -> s activate X 1 + 0X >= 1 + 0X activate n__from X -> from activate X 1 + 0X >= 2 + 0X activate X -> X 1 + 0X >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0X + 0XS + 0N >= 2 + 0XS + 1N sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X from X -> n__from X 1 + 1X >= 0 + 1X from X -> cons(X, n__from n__s X) 1 + 1X >= 0 + 0X SCCS (1): Scc: {activate# n__from X -> activate# X} SCC (1): Strict: {activate# n__from X -> activate# X} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, sel(0(), cons(X, XS)) -> X, sel(s N, cons(X, XS)) -> sel(N, activate XS), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)), zWquot(nil(), XS) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [sel](x0, x1) = x0 + x1 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [zWquot](x0, x1) = 0, [n__zWquot](x0, x1) = x0 + 1, [n__from](x0) = x0 + 1, [n__s](x0) = 1, [from](x0) = x0 + 1, [activate](x0) = 1, [s](x0) = 1, [0] = 1, [nil] = 0, [activate#](x0) = x0 Strict: activate# n__from X -> activate# X 1 + 1X >= 0 + 1X Weak: zWquot(nil(), XS) -> nil() 0 + 0XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)) 0 + 0X + 0XS + 0Y + 0YS >= 0 + 0X + 0XS + 0Y + 0YS zWquot(X1, X2) -> n__zWquot(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 zWquot(XS, nil()) -> nil() 0 + 0XS >= 0 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 0X + 0Y >= 1 + 0X + 0Y quot(0(), s Y) -> 0() 2 + 0Y >= 1 minus(s X, s Y) -> minus(X, Y) 2 + 0X + 0Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 s X -> n__s X 1 + 0X >= 1 + 0X activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__s X -> s activate X 1 + 0X >= 1 + 0X activate n__from X -> from activate X 1 + 0X >= 2 + 0X activate X -> X 1 + 0X >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0X + 0XS + 0N >= 2 + 0XS + 1N sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X from X -> n__from X 1 + 1X >= 1 + 1X from X -> cons(X, n__from n__s X) 1 + 1X >= 0 + 0X Qed SCC (1): Strict: {minus#(s X, s Y) -> minus#(X, Y)} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, sel(0(), cons(X, XS)) -> X, sel(s N, cons(X, XS)) -> sel(N, activate XS), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2), s X -> n__s X, minus(X, 0()) -> 0(), minus(s X, s Y) -> minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y), zWquot(XS, nil()) -> nil(), zWquot(X1, X2) -> n__zWquot(X1, X2), zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate 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) = 0, [n__zWquot](x0, x1) = x0 + 1, [n__from](x0) = x0 + 1, [n__s](x0) = 1, [from](x0) = x0 + 1, [activate](x0) = 1, [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 + 0XS >= 0 zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)) 0 + 0X + 0XS + 0Y + 0YS >= 1 + 0X + 0XS + 0Y + 0YS zWquot(X1, X2) -> n__zWquot(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 zWquot(XS, nil()) -> nil() 0 + 0XS >= 0 quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 0X + 1Y >= 3 + 0X + 1Y quot(0(), s Y) -> 0() 2 + 1Y >= 1 minus(s X, s Y) -> minus(X, Y) 2 + 0X + 1Y >= 1 + 0X + 1Y minus(X, 0()) -> 0() 2 + 0X >= 1 s X -> n__s X 1 + 1X >= 1 + 0X activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__s X -> s activate X 1 + 0X >= 2 + 0X activate n__from X -> from activate X 1 + 0X >= 2 + 0X activate X -> X 1 + 0X >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0X + 0XS + 0N >= 2 + 0XS + 0N sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X from X -> n__from X 1 + 1X >= 1 + 1X from X -> cons(X, n__from n__s X) 1 + 1X >= 1 + 0X Qed