YES(?,O(n^1))

Problem:
 f(s(X),X) -> f(X,a(X))
 f(X,c(X)) -> f(s(X),X)
 f(X,X) -> c(X)

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {19,4}
   transitions:
    f0(3,1) -> 4*
    f0(3,3) -> 4*
    f0(19,2) -> 4*
    f0(3,19) -> 4*
    f0(1,2) -> 4*
    f0(2,1) -> 4*
    f0(2,3) -> 4*
    f0(2,19) -> 4*
    f0(3,2) -> 4*
    f0(19,1) -> 4*
    f0(19,3) -> 4*
    f0(19,19) -> 4*
    f0(1,1) -> 4*
    f0(1,3) -> 4*
    f0(1,19) -> 4*
    f0(2,2) -> 4*
    s0(2) -> 1*
    s0(19) -> 1*
    s0(1) -> 1*
    s0(3) -> 1*
    a0(2) -> 2*
    a0(19) -> 2*
    a0(1) -> 2*
    a0(3) -> 2*
    c0(2) -> 3*
    c0(19) -> 3*
    c0(1) -> 3*
    c0(3) -> 3*
    c1(2) -> 19*,3,4
    c1(19) -> 4,3,19*
    c1(1) -> 19*,3,4
    c1(3) -> 19*,3,4
    f1(19,2) -> 4*
    f1(1,2) -> 4*
    f1(3,2) -> 4*
    f1(1,1) -> 4*
    f1(1,3) -> 4*
    f1(1,19) -> 4*
    f1(2,2) -> 4*
    s1(2) -> 1*
    s1(19) -> 1*
    s1(1) -> 1*
    s1(3) -> 1*
    a1(2) -> 2*
    a1(19) -> 2*
    a1(1) -> 2*
    a1(3) -> 2*
    c2(2) -> 3,19*,4
    c2(1) -> 3,19*,4
    f2(19,2) -> 4*
    f2(1,2) -> 4*
    f2(3,2) -> 4*
    f2(1,1) -> 4*
    f2(2,2) -> 4*
    s2(1) -> 1*
    a2(2) -> 2*
    a2(19) -> 2*
    a2(1) -> 2*
    a2(3) -> 2*
    c3(2) -> 19*,3,4
    c3(1) -> 19*,3,4
    f3(1,2) -> 4*
    a3(1) -> 2*
  problem:
   
  Qed