YES Time: 0.002015 TRS: {f(x, x) -> f(a(), b()), b() -> c()} BOUND: Bound: top(-raise)-bounded by 2 Automaton: { c_2() -> 6* | 4 | 1 b_1() -> 4* | 3 | 1 a_1() -> 5* | 2 | 1 f_1(5, 6) -> 1* f_1(5, 4) -> 1* f_1(5, 3) -> 1* f_1(2, 6) -> 1* f_1(2, 4) -> 1* f_1(2, 3) -> 1* f_0(6, 6) -> 1* f_0(6, 5) -> 1* f_0(6, 4) -> 1* f_0(6, 1) -> 1* f_0(5, 5) -> 1* f_0(5, 1) -> 1* f_0(4, 6) -> 1* f_0(4, 5) -> 1* f_0(4, 4) -> 1* f_0(4, 1) -> 1* f_0(1, 6) -> 1* f_0(1, 5) -> 1* f_0(1, 4) -> 1* f_0(1, 1) -> 1*} Strict: {} Qed