YES Time: 0.157712 TRS: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} DP: DP: { a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> s# h(), a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(h(), h(), h(), x) -> s# x, +#(s x, s y) -> s# s +(x, y), +#(s x, s y) -> s# +(x, y), +#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), app#(cons(x, l), k) -> app#(l, k), sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)} TRS: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} UR: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), b(w, v) -> w, b(w, v) -> v} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# s +(x, y)) (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(h(), h(), h(), x) -> s# x) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> s# h()) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# s +(x, y)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# +(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# s +(x, y)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, x, s y, h()) -> s# h()) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(h(), h(), h(), x) -> s# x) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> a#(x, y, h(), h())) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, x, s y, h()) -> s# h()) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(h(), h(), h(), x) -> s# x)} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# s +(x, y)) (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(h(), h(), h(), x) -> s# x) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> s# h()) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# s +(x, y)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# +(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# s +(x, y)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(h(), h(), h(), x) -> s# x) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> a#(x, y, h(), h())) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(h(), h(), h(), x) -> s# x)} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# s +(x, y)) (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(h(), h(), h(), x) -> s# x) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> s# h()) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# s +(x, y)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# +(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# s +(x, y)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(h(), h(), h(), x) -> s# x) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> a#(x, y, h(), h())) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(h(), h(), h(), x) -> s# x)} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s x, s y) -> s# s +(x, y)) (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(h(), h(), h(), x) -> s# x) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, h()) -> s# h()) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, s x, h(), z) -> a#(l, x, z, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(s x, s y) -> s# s +(x, y)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> +#(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# +(x, y)) (+#(s x, s y) -> +#(x, y), +#(s x, s y) -> s# s +(x, y)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(l, s x, h(), z) -> a#(l, x, z, z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (sum# cons(x, cons(y, l)) -> a#(x, y, h(), h()), a#(h(), h(), h(), x) -> s# x) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> a#(x, y, h(), h())) (sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l), sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(s l, h(), h(), z) -> a#(l, z, h(), z), a#(h(), h(), h(), x) -> s# x) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> s# h()) (a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z))) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, s x, h(), z) -> a#(l, x, z, z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(s l, h(), h(), z) -> a#(l, z, h(), z)) (a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(h(), h(), h(), x) -> s# x)} STATUS: arrows: 0.800000 SCCS (4): Scc: {sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)} Scc: {app#(cons(x, l), k) -> app#(l, k)} Scc: { +#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Scc: { a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)} SCC (1): Strict: {sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l)} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1, [+](x0, x1) = x0 + 1, [app](x0, x1) = x0, [cons](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [sum](x0) = 0, [h] = 1, [1] = 0, [nil] = 0, [sum#](x0) = x0 Strict: sum# cons(x, cons(y, l)) -> sum# cons(a(x, y, h(), h()), l) 2 + 0x + 1l + 0y >= 1 + 0x + 1l + 0y Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y sum cons(x, nil()) -> cons(x, nil()) 0 + 0x >= 1 + 0x app(cons(x, l), k) -> cons(x, app(l, k)) 1 + 0x + 1l + 0k >= 1 + 0x + 1l + 0k app(nil(), k) -> k 0 + 0k >= 1k app(l, nil()) -> l 0 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z +(h(), x) -> x 1 + 1x >= 1x +(s x, s y) -> s s +(x, y) 2 + 0x + 1y >= 3 + 0x + 1y +(x, h()) -> x 2 + 0x >= 1x a(h(), h(), h(), x) -> s x 4 + 1x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 4 + 1l + 1z >= 2 + 1l + 2z a(l, s x, h(), z) -> a(l, x, z, z) 3 + 1x + 1l + 1z >= 1 + 1x + 1l + 2z a(l, x, s y, h()) -> a(l, x, y, s h()) 3 + 1x + 1l + 1y >= 3 + 1x + 1l + 1y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 3 + 1x + 1l + 1y + 1z >= 3 + 2x + 2l + 2y + 1z s h() -> 1() 2 >= 0 Qed SCC (1): Strict: {app#(cons(x, l), k) -> app#(l, k)} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1, [+](x0, x1) = x0 + 1, [app](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [sum](x0) = 0, [h] = 1, [1] = 0, [nil] = 1, [app#](x0, x1) = x0 + 1 Strict: app#(cons(x, l), k) -> app#(l, k) 2 + 0x + 1l + 0k >= 1 + 1l + 0k Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y sum cons(x, nil()) -> cons(x, nil()) 0 + 0x >= 2 + 0x app(cons(x, l), k) -> cons(x, app(l, k)) 2 + 0x + 1l + 1k >= 2 + 0x + 1l + 1k app(nil(), k) -> k 2 + 1k >= 1k app(l, nil()) -> l 2 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z +(h(), x) -> x 1 + 1x >= 1x +(s x, s y) -> s s +(x, y) 2 + 0x + 1y >= 3 + 0x + 1y +(x, h()) -> x 2 + 0x >= 1x a(h(), h(), h(), x) -> s x 4 + 1x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 4 + 1l + 1z >= 2 + 1l + 2z a(l, s x, h(), z) -> a(l, x, z, z) 3 + 1x + 1l + 1z >= 1 + 1x + 1l + 2z a(l, x, s y, h()) -> a(l, x, y, s h()) 3 + 1x + 1l + 1y >= 3 + 1x + 1l + 1y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 3 + 1x + 1l + 1y + 1z >= 3 + 2x + 2l + 2y + 1z s h() -> 1() 2 >= 0 Qed SCC (3): Strict: { +#(s x, s y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = 0, [+](x0, x1) = x0 + x1 + 1, [app](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = 1, [s](x0) = x0 + 1, [sum](x0) = 0, [h] = 1, [1] = 0, [nil] = 1, [+#](x0, x1) = x0 + x1 + 1 Strict: +#(+(x, y), z) -> +#(y, z) 2 + 1x + 1y + 1z >= 1 + 1y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +#(s x, s y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y sum cons(x, nil()) -> cons(x, nil()) 0 + 0x >= 1 + 0x app(cons(x, l), k) -> cons(x, app(l, k)) 2 + 0x + 0l + 1k >= 1 + 0x + 0l + 0k app(nil(), k) -> k 2 + 1k >= 1k app(l, nil()) -> l 2 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(h(), x) -> x 2 + 1x >= 1x +(s x, s y) -> s s +(x, y) 3 + 1x + 1y >= 3 + 1x + 1y +(x, h()) -> x 2 + 1x >= 1x a(h(), h(), h(), x) -> s x 0 + 0x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 0 + 0l + 0z >= 0 + 0l + 0z a(l, s x, h(), z) -> a(l, x, z, z) 0 + 0x + 0l + 0z >= 0 + 0x + 0l + 0z a(l, x, s y, h()) -> a(l, x, y, s h()) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 0 + 0x + 0l + 0y + 0z >= 0 + 0x + 0l + 0y + 0z s h() -> 1() 2 >= 0 SCCS (1): Scc: {+#(+(x, y), z) -> +#(x, +(y, z))} SCC (1): Strict: {+#(+(x, y), z) -> +#(x, +(y, z))} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1, [+](x0, x1) = x0 + x1 + 1, [app](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [sum](x0) = 0, [h] = 1, [1] = 0, [nil] = 1, [+#](x0, x1) = x0 + 1 Strict: +#(+(x, y), z) -> +#(x, +(y, z)) 2 + 1x + 1y + 0z >= 1 + 1x + 0y + 0z Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y sum cons(x, nil()) -> cons(x, nil()) 0 + 0x >= 2 + 0x app(cons(x, l), k) -> cons(x, app(l, k)) 2 + 0x + 1l + 1k >= 2 + 0x + 1l + 1k app(nil(), k) -> k 2 + 1k >= 1k app(l, nil()) -> l 2 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(h(), x) -> x 2 + 1x >= 1x +(s x, s y) -> s s +(x, y) 3 + 1x + 1y >= 3 + 1x + 1y +(x, h()) -> x 2 + 1x >= 1x a(h(), h(), h(), x) -> s x 4 + 1x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 4 + 1l + 1z >= 2 + 1l + 2z a(l, s x, h(), z) -> a(l, x, z, z) 3 + 1x + 1l + 1z >= 1 + 1x + 1l + 2z a(l, x, s y, h()) -> a(l, x, y, s h()) 3 + 1x + 1l + 1y >= 3 + 1x + 1l + 1y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 3 + 1x + 1l + 1y + 1z >= 3 + 2x + 2l + 2y + 1z s h() -> 1() 2 >= 0 Qed SCC (5): Strict: { a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z), a#(s l, h(), h(), z) -> a#(l, z, h(), z)} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = x0 + 1, [+](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [sum](x0) = 0, [h] = 1, [1] = 0, [nil] = 1, [a#](x0, x1, x2, x3) = x0 + 1 Strict: a#(s l, h(), h(), z) -> a#(l, z, h(), z) 2 + 1l + 0z >= 1 + 1l + 0z a#(l, s x, h(), z) -> a#(l, x, z, z) 1 + 0x + 1l + 0z >= 1 + 0x + 1l + 0z a#(l, x, s y, h()) -> a#(l, x, y, s h()) 1 + 0x + 1l + 0y >= 1 + 0x + 1l + 0y a#(l, x, s y, s z) -> a#(l, x, s y, z) 1 + 0x + 1l + 0y + 0z >= 1 + 0x + 1l + 0y + 0z a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)) 1 + 0x + 1l + 0y + 0z >= 1 + 0x + 1l + 0y + 0z Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y sum cons(x, nil()) -> cons(x, nil()) 0 + 0x >= 2 + 0x app(cons(x, l), k) -> cons(x, app(l, k)) 2 + 0x + 1l + 0k >= 2 + 0x + 1l + 0k app(nil(), k) -> k 2 + 0k >= 1k app(l, nil()) -> l 1 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z +(h(), x) -> x 1 + 1x >= 1x +(s x, s y) -> s s +(x, y) 2 + 0x + 1y >= 3 + 0x + 1y +(x, h()) -> x 2 + 0x >= 1x a(h(), h(), h(), x) -> s x 2 + 0x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 2 + 0l + 0z >= 2 + 0l + 0z a(l, s x, h(), z) -> a(l, x, z, z) 2 + 0x + 0l + 0z >= 1 + 0x + 0l + 1z a(l, x, s y, h()) -> a(l, x, y, s h()) 2 + 0x + 0l + 1y >= 1 + 0x + 0l + 1y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 2 + 0x + 0l + 1y + 0z >= 1 + 0x + 0l + 1y + 0z s h() -> 1() 2 >= 0 SCCS (1): Scc: {a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z)} SCC (4): Strict: {a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h()), a#(l, s x, h(), z) -> a#(l, x, z, z)} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = x0 + 1, [+](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [sum](x0) = x0 + 1, [h] = 1, [1] = 0, [nil] = 0, [a#](x0, x1, x2, x3) = x0 + 1 Strict: a#(l, s x, h(), z) -> a#(l, x, z, z) 2 + 1x + 0l + 0z >= 1 + 1x + 0l + 0z a#(l, x, s y, h()) -> a#(l, x, y, s h()) 1 + 1x + 0l + 0y >= 1 + 1x + 0l + 0y a#(l, x, s y, s z) -> a#(l, x, s y, z) 1 + 1x + 0l + 0y + 0z >= 1 + 1x + 0l + 0y + 0z a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)) 1 + 1x + 0l + 0y + 0z >= 1 + 1x + 0l + 0y + 0z Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 3 + 0x + 1l + 0y >= 2 + 0x + 1l + 0y sum cons(x, nil()) -> cons(x, nil()) 2 + 0x >= 1 + 0x app(cons(x, l), k) -> cons(x, app(l, k)) 2 + 0x + 1l + 0k >= 2 + 0x + 1l + 0k app(nil(), k) -> k 1 + 0k >= 1k app(l, nil()) -> l 1 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z +(h(), x) -> x 1 + 1x >= 1x +(s x, s y) -> s s +(x, y) 2 + 0x + 1y >= 3 + 0x + 1y +(x, h()) -> x 2 + 0x >= 1x a(h(), h(), h(), x) -> s x 2 + 0x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 2 + 0l + 0z >= 2 + 0l + 0z a(l, s x, h(), z) -> a(l, x, z, z) 2 + 0x + 0l + 0z >= 1 + 0x + 0l + 1z a(l, x, s y, h()) -> a(l, x, y, s h()) 2 + 0x + 0l + 1y >= 1 + 0x + 0l + 1y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 2 + 0x + 0l + 1y + 0z >= 1 + 0x + 0l + 1y + 0z s h() -> 1() 2 >= 0 SCCS (1): Scc: {a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())} SCC (3): Strict: {a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)), a#(l, x, s y, s z) -> a#(l, x, s y, z), a#(l, x, s y, h()) -> a#(l, x, y, s h())} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = 0, [+](x0, x1) = 0, [app](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = 0, [s](x0) = x0 + 1, [sum](x0) = 0, [h] = 0, [1] = 0, [nil] = 1, [a#](x0, x1, x2, x3) = x0 Strict: a#(l, x, s y, h()) -> a#(l, x, y, s h()) 1 + 0x + 0l + 1y >= 0 + 0x + 0l + 1y a#(l, x, s y, s z) -> a#(l, x, s y, z) 1 + 0x + 0l + 1y + 0z >= 1 + 0x + 0l + 1y + 0z a#(l, x, s y, s z) -> a#(l, x, y, a(l, x, s y, z)) 1 + 0x + 0l + 1y + 0z >= 0 + 0x + 0l + 1y + 0z Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y sum cons(x, nil()) -> cons(x, nil()) 0 + 0x >= 0 + 0x app(cons(x, l), k) -> cons(x, app(l, k)) 1 + 0x + 0l + 1k >= 0 + 0x + 0l + 0k app(nil(), k) -> k 2 + 1k >= 1k app(l, nil()) -> l 2 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z +(h(), x) -> x 0 + 0x >= 1x +(s x, s y) -> s s +(x, y) 0 + 0x + 0y >= 2 + 0x + 0y +(x, h()) -> x 0 + 0x >= 1x a(h(), h(), h(), x) -> s x 0 + 0x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 0 + 0l + 0z >= 0 + 0l + 0z a(l, s x, h(), z) -> a(l, x, z, z) 0 + 0x + 0l + 0z >= 0 + 0x + 0l + 0z a(l, x, s y, h()) -> a(l, x, y, s h()) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 0 + 0x + 0l + 0y + 0z >= 0 + 0x + 0l + 0y + 0z s h() -> 1() 1 >= 0 SCCS (1): Scc: {a#(l, x, s y, s z) -> a#(l, x, s y, z)} SCC (1): Strict: {a#(l, x, s y, s z) -> a#(l, x, s y, z)} Weak: { s h() -> 1(), a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)), a(l, x, s y, h()) -> a(l, x, y, s h()), a(l, s x, h(), z) -> a(l, x, z, z), a(s l, h(), h(), z) -> a(l, z, h(), z), a(h(), h(), h(), x) -> s x, +(x, h()) -> x, +(s x, s y) -> s s +(x, y), +(h(), x) -> x, +(+(x, y), z) -> +(x, +(y, z)), app(l, nil()) -> l, app(nil(), k) -> k, app(cons(x, l), k) -> cons(x, app(l, k)), sum cons(x, nil()) -> cons(x, nil()), sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1, [+](x0, x1) = x0 + 1, [app](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [sum](x0) = 0, [h] = 1, [1] = 0, [nil] = 1, [a#](x0, x1, x2, x3) = x0 + x1 Strict: a#(l, x, s y, s z) -> a#(l, x, s y, z) 2 + 0x + 0l + 1y + 1z >= 1 + 0x + 0l + 1y + 1z Weak: sum cons(x, cons(y, l)) -> sum cons(a(x, y, h(), h()), l) 0 + 0x + 0l + 0y >= 0 + 0x + 0l + 0y sum cons(x, nil()) -> cons(x, nil()) 0 + 0x >= 2 + 1x app(cons(x, l), k) -> cons(x, app(l, k)) 2 + 1x + 1l + 1k >= 2 + 1x + 1l + 1k app(nil(), k) -> k 2 + 1k >= 1k app(l, nil()) -> l 2 + 1l >= 1l +(+(x, y), z) -> +(x, +(y, z)) 1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z +(h(), x) -> x 1 + 1x >= 1x +(s x, s y) -> s s +(x, y) 2 + 0x + 1y >= 3 + 0x + 1y +(x, h()) -> x 2 + 0x >= 1x a(h(), h(), h(), x) -> s x 4 + 1x >= 1 + 1x a(s l, h(), h(), z) -> a(l, z, h(), z) 4 + 1l + 1z >= 2 + 1l + 2z a(l, s x, h(), z) -> a(l, x, z, z) 3 + 1x + 1l + 1z >= 1 + 1x + 1l + 2z a(l, x, s y, h()) -> a(l, x, y, s h()) 3 + 1x + 1l + 1y >= 3 + 1x + 1l + 1y a(l, x, s y, s z) -> a(l, x, y, a(l, x, s y, z)) 3 + 1x + 1l + 1y + 1z >= 3 + 2x + 2l + 2y + 1z s h() -> 1() 2 >= 0 Qed