YES(?,O(n^1))
0.16/0.25	YES(?,O(n^1))
0.16/0.25	
0.16/0.25	Problem:
0.16/0.25	 a(c(d(x))) -> c(x)
0.16/0.25	 u(b(d(d(x)))) -> b(x)
0.16/0.25	 v(a(a(x))) -> u(v(x))
0.16/0.25	 v(a(c(x))) -> u(b(d(x)))
0.16/0.25	 v(c(x)) -> b(x)
0.16/0.25	 w(a(a(x))) -> u(w(x))
0.16/0.25	 w(a(c(x))) -> u(b(d(x)))
0.16/0.25	 w(c(x)) -> b(x)
0.16/0.25	
0.16/0.25	Proof:
0.16/0.25	 Bounds Processor:
0.16/0.25	  bound: 1
0.16/0.25	  enrichment: match
0.16/0.25	  automaton:
0.16/0.25	   final states: {7,6,5,4}
0.16/0.25	   transitions:
0.16/0.25	    b1(20) -> 21*
0.16/0.25	    b1(26) -> 27*
0.16/0.25	    b1(28) -> 29*
0.16/0.25	    c1(10) -> 11*
0.16/0.25	    c1(12) -> 13*
0.16/0.25	    c1(18) -> 19*
0.16/0.25	    a0(2) -> 4*
0.16/0.25	    a0(1) -> 4*
0.16/0.25	    a0(3) -> 4*
0.16/0.25	    c0(2) -> 1*
0.16/0.25	    c0(1) -> 1*
0.16/0.25	    c0(3) -> 1*
0.16/0.25	    d0(2) -> 2*
0.16/0.25	    d0(1) -> 2*
0.16/0.25	    d0(3) -> 2*
0.16/0.25	    u0(2) -> 5*
0.16/0.25	    u0(1) -> 5*
0.16/0.25	    u0(3) -> 5*
0.16/0.25	    b0(2) -> 3*
0.16/0.25	    b0(1) -> 3*
0.16/0.25	    b0(3) -> 3*
0.16/0.25	    v0(2) -> 6*
0.16/0.25	    v0(1) -> 6*
0.16/0.25	    v0(3) -> 6*
0.16/0.25	    w0(2) -> 7*
0.16/0.25	    w0(1) -> 7*
0.16/0.25	    w0(3) -> 7*
0.16/0.25	    1 -> 26,12
0.16/0.25	    2 -> 20,10
0.16/0.25	    3 -> 28,18
0.16/0.25	    11 -> 4*
0.16/0.25	    13 -> 4*
0.16/0.25	    19 -> 4*
0.16/0.25	    21 -> 7,6,5
0.16/0.25	    27 -> 7,6,5
0.16/0.25	    29 -> 7,6,5
0.16/0.25	  problem:
0.16/0.25	   
0.16/0.25	  Qed
0.16/0.25	EOF