YES Time: 0.022387 TRS: { lambda x -> x, a(x, y) -> x, a(x, y) -> y, a(lambda x, y) -> lambda a(x, a(y, t())), a(lambda x, y) -> lambda a(x, 1()), a(a(x, y), z) -> a(x, a(y, z))} DP: DP: {a#(lambda x, y) -> lambda# a(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, 1()), a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)} TRS: { lambda x -> x, a(x, y) -> x, a(x, y) -> y, a(lambda x, y) -> lambda a(x, a(y, t())), a(lambda x, y) -> lambda a(x, 1()), a(a(x, y), z) -> a(x, a(y, z))} UR: { lambda x -> x, a(x, y) -> x, a(x, y) -> y, a(lambda x, y) -> lambda a(x, a(y, t())), a(lambda x, y) -> lambda a(x, 1()), a(a(x, y), z) -> a(x, a(y, z))} EDG: {(a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(y, z))} EDG: {(a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(y, z))} EDG: {(a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(y, z))} EDG: {(a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(y, t()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(y, z), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(y, z), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, a(y, t())), a#(a(x, y), z) -> a#(y, z)) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> lambda# a(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(x, 1())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(lambda x, y) -> a#(y, t())) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> lambda# a(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, a(y, t()))) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(x, 1())) (a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t())) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(x, a(y, z))) (a#(lambda x, y) -> a#(x, 1()), a#(a(x, y), z) -> a#(y, z))} STATUS: arrows: 0.285714 SCCS (1): Scc: {a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)} SCC (5): Strict: {a#(lambda x, y) -> a#(x, a(y, t())), a#(lambda x, y) -> a#(x, 1()), a#(lambda x, y) -> a#(y, t()), a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)} Weak: { lambda x -> x, a(x, y) -> x, a(x, y) -> y, a(lambda x, y) -> lambda a(x, a(y, t())), a(lambda x, y) -> lambda a(x, 1()), a(a(x, y), z) -> a(x, a(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1) = x0 + x1, [lambda](x0) = x0 + 1, [1] = 0, [t] = 0, [a#](x0, x1) = x0 + x1 Strict: a#(a(x, y), z) -> a#(y, z) 0 + 1x + 1y + 1z >= 0 + 1y + 1z a#(a(x, y), z) -> a#(x, a(y, z)) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z a#(lambda x, y) -> a#(y, t()) 1 + 1x + 1y >= 0 + 1y a#(lambda x, y) -> a#(x, 1()) 1 + 1x + 1y >= 0 + 1x a#(lambda x, y) -> a#(x, a(y, t())) 1 + 1x + 1y >= 0 + 1x + 1y Weak: a(a(x, y), z) -> a(x, a(y, z)) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z a(lambda x, y) -> lambda a(x, 1()) 1 + 1x + 1y >= 1 + 1x a(lambda x, y) -> lambda a(x, a(y, t())) 1 + 1x + 1y >= 1 + 1x + 1y a(x, y) -> y 0 + 1x + 1y >= 1y a(x, y) -> x 0 + 1x + 1y >= 1x lambda x -> x 1 + 1x >= 1x SCCS (1): Scc: {a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)} SCC (2): Strict: {a#(a(x, y), z) -> a#(x, a(y, z)), a#(a(x, y), z) -> a#(y, z)} Weak: { lambda x -> x, a(x, y) -> x, a(x, y) -> y, a(lambda x, y) -> lambda a(x, a(y, t())), a(lambda x, y) -> lambda a(x, 1()), a(a(x, y), z) -> a(x, a(y, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a](x0, x1) = x0 + x1 + 1, [lambda](x0) = 0, [1] = 1, [t] = 1, [a#](x0, x1) = x0 Strict: a#(a(x, y), z) -> a#(y, z) 1 + 1x + 1y + 0z >= 0 + 1y + 0z a#(a(x, y), z) -> a#(x, a(y, z)) 1 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z Weak: a(a(x, y), z) -> a(x, a(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z a(lambda x, y) -> lambda a(x, 1()) 1 + 0x + 1y >= 0 + 0x a(lambda x, y) -> lambda a(x, a(y, t())) 1 + 0x + 1y >= 0 + 0x + 0y a(x, y) -> y 1 + 1x + 1y >= 1y a(x, y) -> x 1 + 1x + 1y >= 1x lambda x -> x 0 + 0x >= 1x Qed