YES Time: 0.064799 TRS: {:(z, +(x, f y)) -> :(g(z, y), +(x, a())), :(:(x, y), z) -> :(x, :(y, z)), :(+(x, y), z) -> +(:(x, z), :(y, z))} DP: DP: {:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(y, z)} TRS: {:(z, +(x, f y)) -> :(g(z, y), +(x, a())), :(:(x, y), z) -> :(x, :(y, z)), :(+(x, y), z) -> +(:(x, z), :(y, z))} UR: {:(z, +(x, f y)) -> :(g(z, y), +(x, a())), :(:(x, y), z) -> :(x, :(y, z)), :(+(x, y), z) -> +(:(x, z), :(y, z)), b(w, v) -> w, b(w, v) -> v} EDG: {(:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(+(x, y), z) -> :#(y, z)) (:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(+(x, y), z) -> :#(x, z)) (:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(:(x, y), z) -> :#(y, z)) (:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(:(x, y), z) -> :#(x, :(y, z))) (:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a()))) (:#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(y, z)) (:#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(x, z)) (:#(+(x, y), z) -> :#(x, z), :#(:(x, y), z) -> :#(y, z)) (:#(+(x, y), z) -> :#(x, z), :#(:(x, y), z) -> :#(x, :(y, z))) (:#(+(x, y), z) -> :#(x, z), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a()))) (:#(+(x, y), z) -> :#(y, z), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a()))) (:#(+(x, y), z) -> :#(y, z), :#(:(x, y), z) -> :#(x, :(y, z))) (:#(+(x, y), z) -> :#(y, z), :#(:(x, y), z) -> :#(y, z)) (:#(+(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(x, z)) (:#(+(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(y, z)) (:#(:(x, y), z) -> :#(y, z), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a()))) (:#(:(x, y), z) -> :#(y, z), :#(:(x, y), z) -> :#(x, :(y, z))) (:#(:(x, y), z) -> :#(y, z), :#(:(x, y), z) -> :#(y, z)) (:#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(x, z)) (:#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(y, z)) (:#(:(x, y), z) -> :#(x, :(y, z)), :#(z, +(x, f y)) -> :#(g(z, y), +(x, a()))) (:#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(x, :(y, z))) (:#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z)) (:#(:(x, y), z) -> :#(x, :(y, z)), :#(+(x, y), z) -> :#(x, z)) (:#(:(x, y), z) -> :#(x, :(y, z)), :#(+(x, y), z) -> :#(y, z))} STATUS: arrows: 0.000000 SCCS (1): Scc: {:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(y, z)} SCC (5): Strict: {:#(z, +(x, f y)) -> :#(g(z, y), +(x, a())), :#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(y, z)} Weak: {:(z, +(x, f y)) -> :(g(z, y), +(x, a())), :(:(x, y), z) -> :(x, :(y, z)), :(+(x, y), z) -> +(:(x, z), :(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [:](x0, x1) = 0, [+](x0, x1) = x0, [g](x0, x1) = 0, [f](x0) = 1, [a] = 0, [:#](x0, x1) = x0 Strict: :#(+(x, y), z) -> :#(y, z) 0 + 0x + 0y + 1z >= 0 + 0y + 1z :#(+(x, y), z) -> :#(x, z) 0 + 0x + 0y + 1z >= 0 + 0x + 1z :#(:(x, y), z) -> :#(y, z) 0 + 0x + 0y + 1z >= 0 + 0y + 1z :#(:(x, y), z) -> :#(x, :(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 0z :#(z, +(x, f y)) -> :#(g(z, y), +(x, a())) 1 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z Weak: :(+(x, y), z) -> +(:(x, z), :(y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z :(:(x, y), z) -> :(x, :(y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z :(z, +(x, f y)) -> :(g(z, y), +(x, a())) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z SCCS (1): Scc: {:#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(y, z)} SCC (4): Strict: {:#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z), :#(+(x, y), z) -> :#(x, z), :#(+(x, y), z) -> :#(y, z)} Weak: {:(z, +(x, f y)) -> :(g(z, y), +(x, a())), :(:(x, y), z) -> :(x, :(y, z)), :(+(x, y), z) -> +(:(x, z), :(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [:](x0, x1) = x0 + x1, [+](x0, x1) = x0 + x1 + 1, [g](x0, x1) = 0, [f](x0) = 1, [a] = 0, [:#](x0, x1) = x0 Strict: :#(+(x, y), z) -> :#(y, z) 1 + 1x + 1y + 0z >= 0 + 1y + 0z :#(+(x, y), z) -> :#(x, z) 1 + 1x + 1y + 0z >= 0 + 1x + 0z :#(:(x, y), z) -> :#(y, z) 0 + 1x + 1y + 0z >= 0 + 1y + 0z :#(:(x, y), z) -> :#(x, :(y, z)) 0 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z Weak: :(+(x, y), z) -> +(:(x, z), :(y, z)) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 2z :(:(x, y), z) -> :(x, :(y, z)) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z :(z, +(x, f y)) -> :(g(z, y), +(x, a())) 2 + 1x + 0y + 1z >= 1 + 1x + 0y + 0z SCCS (1): Scc: {:#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z)} SCC (2): Strict: {:#(:(x, y), z) -> :#(x, :(y, z)), :#(:(x, y), z) -> :#(y, z)} Weak: {:(z, +(x, f y)) -> :(g(z, y), +(x, a())), :(:(x, y), z) -> :(x, :(y, z)), :(+(x, y), z) -> +(:(x, z), :(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [:](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + 1, [g](x0, x1) = 1, [f](x0) = 0, [a] = 1, [:#](x0, x1) = x0 Strict: :#(:(x, y), z) -> :#(y, z) 1 + 1x + 1y + 0z >= 0 + 1y + 0z :#(:(x, y), z) -> :#(x, :(y, z)) 1 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z Weak: :(+(x, y), z) -> +(:(x, z), :(y, z)) 2 + 0x + 1y + 1z >= 2 + 0x + 1y + 1z :(:(x, y), z) -> :(x, :(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z :(z, +(x, f y)) -> :(g(z, y), +(x, a())) 2 + 0x + 0y + 1z >= 4 + 0x + 0y + 0z Qed