YES(?,O(n^1))
0.15/0.28	YES(?,O(n^1))
0.15/0.28	
0.15/0.28	Problem:
0.15/0.28	 f(f(a())) -> f(g(n__f(n__a())))
0.15/0.28	 f(X) -> n__f(X)
0.15/0.28	 a() -> n__a()
0.15/0.28	 activate(n__f(X)) -> f(activate(X))
0.15/0.28	 activate(n__a()) -> a()
0.15/0.28	 activate(X) -> X
0.15/0.28	
0.15/0.28	Proof:
0.15/0.28	 Bounds Processor:
0.15/0.28	  bound: 3
0.15/0.28	  enrichment: match
0.15/0.28	  automaton:
0.15/0.28	   final states: {6,5,4}
0.15/0.28	   transitions:
0.15/0.28	    a1() -> 35*
0.15/0.28	    f1(25) -> 26*
0.15/0.28	    activate1(27) -> 28*
0.15/0.28	    activate1(24) -> 25*
0.15/0.28	    activate1(33) -> 34*
0.15/0.28	    n__a1() -> 19*
0.15/0.28	    n__f1(17) -> 18*
0.15/0.28	    n__f1(9) -> 10*
0.15/0.28	    n__f1(11) -> 12*
0.15/0.28	    n__a2() -> 41*
0.15/0.28	    n__f2(37) -> 38*
0.15/0.28	    f0(2) -> 4*
0.15/0.28	    f0(1) -> 4*
0.15/0.28	    f0(3) -> 4*
0.15/0.28	    f2(47) -> 48*
0.15/0.28	    a0() -> 5*
0.15/0.28	    g2(46) -> 47*
0.15/0.28	    g0(2) -> 1*
0.15/0.28	    g0(1) -> 1*
0.15/0.28	    g0(3) -> 1*
0.15/0.28	    n__f3(51) -> 52*
0.15/0.28	    n__f0(2) -> 2*
0.15/0.28	    n__f0(1) -> 2*
0.15/0.28	    n__f0(3) -> 2*
0.15/0.28	    n__a0() -> 3*
0.15/0.28	    activate0(2) -> 6*
0.15/0.28	    activate0(1) -> 6*
0.15/0.28	    activate0(3) -> 6*
0.15/0.28	    1 -> 6,27,11
0.15/0.28	    2 -> 6,24,17
0.15/0.28	    3 -> 6,33,9
0.15/0.28	    10 -> 4*
0.15/0.28	    12 -> 4*
0.15/0.28	    18 -> 4*
0.15/0.28	    19 -> 5*
0.15/0.28	    24 -> 25*
0.15/0.28	    25 -> 37*
0.15/0.28	    26 -> 25,6
0.15/0.28	    27 -> 28,25
0.15/0.28	    28 -> 25*
0.15/0.28	    33 -> 34*
0.15/0.28	    34 -> 25*
0.15/0.28	    35 -> 34,25,6
0.15/0.28	    38 -> 46,26,6
0.15/0.28	    41 -> 35,6
0.15/0.28	    47 -> 51*
0.15/0.28	    48 -> 26,25,6,37
0.15/0.28	    52 -> 48,26
0.15/0.28	  problem:
0.15/0.28	   
0.15/0.28	  Qed
0.15/0.28	EOF