YES(?,O(n^1))
0.16/0.76	YES(?,O(n^1))
0.16/0.77	
0.16/0.77	Problem:
0.16/0.77	 f(y,f(y,x)) -> f(f(a(),y),f(a(),y))
0.16/0.77	
0.16/0.77	Proof:
0.16/0.77	 Bounds Processor:
0.16/0.77	  bound: 3
0.16/0.77	  enrichment: match
0.16/0.77	  automaton:
0.16/0.77	   final states: {37,35,30,29,27,2,1}
0.16/0.77	   transitions:
0.16/0.77	    f0(1,35) -> 1*
0.16/0.77	    f0(29,2) -> 1*
0.16/0.77	    f0(30,27) -> 1*
0.16/0.77	    f0(1,2) -> 1*
0.16/0.77	    f0(30,35) -> 1*
0.16/0.77	    f0(37,27) -> 1*
0.16/0.77	    f0(37,35) -> 1*
0.16/0.77	    f0(30,2) -> 1*
0.16/0.77	    f0(29,27) -> 1*
0.16/0.77	    f0(29,35) -> 1*
0.16/0.77	    f0(37,2) -> 1*
0.16/0.77	    f0(1,27) -> 1*
0.16/0.77	    f1(1,37) -> 1*
0.16/0.77	    f1(37,30) -> 1*
0.16/0.77	    f1(27,30) -> 1*
0.16/0.77	    f1(2,30) -> 1*
0.16/0.77	    f1(35,1) -> 1*
0.16/0.77	    f1(30,1) -> 1*
0.16/0.77	    f1(29,30) -> 1*
0.16/0.77	    f1(35,27) -> 1*
0.16/0.77	    f1(35,29) -> 1*
0.16/0.77	    f1(30,29) -> 1*
0.16/0.77	    f1(35,35) -> 1*
0.16/0.77	    f1(35,37) -> 1*
0.16/0.77	    f1(30,37) -> 1*
0.16/0.77	    f1(37,1) -> 1*
0.16/0.77	    f1(27,1) -> 1*
0.16/0.77	    f1(2,1) -> 1*
0.16/0.77	    f1(1,30) -> 1*
0.16/0.77	    f1(27,27) -> 1*
0.16/0.77	    f1(37,29) -> 1*
0.16/0.77	    f1(27,29) -> 1*
0.16/0.77	    f1(2,27) -> 1*
0.16/0.77	    f1(2,29) -> 1*
0.16/0.77	    f1(37,37) -> 1*
0.16/0.77	    f1(27,35) -> 1*
0.16/0.77	    f1(27,37) -> 1*
0.16/0.77	    f1(2,35) -> 1*
0.16/0.77	    f1(29,1) -> 1*
0.16/0.77	    f1(2,37) -> 1*
0.16/0.77	    f1(35,2) -> 1*
0.16/0.77	    f1(29,29) -> 1*
0.16/0.77	    f1(29,37) -> 1*
0.16/0.77	    f1(1,1) -> 1*
0.16/0.77	    f1(35,30) -> 1*
0.16/0.77	    f1(30,30) -> 1*
0.16/0.77	    f1(27,2) -> 1*
0.16/0.77	    f1(2,2) -> 1*
0.16/0.77	    f1(1,29) -> 1*
0.16/0.77	    f2(26,37) -> 1*
0.16/0.77	    f2(37,24) -> 1*
0.16/0.77	    f2(13,1) -> 14*
0.16/0.77	    f2(37,26) -> 1*
0.16/0.77	    f2(37,30) -> 1*
0.16/0.77	    f2(27,30) -> 1,14,16,29*
0.16/0.77	    f2(28,29) -> 1*
0.16/0.77	    f2(13,27) -> 26*
0.16/0.77	    f2(13,29) -> 14*
0.16/0.77	    f2(29,14) -> 1*
0.16/0.77	    f2(13,35) -> 26*
0.16/0.77	    f2(35,1) -> 1,14,16,29*
0.16/0.77	    f2(13,37) -> 14*
0.16/0.77	    f2(15,1) -> 16*
0.16/0.77	    f2(29,28) -> 1*
0.16/0.77	    f2(35,27) -> 30*
0.16/0.77	    f2(35,29) -> 1,14,16,29*
0.16/0.77	    f2(15,29) -> 16*
0.16/0.77	    f2(35,35) -> 30*
0.16/0.77	    f2(35,37) -> 1,14,29*,16
0.16/0.77	    f2(16,14) -> 1*
0.16/0.77	    f2(30,37) -> 1*
0.16/0.77	    f2(25,37) -> 1*
0.16/0.77	    f2(15,37) -> 16*
0.16/0.77	    f2(27,1) -> 28,29*,1,14,16
0.16/0.77	    f2(26,24) -> 1*
0.16/0.77	    f2(26,26) -> 1*
0.16/0.77	    f2(26,30) -> 1*
0.16/0.77	    f2(16,28) -> 1*
0.16/0.77	    f2(13,2) -> 26*,25,24
0.16/0.77	    f2(27,27) -> 26,30*,1
0.16/0.77	    f2(27,29) -> 1,14,16,29*
0.16/0.77	    f2(28,14) -> 1*
0.16/0.77	    f2(37,37) -> 1*
0.16/0.77	    f2(27,35) -> 1,30*
0.16/0.77	    f2(27,37) -> 1,29*,14,16
0.16/0.77	    f2(28,28) -> 1*
0.16/0.77	    f2(13,30) -> 14*
0.16/0.77	    f2(35,2) -> 1,30*
0.16/0.77	    f2(29,29) -> 1*
0.16/0.77	    f2(30,24) -> 1*
0.16/0.77	    f2(25,24) -> 1*
0.16/0.77	    f2(30,26) -> 1*
0.16/0.77	    f2(25,26) -> 1*
0.16/0.77	    f2(35,30) -> 1,29*,14,16
0.16/0.77	    f2(30,30) -> 1*
0.16/0.77	    f2(25,30) -> 1*
0.16/0.77	    f2(15,30) -> 16*
0.16/0.77	    f2(27,2) -> 26,30*,1
0.16/0.77	    f2(16,29) -> 1*
0.16/0.77	    f3(37,32) -> 29*
0.16/0.77	    f3(37,36) -> 29*
0.16/0.77	    f3(33,27) -> 34*
0.16/0.77	    f3(33,35) -> 34*
0.16/0.77	    f3(34,32) -> 29*
0.16/0.77	    f3(34,36) -> 29*
0.16/0.77	    f3(35,27) -> 36,30,37*,1,34,32
0.16/0.77	    f3(35,35) -> 36,30,37*,1,34,32
0.16/0.77	    f3(36,32) -> 29*
0.16/0.77	    f3(36,36) -> 29*
0.16/0.77	    f3(37,37) -> 1,29*
0.16/0.77	    f3(34,37) -> 29*
0.16/0.77	    f3(31,27) -> 32*
0.16/0.77	    f3(31,35) -> 32*
0.16/0.77	    f3(36,37) -> 29*
0.16/0.77	    a3() -> 27,35*,13,15,2,33,31
0.16/0.77	  problem:
0.16/0.77	   
0.16/0.77	  Qed
0.16/0.77	EOF