MAYBE Time: 0.165091 TRS: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} DP: DP: {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), max# cons(x, cons(y, xs)) -> ge#(x, y), if1#(true(), x, y, xs) -> max# cons(x, xs), if1#(false(), x, y, xs) -> max# cons(y, xs), ge#(s x, s y) -> ge#(x, y), del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs), del#(x, cons(y, xs)) -> eq#(x, y), if2#(false(), x, y, xs) -> del#(x, xs), eq#(s x, s y) -> eq#(x, y), sort# cons(x, xs) -> max# cons(x, xs), sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> h# del(max cons(x, xs), cons(x, xs)), h# cons(x, xs) -> h# xs} TRS: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} UR: { max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs), a(z, w) -> z, a(z, w) -> w} EDG: {(sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> eq#(x, y)) (sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs)) (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y)) (if2#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> eq#(x, y)) (if2#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs)) (if1#(false(), x, y, xs) -> max# cons(y, xs), max# cons(x, cons(y, xs)) -> ge#(x, y)) (if1#(false(), x, y, xs) -> max# cons(y, xs), max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs)) (h# cons(x, xs) -> h# xs, h# cons(x, xs) -> h# xs) (del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs), if2#(false(), x, y, xs) -> del#(x, xs)) (max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(true(), x, y, xs) -> max# cons(x, xs)) (max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(false(), x, y, xs) -> max# cons(y, xs)) (sort# cons(x, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs)) (sort# cons(x, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> ge#(x, y)) (if1#(true(), x, y, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs)) (if1#(true(), x, y, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> ge#(x, y)) (sort# cons(x, xs) -> h# del(max cons(x, xs), cons(x, xs)), h# cons(x, xs) -> h# xs) (del#(x, cons(y, xs)) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y)) (max# cons(x, cons(y, xs)) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> max# cons(x, xs)) (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs))) (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs))) (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> h# del(max cons(x, xs), cons(x, xs)))} STATUS: arrows: 0.882653 SCCS (6): Scc: {sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs))} Scc: {h# cons(x, xs) -> h# xs} Scc: { del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs), if2#(false(), x, y, xs) -> del#(x, xs)} Scc: {eq#(s x, s y) -> eq#(x, y)} Scc: {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(true(), x, y, xs) -> max# cons(x, xs), if1#(false(), x, y, xs) -> max# cons(y, xs)} Scc: {ge#(s x, s y) -> ge#(x, y)} SCC (1): Strict: {sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs))} Weak: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} Fail SCC (1): Strict: {h# cons(x, xs) -> h# xs} Weak: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if1](x0, x1, x2, x3) = x0 + x1 + 1, [if2](x0, x1, x2, x3) = 0, [cons](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + 1, [del](x0, x1) = x0 + x1, [eq](x0, x1) = 0, [max](x0) = x0 + 1, [s](x0) = 1, [sort](x0) = x0 + 1, [h](x0) = x0 + 1, [0] = 1, [nil] = 1, [true] = 1, [false] = 1, [h#](x0) = x0 Strict: h# cons(x, xs) -> h# xs 1 + 0x + 1xs >= 0 + 1xs Weak: h cons(x, xs) -> cons(x, h xs) 2 + 0x + 1xs >= 2 + 0x + 1xs h nil() -> nil() 2 >= 1 sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))) 2 + 0x + 1xs >= 6 + 0x + 2xs sort nil() -> nil() 2 >= 1 eq(s x, s y) -> eq(x, y) 0 + 0x + 0y >= 0 + 0x + 0y eq(s x, 0()) -> false() 0 + 0x >= 1 eq(0(), s y) -> false() 0 + 0y >= 1 eq(0(), 0()) -> true() 0 >= 1 if2(false(), x, y, xs) -> cons(y, del(x, xs)) 0 + 0x + 0y + 0xs >= 1 + 1x + 0y + 1xs if2(true(), x, y, xs) -> xs 0 + 0x + 0y + 0xs >= 1xs del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) 1 + 1x + 0y + 1xs >= 0 + 0x + 0y + 0xs del(x, nil()) -> nil() 1 + 1x >= 1 ge(s x, s y) -> ge(x, y) 2 + 0x + 0y >= 1 + 1x + 0y ge(s x, 0()) -> true() 2 + 0x >= 1 ge(0(), s x) -> false() 2 + 0x >= 1 ge(0(), 0()) -> true() 2 >= 1 if1(false(), x, y, xs) -> max cons(y, xs) 2 + 1x + 0y + 0xs >= 2 + 0y + 1xs if1(true(), x, y, xs) -> max cons(x, xs) 2 + 1x + 0y + 0xs >= 2 + 0x + 1xs max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs) 3 + 0x + 0y + 1xs >= 2 + 2x + 0y + 0xs max cons(x, nil()) -> x 3 + 0x >= 1x max nil() -> 0() 2 >= 1 Qed SCC (2): Strict: { del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs), if2#(false(), x, y, xs) -> del#(x, xs)} Weak: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if1](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [if2](x0, x1, x2, x3) = 0, [cons](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + x1 + 1, [del](x0, x1) = 0, [eq](x0, x1) = 0, [max](x0) = 0, [s](x0) = 1, [sort](x0) = x0 + 1, [h](x0) = x0 + 1, [0] = 0, [nil] = 1, [true] = 1, [false] = 0, [if2#](x0, x1, x2, x3) = x0, [del#](x0, x1) = x0 Strict: if2#(false(), x, y, xs) -> del#(x, xs) 0 + 0x + 0y + 1xs >= 0 + 0x + 1xs del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs) 1 + 0x + 0y + 1xs >= 0 + 0x + 0y + 1xs Weak: h cons(x, xs) -> cons(x, h xs) 2 + 0x + 1xs >= 2 + 0x + 1xs h nil() -> nil() 2 >= 1 sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))) 2 + 0x + 1xs >= 3 + 0x + 0xs sort nil() -> nil() 2 >= 1 eq(s x, s y) -> eq(x, y) 0 + 0x + 0y >= 0 + 0x + 0y eq(s x, 0()) -> false() 0 + 0x >= 0 eq(0(), s y) -> false() 0 + 0y >= 0 eq(0(), 0()) -> true() 0 >= 1 if2(false(), x, y, xs) -> cons(y, del(x, xs)) 0 + 0x + 0y + 0xs >= 1 + 0x + 0y + 0xs if2(true(), x, y, xs) -> xs 0 + 0x + 0y + 0xs >= 1xs del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) 0 + 0x + 0y + 0xs >= 0 + 0x + 0y + 0xs del(x, nil()) -> nil() 0 + 0x >= 1 ge(s x, s y) -> ge(x, y) 3 + 0x + 0y >= 1 + 1x + 1y ge(s x, 0()) -> true() 2 + 0x >= 1 ge(0(), s x) -> false() 2 + 0x >= 0 ge(0(), 0()) -> true() 1 >= 1 if1(false(), x, y, xs) -> max cons(y, xs) 1 + 1x + 1y + 0xs >= 0 + 0y + 0xs if1(true(), x, y, xs) -> max cons(x, xs) 2 + 1x + 1y + 0xs >= 0 + 0x + 0xs max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs) 0 + 0x + 0y + 0xs >= 2 + 2x + 2y + 0xs max cons(x, nil()) -> x 0 + 0x >= 1x max nil() -> 0() 0 >= 0 SCCS (0): SCC (1): Strict: {eq#(s x, s y) -> eq#(x, y)} Weak: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if1](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [if2](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [cons](x0, x1) = x0, [ge](x0, x1) = x0 + x1 + 1, [del](x0, x1) = x0 + 1, [eq](x0, x1) = x0 + x1 + 1, [max](x0) = x0 + 1, [s](x0) = x0 + 1, [sort](x0) = x0 + 1, [h](x0) = x0, [0] = 0, [nil] = 1, [true] = 1, [false] = 1, [eq#](x0, x1) = x0 Strict: eq#(s x, s y) -> eq#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: h cons(x, xs) -> cons(x, h xs) 0 + 0x + 1xs >= 0 + 0x + 1xs h nil() -> nil() 1 >= 1 sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))) 1 + 0x + 1xs >= 2 + 0x + 1xs sort nil() -> nil() 2 >= 1 eq(s x, s y) -> eq(x, y) 3 + 1x + 1y >= 1 + 1x + 1y eq(s x, 0()) -> false() 2 + 1x >= 1 eq(0(), s y) -> false() 2 + 1y >= 1 eq(0(), 0()) -> true() 1 >= 1 if2(false(), x, y, xs) -> cons(y, del(x, xs)) 2 + 1x + 1y + 0xs >= 1 + 0x + 0y + 1xs if2(true(), x, y, xs) -> xs 2 + 1x + 1y + 0xs >= 1xs del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) 1 + 0x + 0y + 1xs >= 2 + 2x + 2y + 0xs del(x, nil()) -> nil() 2 + 0x >= 1 ge(s x, s y) -> ge(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge(s x, 0()) -> true() 2 + 1x >= 1 ge(0(), s x) -> false() 2 + 1x >= 1 ge(0(), 0()) -> true() 1 >= 1 if1(false(), x, y, xs) -> max cons(y, xs) 2 + 1x + 1y + 0xs >= 1 + 0y + 1xs if1(true(), x, y, xs) -> max cons(x, xs) 2 + 1x + 1y + 0xs >= 1 + 0x + 1xs max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs) 1 + 0x + 0y + 1xs >= 2 + 2x + 2y + 0xs max cons(x, nil()) -> x 2 + 0x >= 1x max nil() -> 0() 2 >= 0 Qed SCC (3): Strict: {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(true(), x, y, xs) -> max# cons(x, xs), if1#(false(), x, y, xs) -> max# cons(y, xs)} Weak: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if1](x0, x1, x2, x3) = x0 + 1, [if2](x0, x1, x2, x3) = x0 + x1 + 1, [cons](x0, x1) = x0 + 1, [ge](x0, x1) = 1, [del](x0, x1) = x0 + x1 + 1, [eq](x0, x1) = x0 + 1, [max](x0) = 1, [s](x0) = 1, [sort](x0) = x0 + 1, [h](x0) = x0 + 1, [0] = 1, [nil] = 1, [true] = 1, [false] = 0, [if1#](x0, x1, x2, x3) = x0 + x1 + 1, [max#](x0) = x0 Strict: if1#(false(), x, y, xs) -> max# cons(y, xs) 1 + 0x + 0y + 1xs >= 1 + 0y + 1xs if1#(true(), x, y, xs) -> max# cons(x, xs) 2 + 0x + 0y + 1xs >= 1 + 0x + 1xs max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs) 2 + 0x + 0y + 1xs >= 2 + 0x + 0y + 1xs Weak: h cons(x, xs) -> cons(x, h xs) 2 + 0x + 1xs >= 2 + 0x + 1xs h nil() -> nil() 2 >= 1 sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))) 2 + 0x + 1xs >= 6 + 0x + 1xs sort nil() -> nil() 2 >= 1 eq(s x, s y) -> eq(x, y) 2 + 0x + 0y >= 1 + 1x + 0y eq(s x, 0()) -> false() 2 + 0x >= 0 eq(0(), s y) -> false() 2 + 0y >= 0 eq(0(), 0()) -> true() 2 >= 1 if2(false(), x, y, xs) -> cons(y, del(x, xs)) 1 + 1x + 0y + 0xs >= 2 + 1x + 0y + 1xs if2(true(), x, y, xs) -> xs 2 + 1x + 0y + 0xs >= 1xs del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) 2 + 1x + 0y + 1xs >= 2 + 2x + 0y + 0xs del(x, nil()) -> nil() 2 + 1x >= 1 ge(s x, s y) -> ge(x, y) 1 + 0x + 0y >= 1 + 0x + 0y ge(s x, 0()) -> true() 1 + 0x >= 1 ge(0(), s x) -> false() 1 + 0x >= 0 ge(0(), 0()) -> true() 1 >= 1 if1(false(), x, y, xs) -> max cons(y, xs) 1 + 0x + 0y + 0xs >= 1 + 0y + 0xs if1(true(), x, y, xs) -> max cons(x, xs) 2 + 0x + 0y + 0xs >= 1 + 0x + 0xs max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs) 1 + 0x + 0y + 0xs >= 2 + 0x + 0y + 0xs max cons(x, nil()) -> x 1 + 0x >= 1x max nil() -> 0() 1 >= 1 SCCS (1): Scc: {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(false(), x, y, xs) -> max# cons(y, xs)} SCC (2): Strict: {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(false(), x, y, xs) -> max# cons(y, xs)} Weak: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if1](x0, x1, x2, x3) = x0 + 1, [if2](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [cons](x0, x1) = x0 + 1, [ge](x0, x1) = 1, [del](x0, x1) = x0, [eq](x0, x1) = x0 + x1 + 1, [max](x0) = x0 + 1, [s](x0) = 0, [sort](x0) = 0, [h](x0) = 0, [0] = 0, [nil] = 0, [true] = 1, [false] = 1, [if1#](x0, x1, x2, x3) = x0 + x1, [max#](x0) = x0 Strict: if1#(false(), x, y, xs) -> max# cons(y, xs) 1 + 0x + 0y + 1xs >= 1 + 0y + 1xs max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs) 2 + 0x + 0y + 1xs >= 1 + 0x + 0y + 1xs Weak: h cons(x, xs) -> cons(x, h xs) 0 + 0x + 0xs >= 1 + 0x + 0xs h nil() -> nil() 0 >= 0 sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))) 0 + 0x + 0xs >= 1 + 0x + 0xs sort nil() -> nil() 0 >= 0 eq(s x, s y) -> eq(x, y) 1 + 0x + 0y >= 1 + 1x + 1y eq(s x, 0()) -> false() 1 + 0x >= 1 eq(0(), s y) -> false() 1 + 0y >= 1 eq(0(), 0()) -> true() 1 >= 1 if2(false(), x, y, xs) -> cons(y, del(x, xs)) 2 + 1x + 1y + 0xs >= 1 + 0x + 0y + 1xs if2(true(), x, y, xs) -> xs 2 + 1x + 1y + 0xs >= 1xs del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) 1 + 0x + 0y + 1xs >= 2 + 2x + 2y + 0xs del(x, nil()) -> nil() 0 + 0x >= 0 ge(s x, s y) -> ge(x, y) 1 + 0x + 0y >= 1 + 0x + 0y ge(s x, 0()) -> true() 1 + 0x >= 1 ge(0(), s x) -> false() 1 + 0x >= 1 ge(0(), 0()) -> true() 1 >= 1 if1(false(), x, y, xs) -> max cons(y, xs) 2 + 0x + 0y + 0xs >= 2 + 0y + 1xs if1(true(), x, y, xs) -> max cons(x, xs) 2 + 0x + 0y + 0xs >= 2 + 0x + 1xs max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs) 3 + 0x + 0y + 1xs >= 2 + 0x + 0y + 0xs max cons(x, nil()) -> x 2 + 0x >= 1x max nil() -> 0() 1 >= 0 SCCS (0): SCC (1): Strict: {ge#(s x, s y) -> ge#(x, y)} Weak: { max nil() -> 0(), max cons(x, nil()) -> x, max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs), if1(true(), x, y, xs) -> max cons(x, xs), if1(false(), x, y, xs) -> max cons(y, xs), ge(0(), 0()) -> true(), ge(0(), s x) -> false(), ge(s x, 0()) -> true(), ge(s x, s y) -> ge(x, y), del(x, nil()) -> nil(), del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs), if2(true(), x, y, xs) -> xs, if2(false(), x, y, xs) -> cons(y, del(x, xs)), eq(0(), 0()) -> true(), eq(0(), s y) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), sort nil() -> nil(), sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))), h nil() -> nil(), h cons(x, xs) -> cons(x, h xs)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if1](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [if2](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [cons](x0, x1) = x0, [ge](x0, x1) = x0 + x1 + 1, [del](x0, x1) = x0 + 1, [eq](x0, x1) = x0 + x1 + 1, [max](x0) = x0 + 1, [s](x0) = x0 + 1, [sort](x0) = x0 + 1, [h](x0) = x0, [0] = 0, [nil] = 1, [true] = 1, [false] = 1, [ge#](x0, x1) = x0 Strict: ge#(s x, s y) -> ge#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: h cons(x, xs) -> cons(x, h xs) 0 + 0x + 1xs >= 0 + 0x + 1xs h nil() -> nil() 1 >= 1 sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))) 1 + 0x + 1xs >= 2 + 0x + 1xs sort nil() -> nil() 2 >= 1 eq(s x, s y) -> eq(x, y) 3 + 1x + 1y >= 1 + 1x + 1y eq(s x, 0()) -> false() 2 + 1x >= 1 eq(0(), s y) -> false() 2 + 1y >= 1 eq(0(), 0()) -> true() 1 >= 1 if2(false(), x, y, xs) -> cons(y, del(x, xs)) 2 + 1x + 1y + 0xs >= 1 + 0x + 0y + 1xs if2(true(), x, y, xs) -> xs 2 + 1x + 1y + 0xs >= 1xs del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) 1 + 0x + 0y + 1xs >= 2 + 2x + 2y + 0xs del(x, nil()) -> nil() 2 + 0x >= 1 ge(s x, s y) -> ge(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge(s x, 0()) -> true() 2 + 1x >= 1 ge(0(), s x) -> false() 2 + 1x >= 1 ge(0(), 0()) -> true() 1 >= 1 if1(false(), x, y, xs) -> max cons(y, xs) 2 + 1x + 1y + 0xs >= 1 + 0y + 1xs if1(true(), x, y, xs) -> max cons(x, xs) 2 + 1x + 1y + 0xs >= 1 + 0x + 1xs max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs) 1 + 0x + 0y + 1xs >= 2 + 2x + 2y + 0xs max cons(x, nil()) -> x 2 + 0x >= 1x max nil() -> 0() 2 >= 0 Qed