Input TRS: 1: fst(0(),Z) -> nil() 2: fst(s(),cons(Y)) -> cons(Y) 3: from(X) -> cons(X) 4: add(0(),X) -> X 5: add(s(),Y) -> s() 6: len(nil()) -> 0() 7: len(cons(X)) -> s() Number of Rules: 7 Direct POLO(mPol) ... orients all. I(0) = 2 I(len) = 2 * x1 + 3 I(from) = 3 * x1 + 1 I(nil) = 0 I(s) = 2 I(add) = 3 * x1 + 2 * x2 + 2 I(cons) = x1 I(fst) = 3 * x1 + 3 * x2 + 3 Number of Rules: 0