YES(?,O(n^1))
0.15/0.23	YES(?,O(n^1))
0.15/0.23	
0.15/0.23	Problem:
0.15/0.23	 a__f(f(a())) -> a__f(g(f(a())))
0.15/0.23	 mark(f(X)) -> a__f(X)
0.15/0.23	 mark(a()) -> a()
0.15/0.23	 mark(g(X)) -> g(mark(X))
0.15/0.23	 a__f(X) -> f(X)
0.15/0.23	
0.15/0.23	Proof:
0.15/0.23	 Bounds Processor:
0.15/0.23	  bound: 2
0.15/0.23	  enrichment: match
0.15/0.23	  automaton:
0.15/0.23	   final states: {5,4}
0.15/0.23	   transitions:
0.15/0.23	    f1(40) -> 41*
0.15/0.23	    f1(46) -> 47*
0.15/0.23	    f1(6) -> 7*
0.15/0.23	    f1(48) -> 49*
0.15/0.23	    g1(30) -> 31*
0.15/0.23	    g1(7) -> 8*
0.15/0.23	    mark1(32) -> 33*
0.15/0.23	    mark1(29) -> 30*
0.15/0.23	    mark1(38) -> 39*
0.15/0.23	    a1() -> 6*
0.15/0.23	    a__f1(24) -> 25*
0.15/0.23	    a__f1(16) -> 17*
0.15/0.23	    a__f1(18) -> 19*
0.15/0.23	    a__f1(8) -> 9*
0.15/0.23	    f2(60) -> 61*
0.15/0.23	    f2(52) -> 53*
0.15/0.23	    f2(66) -> 67*
0.15/0.23	    f2(58) -> 59*
0.15/0.23	    a__f0(2) -> 4*
0.15/0.23	    a__f0(1) -> 4*
0.15/0.23	    a__f0(3) -> 4*
0.15/0.23	    f0(2) -> 1*
0.15/0.23	    f0(1) -> 1*
0.15/0.23	    f0(3) -> 1*
0.15/0.23	    a0() -> 2*
0.15/0.23	    g0(2) -> 3*
0.15/0.23	    g0(1) -> 3*
0.15/0.23	    g0(3) -> 3*
0.15/0.23	    mark0(2) -> 5*
0.15/0.23	    mark0(1) -> 5*
0.15/0.23	    mark0(3) -> 5*
0.15/0.23	    1 -> 46,32,18
0.15/0.23	    2 -> 48,29,16
0.15/0.23	    3 -> 40,38,24
0.15/0.23	    6 -> 30,5
0.15/0.23	    8 -> 66*
0.15/0.23	    9 -> 19,5,4
0.15/0.23	    16 -> 52*
0.15/0.23	    17 -> 33,30,5
0.15/0.23	    18 -> 58*
0.15/0.23	    19 -> 33,30,5
0.15/0.23	    24 -> 60*
0.15/0.23	    25 -> 33,30,5
0.15/0.23	    31 -> 39,30,5
0.15/0.23	    33 -> 30*
0.15/0.23	    39 -> 30*
0.15/0.23	    41 -> 4*
0.15/0.23	    47 -> 4*
0.15/0.23	    49 -> 4*
0.15/0.23	    53 -> 17*
0.15/0.23	    59 -> 19,5
0.15/0.23	    61 -> 25,5
0.15/0.23	    67 -> 9,4
0.15/0.23	  problem:
0.15/0.23	   
0.15/0.23	  Qed
0.15/0.24	EOF