MAYBE Time: 0.013750 TRS: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s X, cons(Y, Z)) -> cons(mark Y, fst(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark fst(X1, X2) -> a__fst(mark X1, mark X2), mark s X -> s X, mark from X -> a__from mark X, mark add(X1, X2) -> a__add(mark X1, mark X2), mark len X -> a__len mark X, a__from X -> cons(mark X, from s X), a__from X -> from X, a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark X, a__add(s X, Y) -> s add(X, Y), a__len X -> len X, a__len nil() -> 0(), a__len cons(X, Z) -> s len Z} DP: DP: {a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2), mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# len X -> mark# X, mark# len X -> a__len# mark X, a__from# X -> mark# X, a__add#(0(), X) -> mark# X} TRS: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s X, cons(Y, Z)) -> cons(mark Y, fst(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark fst(X1, X2) -> a__fst(mark X1, mark X2), mark s X -> s X, mark from X -> a__from mark X, mark add(X1, X2) -> a__add(mark X1, mark X2), mark len X -> a__len mark X, a__from X -> cons(mark X, from s X), a__from X -> from X, a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark X, a__add(s X, Y) -> s add(X, Y), a__len X -> len X, a__len nil() -> 0(), a__len cons(X, Z) -> s len Z} EDG: {(mark# fst(X1, X2) -> mark# X1, mark# len X -> a__len# mark X) (mark# fst(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# fst(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# len X -> a__len# mark X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# len X -> mark# X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X2) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> mark# X2) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# len X -> a__len# mark X) (mark# add(X1, X2) -> mark# X2, mark# len X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# add(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# len X -> a__len# mark X) (mark# from X -> mark# X, mark# len X -> mark# X) (mark# from X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# from X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# add(X1, X2) -> mark# X1) (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# fst(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# fst(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# len X -> a__len# mark X) (mark# len X -> mark# X, mark# len X -> mark# X) (mark# len X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# len X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# len X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# from X -> a__from# mark X) (mark# len X -> mark# X, mark# from X -> mark# X) (mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X2) (mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# len X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# len X -> a__len# mark X) (a__add#(0(), X) -> mark# X, mark# len X -> mark# X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# from X -> a__from# mark X) (a__add#(0(), X) -> mark# X, mark# from X -> mark# X) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__from# X -> mark# X, mark# fst(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# fst(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# add(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# add(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__from# X -> mark# X, mark# len X -> mark# X) (a__from# X -> mark# X, mark# len X -> a__len# mark X) (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> mark# X) (mark# fst(X1, X2) -> a__fst#(mark X1, mark X2), a__fst#(s X, cons(Y, Z)) -> mark# Y) (mark# fst(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# fst(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X2, mark# len X -> mark# X) (mark# fst(X1, X2) -> mark# X2, mark# len X -> a__len# mark X) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# len X -> a__len# mark X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (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# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# len X -> a__len# mark X)} EDG: {(mark# fst(X1, X2) -> mark# X1, mark# len X -> a__len# mark X) (mark# fst(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# fst(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# len X -> a__len# mark X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# len X -> mark# X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X2) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> mark# X2) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# len X -> a__len# mark X) (mark# add(X1, X2) -> mark# X2, mark# len X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# add(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# len X -> a__len# mark X) (mark# from X -> mark# X, mark# len X -> mark# X) (mark# from X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# from X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# add(X1, X2) -> mark# X1) (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# fst(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# fst(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# len X -> a__len# mark X) (mark# len X -> mark# X, mark# len X -> mark# X) (mark# len X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# len X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# len X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# from X -> a__from# mark X) (mark# len X -> mark# X, mark# from X -> mark# X) (mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X2) (mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# len X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# len X -> a__len# mark X) (a__add#(0(), X) -> mark# X, mark# len X -> mark# X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# from X -> a__from# mark X) (a__add#(0(), X) -> mark# X, mark# from X -> mark# X) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__from# X -> mark# X, mark# fst(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# fst(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# add(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# add(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__from# X -> mark# X, mark# len X -> mark# X) (a__from# X -> mark# X, mark# len X -> a__len# mark X) (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> mark# X) (mark# fst(X1, X2) -> a__fst#(mark X1, mark X2), a__fst#(s X, cons(Y, Z)) -> mark# Y) (mark# fst(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# fst(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X2, mark# len X -> mark# X) (mark# fst(X1, X2) -> mark# X2, mark# len X -> a__len# mark X) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# len X -> a__len# mark X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (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# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# len X -> a__len# mark X)} EDG: {(mark# fst(X1, X2) -> mark# X1, mark# len X -> a__len# mark X) (mark# fst(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# fst(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# len X -> a__len# mark X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# len X -> mark# X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X2) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# add(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> mark# X2) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> mark# X1) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# len X -> a__len# mark X) (mark# add(X1, X2) -> mark# X2, mark# len X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# add(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# len X -> a__len# mark X) (mark# from X -> mark# X, mark# len X -> mark# X) (mark# from X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# from X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# add(X1, X2) -> mark# X1) (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# fst(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# fst(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# len X -> a__len# mark X) (mark# len X -> mark# X, mark# len X -> mark# X) (mark# len X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# len X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# len X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# from X -> a__from# mark X) (mark# len X -> mark# X, mark# from X -> mark# X) (mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X2) (mark# len X -> mark# X, mark# fst(X1, X2) -> mark# X1) (mark# len X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# len X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# len X -> a__len# mark X) (a__add#(0(), X) -> mark# X, mark# len X -> mark# X) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# from X -> a__from# mark X) (a__add#(0(), X) -> mark# X, mark# from X -> mark# X) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X2) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> mark# X1) (a__add#(0(), X) -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__add#(0(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (a__from# X -> mark# X, mark# fst(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# fst(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# add(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# add(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (a__from# X -> mark# X, mark# len X -> mark# X) (a__from# X -> mark# X, mark# len X -> a__len# mark X) (mark# add(X1, X2) -> a__add#(mark X1, mark X2), a__add#(0(), X) -> mark# X) (mark# fst(X1, X2) -> a__fst#(mark X1, mark X2), a__fst#(s X, cons(Y, Z)) -> mark# Y) (mark# fst(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# fst(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# fst(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# fst(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# fst(X1, X2) -> mark# X2, mark# len X -> mark# X) (mark# fst(X1, X2) -> mark# X2, mark# len X -> a__len# mark X) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# len X -> a__len# mark X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2) (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# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# add(X1, X2) -> a__add#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# len X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# len X -> a__len# mark X)} STATUS: arrows: 0.423469 SCCS (1): Scc: {a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2), mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# len X -> mark# X, a__from# X -> mark# X, a__add#(0(), X) -> mark# X} SCC (13): Strict: {a__fst#(s X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1, mark# fst(X1, X2) -> a__fst#(mark X1, mark X2), mark# fst(X1, X2) -> mark# X1, mark# fst(X1, X2) -> mark# X2, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> a__add#(mark X1, mark X2), mark# len X -> mark# X, a__from# X -> mark# X, a__add#(0(), X) -> mark# X} Weak: { a__fst(X1, X2) -> fst(X1, X2), a__fst(0(), Z) -> nil(), a__fst(s X, cons(Y, Z)) -> cons(mark Y, fst(X, Z)), mark nil() -> nil(), mark 0() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark fst(X1, X2) -> a__fst(mark X1, mark X2), mark s X -> s X, mark from X -> a__from mark X, mark add(X1, X2) -> a__add(mark X1, mark X2), mark len X -> a__len mark X, a__from X -> cons(mark X, from s X), a__from X -> from X, a__add(X1, X2) -> add(X1, X2), a__add(0(), X) -> mark X, a__add(s X, Y) -> s add(X, Y), a__len X -> len X, a__len nil() -> 0(), a__len cons(X, Z) -> s len Z} Open