YES Time: 0.026895 TRS: { f nil() -> nil(), f .(nil(), y) -> .(nil(), f y), f .(.(x, y), z) -> f .(x, .(y, z)), g nil() -> nil(), g .(x, nil()) -> .(g x, nil()), g .(x, .(y, z)) -> g .(.(x, y), z)} DP: DP: { f# .(nil(), y) -> f# y, f# .(.(x, y), z) -> f# .(x, .(y, z)), g# .(x, nil()) -> g# x, g# .(x, .(y, z)) -> g# .(.(x, y), z)} TRS: { f nil() -> nil(), f .(nil(), y) -> .(nil(), f y), f .(.(x, y), z) -> f .(x, .(y, z)), g nil() -> nil(), g .(x, nil()) -> .(g x, nil()), g .(x, .(y, z)) -> g .(.(x, y), z)} EDG: {(g# .(x, nil()) -> g# x, g# .(x, .(y, z)) -> g# .(.(x, y), z)) (g# .(x, nil()) -> g# x, g# .(x, nil()) -> g# x) (g# .(x, .(y, z)) -> g# .(.(x, y), z), g# .(x, .(y, z)) -> g# .(.(x, y), z)) (g# .(x, .(y, z)) -> g# .(.(x, y), z), g# .(x, nil()) -> g# x) (f# .(.(x, y), z) -> f# .(x, .(y, z)), f# .(nil(), y) -> f# y) (f# .(.(x, y), z) -> f# .(x, .(y, z)), f# .(.(x, y), z) -> f# .(x, .(y, z))) (f# .(nil(), y) -> f# y, f# .(nil(), y) -> f# y) (f# .(nil(), y) -> f# y, f# .(.(x, y), z) -> f# .(x, .(y, z)))} SCCS (2): Scc: { g# .(x, nil()) -> g# x, g# .(x, .(y, z)) -> g# .(.(x, y), z)} Scc: { f# .(nil(), y) -> f# y, f# .(.(x, y), z) -> f# .(x, .(y, z))} SCC (2): Strict: { g# .(x, nil()) -> g# x, g# .(x, .(y, z)) -> g# .(.(x, y), z)} Weak: { f nil() -> nil(), f .(nil(), y) -> .(nil(), f y), f .(.(x, y), z) -> f .(x, .(y, z)), g nil() -> nil(), g .(x, nil()) -> .(g x, nil()), g .(x, .(y, z)) -> g .(.(x, y), z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [.](x0, x1) = x0 + x1, [f](x0) = 0, [g](x0) = x0 + 1, [nil] = 1, [g#](x0) = x0 Strict: g# .(x, .(y, z)) -> g# .(.(x, y), z) 0 + 1y + 1x + 1z >= 0 + 1y + 1x + 1z g# .(x, nil()) -> g# x 1 + 1x >= 0 + 1x Weak: EDG: {(g# .(x, .(y, z)) -> g# .(.(x, y), z), g# .(x, .(y, z)) -> g# .(.(x, y), z))} SCCS (1): Scc: {g# .(x, .(y, z)) -> g# .(.(x, y), z)} SCC (1): Strict: {g# .(x, .(y, z)) -> g# .(.(x, y), z)} Weak: { f nil() -> nil(), f .(nil(), y) -> .(nil(), f y), f .(.(x, y), z) -> f .(x, .(y, z)), g nil() -> nil(), g .(x, nil()) -> .(g x, nil()), g .(x, .(y, z)) -> g .(.(x, y), z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [.](x0, x1) = x0 + 1, [f](x0) = 0, [g](x0) = x0 + 1, [nil] = 1, [g#](x0) = x0 Strict: g# .(x, .(y, z)) -> g# .(.(x, y), z) 2 + 0y + 0x + 1z >= 1 + 0y + 0x + 1z Weak: Qed SCC (2): Strict: { f# .(nil(), y) -> f# y, f# .(.(x, y), z) -> f# .(x, .(y, z))} Weak: { f nil() -> nil(), f .(nil(), y) -> .(nil(), f y), f .(.(x, y), z) -> f .(x, .(y, z)), g nil() -> nil(), g .(x, nil()) -> .(g x, nil()), g .(x, .(y, z)) -> g .(.(x, y), z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [.](x0, x1) = x0 + x1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [nil] = 1, [f#](x0) = x0 Strict: f# .(.(x, y), z) -> f# .(x, .(y, z)) 0 + 1y + 1x + 1z >= 0 + 1y + 1x + 1z f# .(nil(), y) -> f# y 1 + 1y >= 0 + 1y Weak: EDG: {(f# .(.(x, y), z) -> f# .(x, .(y, z)), f# .(.(x, y), z) -> f# .(x, .(y, z)))} SCCS (1): Scc: {f# .(.(x, y), z) -> f# .(x, .(y, z))} SCC (1): Strict: {f# .(.(x, y), z) -> f# .(x, .(y, z))} Weak: { f nil() -> nil(), f .(nil(), y) -> .(nil(), f y), f .(.(x, y), z) -> f .(x, .(y, z)), g nil() -> nil(), g .(x, nil()) -> .(g x, nil()), g .(x, .(y, z)) -> g .(.(x, y), z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [.](x0, x1) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [nil] = 1, [f#](x0) = x0 Strict: f# .(.(x, y), z) -> f# .(x, .(y, z)) 2 + 0y + 1x + 0z >= 1 + 0y + 1x + 0z Weak: Qed