MAYBE Time: 0.000685 TRS: { is_empty nil() -> true(), is_empty cons(x, l) -> false(), hd cons(x, l) -> x, tl cons(x, l) -> l, ifappend(l1, l2, nil()) -> l2, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)), append(l1, l2) -> ifappend(l1, l2, l1)} DP: DP: {ifappend#(l1, l2, cons(x, l)) -> append#(l, l2), append#(l1, l2) -> ifappend#(l1, l2, l1)} TRS: { is_empty nil() -> true(), is_empty cons(x, l) -> false(), hd cons(x, l) -> x, tl cons(x, l) -> l, ifappend(l1, l2, nil()) -> l2, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)), append(l1, l2) -> ifappend(l1, l2, l1)} UR: {a(y, z) -> y, a(y, z) -> z} EDG: {(append#(l1, l2) -> ifappend#(l1, l2, l1), ifappend#(l1, l2, cons(x, l)) -> append#(l, l2)) (ifappend#(l1, l2, cons(x, l)) -> append#(l, l2), append#(l1, l2) -> ifappend#(l1, l2, l1))} STATUS: arrows: 0.500000 SCCS (1): Scc: {ifappend#(l1, l2, cons(x, l)) -> append#(l, l2), append#(l1, l2) -> ifappend#(l1, l2, l1)} SCC (2): Strict: {ifappend#(l1, l2, cons(x, l)) -> append#(l, l2), append#(l1, l2) -> ifappend#(l1, l2, l1)} Weak: { is_empty nil() -> true(), is_empty cons(x, l) -> false(), hd cons(x, l) -> x, tl cons(x, l) -> l, ifappend(l1, l2, nil()) -> l2, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)), append(l1, l2) -> ifappend(l1, l2, l1)} Open