YES(?,O(n^1))

Problem:
 f(f(X)) -> f(a(b(f(X))))
 f(a(g(X))) -> b(X)
 b(X) -> a(X)

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {6,5}
   transitions:
    b3(72) -> 73*
    a1(14) -> 15*
    a1(31) -> 32*
    a1(33) -> 34*
    a4(88) -> 89*
    b1(25) -> 26*
    b1(23) -> 24*
    b1(13) -> 14*
    f1(15) -> 16*
    f1(17) -> 18*
    f1(12) -> 13*
    a2(52) -> 53*
    a2(61) -> 62*
    a2(41) -> 42*
    f2(65) -> 66*
    f2(42) -> 43*
    f2(39) -> 40*
    f2(63) -> 64*
    f0(5) -> 5*
    f0(6) -> 5*
    b2(40) -> 41*
    b2(67) -> 68*
    a0(5) -> 5*
    a0(6) -> 5*
    a3(69) -> 70*
    a3(86) -> 87*
    a3(73) -> 74*
    b0(5) -> 5*
    b0(6) -> 5*
    f3(74) -> 75*
    f3(71) -> 72*
    g0(5) -> 6*
    g0(6) -> 6*
    5 -> 33,23,12
    6 -> 31,25,17
    12 -> 63*
    13 -> 5*
    15 -> 39*
    16 -> 5*
    17 -> 65*
    18 -> 13*
    23 -> 52*
    24 -> 64,40,69,13,5
    25 -> 61*
    26 -> 64,40,69,13,5
    32 -> 5*
    34 -> 5*
    40 -> 69*
    42 -> 71*
    43 -> 64,40,69,67,13
    53 -> 14,24
    62 -> 26,5,33,12,23
    64 -> 40*
    66 -> 40*
    67 -> 86*
    68 -> 41*
    70 -> 41*
    72 -> 88*
    75 -> 64,40,69
    87 -> 68,41
    89 -> 73*
  problem:
   
  Qed