YES Time: 1.065314 TRS: { mark true() -> true(), mark false() -> false(), mark 0() -> 0(), mark s X -> s X, mark add(X1, X2) -> a__add(mark X1, X2), mark nil() -> nil(), mark cons(X1, X2) -> cons(X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark from X -> a__from X, mark and(X1, X2) -> a__and(mark X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3), a__and(X1, X2) -> and(X1, X2), a__and(true(), X) -> mark X, a__and(false(), Y) -> false(), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark X, a__add(s X, Y) -> s add(X, Y), a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)), a__from X -> cons(X, from s X), a__from X -> from X} DP: DP: { mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2), mark# from X -> a__from# X, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__and#(true(), X) -> mark# X, a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, a__add#(0(), X) -> mark# X} TRS: { mark true() -> true(), mark false() -> false(), mark 0() -> 0(), mark s X -> s X, mark add(X1, X2) -> a__add(mark X1, X2), mark nil() -> nil(), mark cons(X1, X2) -> cons(X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark from X -> a__from X, mark and(X1, X2) -> a__and(mark X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3), a__and(X1, X2) -> and(X1, X2), a__and(true(), X) -> mark X, a__and(false(), Y) -> false(), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark X, a__add(s X, Y) -> s add(X, Y), a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)), a__from X -> cons(X, from s X), a__from X -> from X} EDG: {(mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# from X -> a__from# X) (mark# first(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# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# from X -> a__from# X) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# from X -> a__from# X) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (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# add(X1, X2) -> a__add#(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__if#(true(), X, Y) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# from X -> a__from# X) (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> a__add#(mark X1, X2), a__add#(0(), X) -> mark# X) (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y) (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(true(), X, Y) -> mark# X) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(true(), X) -> mark# X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# from X -> a__from# X) (a__add#(0(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__and#(true(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__and#(true(), X) -> mark# X, mark# from X -> a__from# X) (a__and#(true(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(true(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X2) (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__if#(false(), X, Y) -> mark# Y, mark# from X -> a__from# X) (a__if#(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# from X -> a__from# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# from X -> a__from# X) (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))} EDG: {(mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# from X -> a__from# X) (mark# first(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# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# from X -> a__from# X) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# from X -> a__from# X) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (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# add(X1, X2) -> a__add#(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__if#(true(), X, Y) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# from X -> a__from# X) (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__if#(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__if#(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> a__add#(mark X1, X2), a__add#(0(), X) -> mark# X) (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y) (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(true(), X, Y) -> mark# X) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(true(), X) -> mark# X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# from X -> a__from# X) (a__add#(0(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__and#(true(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (a__and#(true(), X) -> mark# X, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__and#(true(), X) -> mark# X, mark# from X -> a__from# X) (a__and#(true(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(true(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (a__and#(true(), X) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, X2)) (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X2) (a__if#(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (a__if#(false(), X, Y) -> mark# Y, mark# from X -> a__from# X) (a__if#(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# from X -> a__from# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> a__first#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# from X -> a__from# X) (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))} STATUS: arrows: 0.520408 SCCS (1): Scc: { mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__and#(true(), X) -> mark# X, a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, a__add#(0(), X) -> mark# X} SCC (12): Strict: { mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, X2), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__and#(true(), X) -> mark# X, a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, a__add#(0(), X) -> mark# X} Weak: { mark true() -> true(), mark false() -> false(), mark 0() -> 0(), mark s X -> s X, mark add(X1, X2) -> a__add(mark X1, X2), mark nil() -> nil(), mark cons(X1, X2) -> cons(X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark from X -> a__from X, mark and(X1, X2) -> a__and(mark X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3), a__and(X1, X2) -> and(X1, X2), a__and(true(), X) -> mark X, a__and(false(), Y) -> false(), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark X, a__add(s X, Y) -> s add(X, Y), a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)), a__from X -> cons(X, from s X), a__from X -> from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = x0 + x1 + x2 + 1, [if](x0, x1, x2) = x0 + x1 + x2 + 1, [a__and](x0, x1) = x0 + x1, [a__add](x0, x1) = x0 + x1, [add](x0, x1) = x0 + x1, [a__first](x0, x1) = x0 + x1, [cons](x0, x1) = 0, [first](x0, x1) = x0 + x1, [and](x0, x1) = x0 + x1, [mark](x0) = x0, [s](x0) = 1, [from](x0) = 0, [a__from](x0) = 0, [true] = 1, [false] = 1, [0] = 1, [nil] = 0, [a__if#](x0, x1, x2) = x0 + x1 + x2 + 1, [a__and#](x0, x1) = x0 + x1, [a__add#](x0, x1) = x0 + x1, [mark#](x0) = x0 Strict: a__add#(0(), X) -> mark# X 1 + 1X >= 0 + 1X a__if#(false(), X, Y) -> mark# Y 2 + 1X + 1Y >= 0 + 1Y a__if#(true(), X, Y) -> mark# X 2 + 1X + 1Y >= 0 + 1X a__and#(true(), X) -> mark# X 1 + 1X >= 0 + 1X mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark# if(X1, X2, X3) -> mark# X1 1 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 mark# and(X1, X2) -> a__and#(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark# and(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 mark# first(X1, X2) -> mark# X2 0 + 1X1 + 1X2 >= 0 + 1X2 mark# first(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 mark# add(X1, X2) -> a__add#(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark# add(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: a__from X -> from X 0 + 0X >= 0 + 0X a__from X -> cons(X, from s X) 0 + 0X >= 0 + 0X a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)) 1 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z a__first(0(), X) -> nil() 1 + 1X >= 0 a__first(X1, X2) -> first(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 a__add(s X, Y) -> s add(X, Y) 1 + 0X + 1Y >= 1 + 0X + 0Y a__add(0(), X) -> mark X 1 + 1X >= 0 + 1X a__add(X1, X2) -> add(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 a__if(false(), X, Y) -> mark Y 2 + 1X + 1Y >= 0 + 1Y a__if(true(), X, Y) -> mark X 2 + 1X + 1Y >= 0 + 1X a__if(X1, X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 a__and(false(), Y) -> false() 1 + 1Y >= 1 a__and(true(), X) -> mark X 1 + 1X >= 0 + 1X a__and(X1, X2) -> and(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark and(X1, X2) -> a__and(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark from X -> a__from X 0 + 0X >= 0 + 0X mark first(X1, X2) -> a__first(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark cons(X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark nil() -> nil() 0 >= 0 mark add(X1, X2) -> a__add(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark s X -> s X 1 + 0X >= 1 + 0X mark 0() -> 0() 1 >= 1 mark false() -> false() 1 >= 1 mark true() -> true() 1 >= 1 SCCS (1): Scc: { mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1} SCC (4): Strict: { mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1} Weak: { mark true() -> true(), mark false() -> false(), mark 0() -> 0(), mark s X -> s X, mark add(X1, X2) -> a__add(mark X1, X2), mark nil() -> nil(), mark cons(X1, X2) -> cons(X1, X2), mark first(X1, X2) -> a__first(mark X1, mark X2), mark from X -> a__from X, mark and(X1, X2) -> a__and(mark X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3), a__and(X1, X2) -> and(X1, X2), a__and(true(), X) -> mark X, a__and(false(), Y) -> false(), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark X, a__add(s X, Y) -> s add(X, Y), a__first(X1, X2) -> first(X1, X2), a__first(0(), X) -> nil(), a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)), a__from X -> cons(X, from s X), a__from X -> from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = x0 + 1, [if](x0, x1, x2) = 1, [a__and](x0, x1) = x0 + 1, [a__add](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [a__first](x0, x1) = 0, [cons](x0, x1) = 1, [first](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [s](x0) = 1, [from](x0) = 1, [a__from](x0) = 0, [true] = 1, [false] = 1, [0] = 1, [nil] = 1, [mark#](x0) = x0 + 1 Strict: mark# and(X1, X2) -> mark# X1 2 + 1X1 + 0X2 >= 1 + 1X1 mark# first(X1, X2) -> mark# X2 2 + 1X1 + 1X2 >= 1 + 1X2 mark# first(X1, X2) -> mark# X1 2 + 1X1 + 1X2 >= 1 + 1X1 mark# add(X1, X2) -> mark# X1 2 + 1X1 + 0X2 >= 1 + 1X1 Weak: a__from X -> from X 0 + 0X >= 1 + 0X a__from X -> cons(X, from s X) 0 + 0X >= 1 + 0X a__first(s X, cons(Y, Z)) -> cons(Y, first(X, Z)) 0 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z a__first(0(), X) -> nil() 0 + 0X >= 1 a__first(X1, X2) -> first(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2 a__add(s X, Y) -> s add(X, Y) 2 + 0X + 0Y >= 1 + 0X + 0Y a__add(0(), X) -> mark X 2 + 0X >= 1 + 1X a__add(X1, X2) -> add(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 a__if(false(), X, Y) -> mark Y 2 + 0X + 0Y >= 1 + 1Y a__if(true(), X, Y) -> mark X 2 + 0X + 0Y >= 1 + 1X a__if(X1, X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 a__and(false(), Y) -> false() 2 + 0Y >= 1 a__and(true(), X) -> mark X 2 + 0X >= 1 + 1X a__and(X1, X2) -> and(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 2 + 1X1 + 0X2 + 0X3 mark and(X1, X2) -> a__and(mark X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 mark from X -> a__from X 2 + 0X >= 0 + 0X mark first(X1, X2) -> a__first(mark X1, mark X2) 2 + 1X1 + 1X2 >= 0 + 0X1 + 0X2 mark cons(X1, X2) -> cons(X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark nil() -> nil() 2 >= 1 mark add(X1, X2) -> a__add(mark X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2 mark s X -> s X 2 + 0X >= 1 + 0X mark 0() -> 0() 2 >= 1 mark false() -> false() 2 >= 1 mark true() -> true() 2 >= 1 Qed