YES Time: 0.042959 TRS: { a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark s X -> s mark X, mark from X -> a__from mark X, a__from X -> cons(mark X, from s X), a__from X -> from X} DP: DP: {a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X, mark# from X -> mark# X, mark# from X -> a__from# mark X, a__from# X -> mark# X} TRS: { a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark s X -> s mark X, mark from X -> a__from mark X, a__from X -> cons(mark X, from s X), a__from X -> from X} EDG: {(mark# from X -> mark# X, mark# from X -> a__from# mark X) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# s X -> mark# X) (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X2) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> mark# X1) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# first(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# first(X1, X2) -> a__first#(mark X1, mark X2), a__first#(s X, cons(Y, Z)) -> mark# Y) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__from# X -> mark# X, mark# first(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# first(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# s X -> mark# X) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# from X -> a__from# mark X)} STATUS: arrows: 0.370370 SCCS (1): Scc: {a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X, mark# from X -> mark# X, mark# from X -> a__from# mark X, a__from# X -> mark# X} SCC (9): Strict: {a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X, mark# from X -> mark# X, mark# from X -> a__from# mark X, a__from# X -> mark# X} Weak: { a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark s X -> s mark X, mark from X -> a__from mark X, a__from X -> cons(mark X, from s X), a__from X -> from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__first](x0, x1) = x0 + x1, [cons](x0, x1) = x0, [first](x0, x1) = x0 + x1, [mark](x0) = x0, [s](x0) = x0 + 1, [from](x0) = x0, [a__from](x0) = x0, [nil] = 0, [0] = 0, [a__first#](x0, x1) = x0, [mark#](x0) = x0, [a__from#](x0) = x0 Strict: a__from# X -> mark# X 0 + 1X >= 0 + 1X mark# from X -> a__from# mark X 0 + 1X >= 0 + 1X mark# from X -> mark# X 0 + 1X >= 0 + 1X mark# s X -> mark# X 1 + 1X >= 0 + 1X mark# first(X1, X2) -> mark# X2 0 + 1X1 + 1X2 >= 0 + 1X2 mark# first(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 mark# first(X1, X2) -> a__first#(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 0X2 >= 0 + 1X1 a__first#(s X, cons(Y, Z)) -> mark# Y 0 + 0X + 1Y + 0Z >= 0 + 1Y Weak: a__from X -> from X 0 + 1X >= 0 + 1X a__from X -> cons(mark X, from s X) 0 + 1X >= 0 + 1X mark from X -> a__from mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 1 + 1X >= 1 + 1X mark first(X1, X2) -> a__first(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 mark 0() -> 0() 0 >= 0 mark nil() -> nil() 0 >= 0 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 1 + 1X + 1Y + 0Z >= 0 + 0X + 1Y + 0Z a__first(0(), X) -> nil() 0 + 1X >= 0 a__first(X1, X2) -> first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 SCCS (1): Scc: {a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X, mark# from X -> a__from# mark X, a__from# X -> mark# X} SCC (8): Strict: {a__first#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X, mark# from X -> a__from# mark X, a__from# X -> mark# X} Weak: { a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark s X -> s mark X, mark from X -> a__from mark X, a__from X -> cons(mark X, from s X), a__from X -> from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__first](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0, [first](x0, x1) = x0 + x1 + 1, [mark](x0) = x0, [s](x0) = 0, [from](x0) = x0, [a__from](x0) = x0, [nil] = 0, [0] = 0, [a__first#](x0, x1) = x0, [mark#](x0) = x0, [a__from#](x0) = x0 Strict: a__from# X -> mark# X 0 + 1X >= 0 + 1X mark# from X -> a__from# mark X 0 + 1X >= 0 + 1X mark# from X -> mark# X 0 + 1X >= 0 + 1X mark# first(X1, X2) -> mark# X2 1 + 1X1 + 1X2 >= 0 + 1X2 mark# first(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 mark# first(X1, X2) -> a__first#(mark X1, mark X2) 1 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 0X2 >= 0 + 1X1 a__first#(s X, cons(Y, Z)) -> mark# Y 0 + 0X + 1Y + 0Z >= 0 + 1Y Weak: a__from X -> from X 0 + 1X >= 0 + 1X a__from X -> cons(mark X, from s X) 0 + 1X >= 0 + 1X mark from X -> a__from mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 0 + 0X >= 0 + 0X mark first(X1, X2) -> a__first(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 mark 0() -> 0() 0 >= 0 mark nil() -> nil() 0 >= 0 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 1 + 0X + 1Y + 0Z >= 0 + 0X + 1Y + 0Z a__first(0(), X) -> nil() 1 + 1X >= 0 a__first(X1, X2) -> first(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 SCCS (1): Scc: {mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, a__from# X -> mark# X} SCC (4): Strict: {mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, a__from# X -> mark# X} Weak: { a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark s X -> s mark X, mark from X -> a__from mark X, a__from X -> cons(mark X, from s X), a__from X -> from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__first](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + x1, [first](x0, x1) = x0 + 1, [mark](x0) = x0, [s](x0) = 0, [from](x0) = x0 + 1, [a__from](x0) = x0 + 1, [nil] = 0, [0] = 0, [mark#](x0) = x0, [a__from#](x0) = x0 + 1 Strict: a__from# X -> mark# X 1 + 1X >= 0 + 1X mark# from X -> a__from# mark X 1 + 1X >= 1 + 1X mark# from X -> mark# X 1 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: a__from X -> from X 1 + 1X >= 1 + 1X a__from X -> cons(mark X, from s X) 1 + 1X >= 1 + 1X mark from X -> a__from mark X 1 + 1X >= 1 + 1X mark s X -> s mark X 0 + 0X >= 0 + 0X mark first(X1, X2) -> a__first(mark X1, mark X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark 0() -> 0() 0 >= 0 mark nil() -> nil() 0 >= 0 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 1 + 0X + 1Y + 1Z >= 1 + 0X + 1Y + 1Z a__first(0(), X) -> nil() 1 + 1X >= 0 a__first(X1, X2) -> first(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 SCCS (1): Scc: {mark# cons(X1, X2) -> mark# X1} SCC (1): Strict: {mark# cons(X1, X2) -> mark# X1} Weak: { a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark s X -> s mark X, mark from X -> a__from mark X, a__from X -> cons(mark X, from s X), a__from X -> from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__first](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + x1 + 1, [first](x0, x1) = 0, [mark](x0) = 0, [s](x0) = 0, [from](x0) = 1, [a__from](x0) = 0, [nil] = 0, [0] = 1, [mark#](x0) = x0 Strict: mark# cons(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 Weak: a__from X -> from X 0 + 0X >= 1 + 0X a__from X -> cons(mark X, from s X) 0 + 0X >= 2 + 0X mark from X -> a__from mark X 0 + 0X >= 0 + 0X mark s X -> s mark X 0 + 0X >= 0 + 0X mark first(X1, X2) -> a__first(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 mark 0() -> 0() 0 >= 1 mark nil() -> nil() 0 >= 0 a__first(s X, cons(Y, Z)) -> cons(mark Y, first(X, Z)) 2 + 0X + 1Y + 1Z >= 1 + 0X + 0Y + 0Z a__first(0(), X) -> nil() 2 + 1X >= 0 a__first(X1, X2) -> first(X1, X2) 1 + 1X1 + 1X2 >= 0 + 0X1 + 0X2 Qed