YES(?,O(n^1))
0.15/0.22	YES(?,O(n^1))
0.15/0.22	
0.15/0.22	Problem:
0.15/0.22	 d(x) -> e(u(x))
0.15/0.22	 d(u(x)) -> c(x)
0.15/0.22	 c(u(x)) -> b(x)
0.15/0.22	 v(e(x)) -> x
0.15/0.22	 b(u(x)) -> a(e(x))
0.15/0.22	
0.15/0.22	Proof:
0.15/0.22	 Bounds Processor:
0.15/0.22	  bound: 1
0.15/0.22	  enrichment: match
0.15/0.22	  automaton:
0.15/0.22	   final states: {7,6,5,4}
0.15/0.22	   transitions:
0.15/0.22	    a1(47) -> 48*
0.15/0.22	    e1(54) -> 55*
0.15/0.22	    e1(9) -> 10*
0.15/0.22	    e1(56) -> 57*
0.15/0.22	    e1(46) -> 47*
0.15/0.22	    b1(40) -> 41*
0.15/0.22	    b1(42) -> 43*
0.15/0.22	    b1(34) -> 35*
0.15/0.22	    c1(32) -> 33*
0.15/0.22	    c1(24) -> 25*
0.15/0.22	    c1(26) -> 27*
0.15/0.22	    u1(16) -> 17*
0.15/0.22	    u1(18) -> 19*
0.15/0.22	    u1(8) -> 9*
0.15/0.22	    d0(2) -> 4*
0.15/0.22	    d0(1) -> 4*
0.15/0.22	    d0(3) -> 4*
0.15/0.22	    e0(2) -> 1*
0.15/0.22	    e0(1) -> 1*
0.15/0.22	    e0(3) -> 1*
0.15/0.22	    u0(2) -> 2*
0.15/0.22	    u0(1) -> 2*
0.15/0.22	    u0(3) -> 2*
0.15/0.22	    c0(2) -> 5*
0.15/0.22	    c0(1) -> 5*
0.15/0.22	    c0(3) -> 5*
0.15/0.22	    b0(2) -> 7*
0.15/0.22	    b0(1) -> 7*
0.15/0.22	    b0(3) -> 7*
0.15/0.22	    v0(2) -> 6*
0.15/0.22	    v0(1) -> 6*
0.15/0.22	    v0(3) -> 6*
0.15/0.22	    a0(2) -> 3*
0.15/0.22	    a0(1) -> 3*
0.15/0.22	    a0(3) -> 3*
0.15/0.22	    1 -> 54,6,40,26,16
0.15/0.22	    2 -> 46,6,34,24,18
0.15/0.22	    3 -> 56,6,42,32,8
0.15/0.22	    10 -> 4*
0.15/0.22	    17 -> 9*
0.15/0.22	    19 -> 9*
0.15/0.22	    25 -> 4*
0.15/0.22	    27 -> 4*
0.15/0.22	    33 -> 4*
0.15/0.22	    35 -> 25,4,5
0.15/0.22	    41 -> 25,4,5
0.15/0.22	    43 -> 25,4,5
0.15/0.22	    48 -> 35,5,7
0.15/0.22	    55 -> 47*
0.15/0.22	    57 -> 47*
0.15/0.22	  problem:
0.15/0.22	   
0.15/0.22	  Qed
0.15/0.22	EOF