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