YES(?,O(n^1))
0.16/0.26	YES(?,O(n^1))
0.16/0.26	
0.16/0.26	Problem:
0.16/0.26	 a(c(d(x))) -> c(x)
0.16/0.26	 u(b(d(d(x)))) -> b(x)
0.16/0.26	 v(a(a(x))) -> u(v(x))
0.16/0.26	 v(a(c(x))) -> u(b(d(x)))
0.16/0.26	 v(c(x)) -> b(x)
0.16/0.26	 w(a(a(x))) -> u(w(x))
0.16/0.26	 w(a(c(x))) -> u(b(d(x)))
0.16/0.26	 w(c(x)) -> b(x)
0.16/0.26	
0.16/0.26	Proof:
0.16/0.26	 Bounds Processor:
0.16/0.26	  bound: 2
0.16/0.26	  enrichment: match
0.16/0.26	  automaton:
0.16/0.26	   final states: {8}
0.16/0.26	   transitions:
0.16/0.26	    b1(41) -> 42*
0.16/0.26	    b1(23) -> 24*
0.16/0.26	    b1(13) -> 14*
0.16/0.26	    u1(20) -> 21*
0.16/0.26	    d1(35) -> 36*
0.16/0.26	    d1(22) -> 23*
0.16/0.26	    w1(29) -> 30*
0.16/0.26	    v1(19) -> 20*
0.16/0.26	    c1(11) -> 12*
0.16/0.26	    b2(43) -> 44*
0.16/0.26	    a0(8) -> 8*
0.16/0.26	    c0(8) -> 8*
0.16/0.26	    d0(8) -> 8*
0.16/0.26	    u0(8) -> 8*
0.16/0.26	    b0(8) -> 8*
0.16/0.26	    v0(8) -> 8*
0.16/0.26	    w0(8) -> 8*
0.16/0.26	    8 -> 29,22,19,13,11
0.16/0.26	    11 -> 43,41,35
0.16/0.26	    12 -> 8*
0.16/0.26	    14 -> 21,8
0.16/0.26	    21 -> 30,20,8
0.16/0.26	    24 -> 20*
0.16/0.26	    30 -> 20*
0.16/0.26	    36 -> 13*
0.16/0.26	    42 -> 8*
0.16/0.26	    44 -> 30,20
0.16/0.26	  problem:
0.16/0.26	   
0.16/0.26	  Qed
0.16/0.26	EOF