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: 6
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    g3() -> 74*
    f3() -> 70*
    a4(126,128) -> 113*
    a4(122,115) -> 156*
    a4(122,123) -> 124*
    a4(126,144) -> 145*
    a4(126,148) -> 149*
    a4(126,150) -> 73*
    a4(126,154) -> 155*
    a4(126,158) -> 159*
    a4(126,160) -> 123*
    a4(122,141) -> 142*
    a4(122,145) -> 151*
    a4(122,147) -> 148*
    a4(122,151) -> 152*
    a4(122,157) -> 158*
    a4(122,187) -> 141*
    a4(126,125) -> 127*
    a4(126,127) -> 128*
    a4(122,120) -> 146*
    a4(126,143) -> 144*
    a4(122,124) -> 125*
    a4(126,145) -> 73,72
    a4(126,149) -> 150*
    a4(126,153) -> 154*
    a4(126,155) -> 72,142
    a4(122,73) -> 123*
    a4(126,159) -> 160*
    a4(122,75) -> 141*
    a4(122,142) -> 143*
    a4(122,144) -> 156*
    a4(122,146) -> 147*
    a4(122,150) -> 151*
    a4(122,152) -> 153*
    a4(122,154) -> 156*
    a4(122,156) -> 157*
    g4() -> 126*
    a0(4,4) -> 4*
    f4() -> 122*
    f0() -> 4*
    a5(166,144) -> 167*
    a5(166,148) -> 193*
    a5(170,169) -> 171*
    a5(170,171) -> 172*
    a5(166,154) -> 203*
    a5(170,185) -> 186*
    a5(170,187) -> 125*
    a5(166,168) -> 169*
    a5(170,195) -> 196*
    a5(170,197) -> 152*
    a5(170,201) -> 202*
    a5(166,184) -> 185*
    a5(170,205) -> 206*
    a5(170,207) -> 193*
    a5(166,194) -> 195*
    a5(166,198) -> 199*
    a5(166,204) -> 205*
    a5(166,143) -> 193*
    a5(166,149) -> 167*
    a5(170,172) -> 124*
    a5(166,159) -> 183*
    a5(170,186) -> 187*
    a5(166,167) -> 168*
    a5(170,196) -> 197*
    a5(170,200) -> 201*
    a5(170,202) -> 142*
    a5(166,183) -> 184*
    a5(166,185) -> 198*
    a5(170,206) -> 207*
    a5(166,193) -> 194*
    a5(166,199) -> 200*
    a5(166,201) -> 203*
    a5(166,203) -> 204*
    g0() -> 4*
    g5() -> 170*
    a1(12,14) -> 15*
    a1(12,18) -> 19*
    a1(12,20) -> 21*
    a1(16,57) -> 13,4
    a1(12,52) -> 13*
    a1(16,81) -> 13,4
    a1(16,18) -> 14,13,4
    a1(16,22) -> 23*
    a1(12,13) -> 14*
    a1(12,17) -> 19*
    a1(12,19) -> 20*
    a1(16,42) -> 4,13
    a1(12,23) -> 13*
    a1(16,52) -> 14,13,4
    a1(16,76) -> 13,4
    a1(16,15) -> 17*
    a1(16,17) -> 18*
    a1(16,21) -> 22*
    a1(16,23) -> 14,4,13
    a1(12,4) -> 13*
    f5() -> 166*
    g1() -> 16*
    a6(208,209) -> 210*
    a6(212,211) -> 213*
    a6(212,213) -> 214*
    a6(208,206) -> 209*
    a6(208,210) -> 211*
    a6(212,214) -> 195*
    f1() -> 12*
    g6() -> 212*
    a2(36,41) -> 53*
    a2(36,49) -> 50*
    a2(36,51) -> 77*
    a2(36,53) -> 54*
    a2(40,76) -> 48,14,15
    a2(36,57) -> 48*
    a2(40,80) -> 81*
    a2(36,77) -> 78*
    a2(36,81) -> 48*
    a2(40,39) -> 41*
    a2(40,41) -> 42*
    a2(36,22) -> 37*
    a2(40,51) -> 52*
    a2(40,55) -> 56*
    a2(40,57) -> 14,15,48
    a2(36,38) -> 39*
    a2(36,42) -> 48*
    a2(36,48) -> 49*
    a2(36,50) -> 37*
    a2(36,54) -> 55*
    a2(40,79) -> 80*
    a2(40,81) -> 48,14,15,37
    a2(36,76) -> 48*
    a2(36,78) -> 79*
    a2(36,15) -> 48*
    a2(36,17) -> 37*
    a2(36,21) -> 37*
    a2(40,42) -> 48,15,14
    a2(40,50) -> 51*
    a2(40,52) -> 38,20
    a2(40,56) -> 57*
    a2(36,37) -> 38*
    f6() -> 208*
    g2() -> 40*
    f2() -> 36*
    a3(70,72) -> 73*
    a3(70,76) -> 112*
    a3(70,80) -> 71*
    a3(70,112) -> 113*
    a3(74,115) -> 116*
    a3(74,119) -> 120*
    a3(74,121) -> 71*
    a3(70,39) -> 71*
    a3(70,41) -> 71*
    a3(70,51) -> 117*
    a3(70,118) -> 119*
    a3(70,55) -> 71*
    a3(74,76) -> 71,37,38,39,50,49
    a3(70,71) -> 72*
    a3(70,75) -> 71*
    a3(70,79) -> 71*
    a3(74,114) -> 115*
    a3(74,116) -> 72,54,118,78
    a3(74,120) -> 121*
    a3(74,128) -> 49*
    a3(70,113) -> 114*
    a3(70,115) -> 117*
    a3(70,117) -> 118*
    a3(74,73) -> 75*
    a3(74,75) -> 76*
    a3(70,56) -> 71*
    a3(70,127) -> 71*
  problem:
   
  Qed