Input TRS: 1: active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y) 2: active(2nd(cons(X,X1))) -> mark(2nd(cons1(X,X1))) 3: active(from(X)) -> mark(cons(X,from(s(X)))) 4: active(2nd(X)) -> 2nd(active(X)) 5: active(cons(X1,X2)) -> cons(active(X1),X2) 6: active(from(X)) -> from(active(X)) 7: active(s(X)) -> s(active(X)) 8: active(cons1(X1,X2)) -> cons1(active(X1),X2) 9: active(cons1(X1,X2)) -> cons1(X1,active(X2)) 10: 2nd(mark(X)) -> mark(2nd(X)) 11: cons(mark(X1),X2) -> mark(cons(X1,X2)) 12: from(mark(X)) -> mark(from(X)) 13: s(mark(X)) -> mark(s(X)) 14: cons1(mark(X1),X2) -> mark(cons1(X1,X2)) 15: cons1(X1,mark(X2)) -> mark(cons1(X1,X2)) 16: proper(2nd(X)) -> 2nd(proper(X)) 17: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) 18: proper(from(X)) -> from(proper(X)) 19: proper(s(X)) -> s(proper(X)) 20: proper(cons1(X1,X2)) -> cons1(proper(X1),proper(X2)) 21: 2nd(ok(X)) -> ok(2nd(X)) 22: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) 23: from(ok(X)) -> ok(from(X)) 24: s(ok(X)) -> ok(s(X)) 25: cons1(ok(X1),ok(X2)) -> ok(cons1(X1,X2)) 26: top(mark(X)) -> top(proper(X)) 27: top(ok(X)) -> top(active(X)) Number of strict rules: 27 Direct Order(PosReal,>,Poly) ... removes: 8 1 3 26 27 22 5 25 9 2 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: x1 cons1(x1,x2) weight: (/ 1 16) + x1 + x2 proper(x1) weight: x1 ok(x1) weight: (/ 1 4) + 2 * x1 from(x1) weight: x1 mark(x1) weight: (/ 1 16) + x1 active(x1) weight: (/ 3 16) + 2 * x1 cons(x1,x2) weight: (/ 1 16) + x1 + x2 Number of strict rules: 17 Direct Order(PosReal,>,Poly) ... removes: 21 10 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: 2 * x1 cons1(x1,x2) weight: (/ 1 16) + x1 + x2 proper(x1) weight: x1 ok(x1) weight: (/ 1 16) + x1 from(x1) weight: x1 mark(x1) weight: (/ 1 16) + x1 active(x1) weight: 2 * x1 cons(x1,x2) weight: (/ 1 16) + x1 + x2 Number of strict rules: 15 Direct Order(PosReal,>,Poly) ... removes: 14 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: 2 * x1 cons1(x1,x2) weight: (/ 1 16) + 2 * x1 + x2 proper(x1) weight: x1 ok(x1) weight: (/ 1 16) + x1 from(x1) weight: x1 mark(x1) weight: (/ 1 16) + x1 active(x1) weight: 2 * x1 cons(x1,x2) weight: (/ 1 16) + x1 + x2 Number of strict rules: 14 Direct Order(PosReal,>,Poly) ... removes: 11 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: 2 * x1 cons1(x1,x2) weight: (/ 1 16) + 2 * x1 + x2 proper(x1) weight: x1 ok(x1) weight: (/ 1 16) + x1 from(x1) weight: x1 mark(x1) weight: (/ 1 16) + x1 active(x1) weight: 2 * x1 cons(x1,x2) weight: (/ 1 16) + 2 * x1 + x2 Number of strict rules: 13 Direct Order(PosReal,>,Poly) ... removes: 20 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: 2 * x1 cons1(x1,x2) weight: (/ 1 8) + 2 * x1 + x2 proper(x1) weight: 2 * x1 ok(x1) weight: (/ 1 8) + x1 from(x1) weight: x1 mark(x1) weight: (/ 1 8) + x1 active(x1) weight: 2 * x1 cons(x1,x2) weight: x1 + x2 Number of strict rules: 12 Direct Order(PosReal,>,Poly) ... removes: 12 23 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: 2 * x1 cons1(x1,x2) weight: (/ 1 8) + 2 * x1 + x2 proper(x1) weight: 2 * x1 ok(x1) weight: (/ 1 8) + x1 from(x1) weight: 2 * x1 mark(x1) weight: (/ 1 8) + x1 active(x1) weight: 2 * x1 cons(x1,x2) weight: x1 + x2 Number of strict rules: 10 Direct Order(PosReal,>,Poly) ... removes: 15 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: x1 cons1(x1,x2) weight: (/ 3 8) + 2 * x1 + 2 * x2 proper(x1) weight: (/ 1 8) + 2 * x1 ok(x1) weight: x1 from(x1) weight: (/ 1 8) + 2 * x1 mark(x1) weight: (/ 5 8) + x1 active(x1) weight: x1 cons(x1,x2) weight: (/ 1 8) + x1 + x2 Number of strict rules: 9 Direct Order(PosReal,>,Poly) ... removes: 18 17 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: x1 cons1(x1,x2) weight: (/ 3 16) + 2 * x1 + 2 * x2 proper(x1) weight: (/ 1 16) + 2 * x1 ok(x1) weight: x1 from(x1) weight: (/ 1 8) + 2 * x1 mark(x1) weight: (/ 5 16) + x1 active(x1) weight: x1 cons(x1,x2) weight: (/ 1 8) + x1 + x2 Number of strict rules: 7 Direct Order(PosReal,>,Poly) ... removes: 6 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: x1 cons1(x1,x2) weight: (/ 3 16) + 2 * x1 + 2 * x2 proper(x1) weight: (/ 1 16) + 2 * x1 ok(x1) weight: x1 from(x1) weight: (/ 1 8) + x1 mark(x1) weight: (/ 5 16) + x1 active(x1) weight: 2 * x1 cons(x1,x2) weight: (/ 1 8) + x1 + x2 Number of strict rules: 6 Direct Order(PosReal,>,Poly) ... removes: 24 s(x1) weight: 2 * x1 top(x1) weight: x1 2nd(x1) weight: x1 cons1(x1,x2) weight: (/ 5 16) + x1 + x2 proper(x1) weight: x1 ok(x1) weight: (/ 1 16) + x1 from(x1) weight: (/ 1 16) + x1 mark(x1) weight: x1 active(x1) weight: 2 * x1 cons(x1,x2) weight: (/ 1 8) + x1 + x2 Number of strict rules: 5 Direct Order(PosReal,>,Poly) ... removes: 13 s(x1) weight: 2 * x1 top(x1) weight: x1 2nd(x1) weight: x1 cons1(x1,x2) weight: (/ 1 16) + x1 + x2 proper(x1) weight: x1 ok(x1) weight: (/ 1 16) + x1 from(x1) weight: (/ 1 16) + x1 mark(x1) weight: (/ 1 16) + x1 active(x1) weight: x1 cons(x1,x2) weight: (/ 1 16) + x1 + x2 Number of strict rules: 4 Direct Order(PosReal,>,Poly) ... removes: 4 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: (/ 181961 8) + x1 cons1(x1,x2) weight: (/ 1 8) + x1 + x2 proper(x1) weight: x1 ok(x1) weight: (/ 1 8) + 2 * x1 from(x1) weight: (/ 1 8) + x1 mark(x1) weight: (/ 45491 2) + x1 active(x1) weight: (/ 1 8) + 2 * x1 cons(x1,x2) weight: (/ 1 8) + x1 + x2 Number of strict rules: 3 Direct Order(PosReal,>,Poly) ... removes: 16 s(x1) weight: x1 top(x1) weight: x1 2nd(x1) weight: (/ 181961 8) + x1 cons1(x1,x2) weight: (/ 1 8) + x1 + x2 proper(x1) weight: 2 * x1 ok(x1) weight: (/ 1 8) + 2 * x1 from(x1) weight: (/ 1 8) + x1 mark(x1) weight: (/ 45491 2) + x1 active(x1) weight: (/ 1 8) + 2 * x1 cons(x1,x2) weight: (/ 1 8) + x1 + x2 Number of strict rules: 2 Direct Order(PosReal,>,Poly) ... removes: 19 7 s(x1) weight: (/ 1 16) + x1 top(x1) weight: x1 2nd(x1) weight: (/ 1 16) + 2 * x1 cons1(x1,x2) weight: x1 + x2 proper(x1) weight: (/ 1 16) + 2 * x1 ok(x1) weight: (/ 1 8) + 2 * x1 from(x1) weight: x1 mark(x1) weight: (/ 1 4) + x1 active(x1) weight: (/ 1 8) + 2 * x1 cons(x1,x2) weight: x1 + x2 Number of strict rules: 0 YES