YES(?,O(n^1))

Problem:
 a(f(),a(f(),a(g(),a(g(),x)))) -> a(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    g3() -> 74*
    f3() -> 70*
    a4(126,128) -> 108*
    a4(122,115) -> 156*
    a4(126,142) -> 143*
    a4(122,123) -> 124*
    a4(122,137) -> 166*
    a4(126,158) -> 159*
    a4(122,139) -> 140*
    a4(126,160) -> 73*
    a4(126,168) -> 169*
    a4(126,170) -> 123*
    a4(122,157) -> 158*
    a4(126,178) -> 179*
    a4(122,94) -> 176*
    a4(126,180) -> 135*
    a4(122,167) -> 168*
    a4(122,177) -> 178*
    a4(126,125) -> 127*
    a4(126,127) -> 128*
    a4(126,141) -> 142*
    a4(126,143) -> 72*
    a4(122,124) -> 125*
    a4(122,73) -> 123*
    a4(126,159) -> 160*
    a4(122,140) -> 141*
    a4(122,142) -> 166*
    a4(126,169) -> 170*
    a4(122,156) -> 157*
    a4(126,179) -> 180*
    a4(122,95) -> 139*
    a4(122,166) -> 167*
    a4(122,176) -> 177*
    g4() -> 126*
    a0(4,4) -> 4*
    f4() -> 122*
    f0() -> 4*
    a5(185,187) -> 124*
    a5(185,201) -> 202*
    a5(181,182) -> 183*
    a5(181,198) -> 199*
    a5(181,159) -> 182*
    a5(185,184) -> 186*
    a5(185,186) -> 187*
    a5(181,169) -> 198*
    a5(185,200) -> 201*
    a5(185,202) -> 125*
    a5(181,183) -> 184*
    a5(181,199) -> 200*
    g0() -> 4*
    g5() -> 185*
    a1(12,14) -> 15*
    a1(12,18) -> 19*
    a1(12,20) -> 21*
    a1(12,22) -> 13*
    a1(16,18) -> 14,13,4
    a1(16,22) -> 23*
    a1(12,13) -> 14*
    a1(12,17) -> 19*
    a1(12,19) -> 20*
    a1(12,23) -> 13*
    a1(16,15) -> 17*
    a1(16,17) -> 18*
    a1(16,21) -> 22*
    a1(16,23) -> 14,4,13
    a1(12,4) -> 13*
    f5() -> 181*
    g1() -> 16*
    f1() -> 12*
    a2(36,41) -> 48*
    a2(36,43) -> 44*
    a2(36,49) -> 50*
    a2(40,84) -> 85*
    a2(40,86) -> 37*
    a2(36,83) -> 84*
    a2(40,39) -> 41*
    a2(40,41) -> 42*
    a2(36,22) -> 37*
    a2(40,45) -> 46*
    a2(40,47) -> 38,20
    a2(40,51) -> 52*
    a2(36,38) -> 39*
    a2(36,42) -> 43*
    a2(36,44) -> 45*
    a2(36,46) -> 82*
    a2(36,48) -> 49*
    a2(40,85) -> 86*
    a2(36,82) -> 83*
    a2(36,15) -> 43*
    a2(36,17) -> 37*
    a2(36,21) -> 37*
    a2(40,42) -> 43,15,14
    a2(40,46) -> 47*
    a2(40,50) -> 51*
    a2(40,52) -> 43*
    a2(36,37) -> 38*
    g2() -> 40*
    f2() -> 36*
    a3(70,135) -> 136*
    a3(70,72) -> 73*
    a3(74,95) -> 96*
    a3(70,76) -> 107*
    a3(74,109) -> 110*
    a3(74,111) -> 113,83
    a3(70,92) -> 93*
    a3(70,96) -> 134*
    a3(70,108) -> 109*
    a3(70,112) -> 113*
    a3(74,115) -> 116*
    a3(70,39) -> 71*
    a3(70,41) -> 71*
    a3(70,51) -> 71*
    a3(74,137) -> 138*
    a3(74,76) -> 45,44
    a3(70,134) -> 135*
    a3(70,71) -> 72*
    a3(74,94) -> 95*
    a3(74,96) -> 39*
    a3(70,85) -> 92*
    a3(74,110) -> 111*
    a3(70,93) -> 94*
    a3(70,107) -> 108*
    a3(74,114) -> 115*
    a3(74,116) -> 71*
    a3(70,46) -> 112*
    a3(70,113) -> 114*
    a3(74,136) -> 137*
    a3(74,73) -> 75*
    a3(74,138) -> 72,49
    a3(74,75) -> 76*
  problem:
   
  Qed