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	 b(b(0(),y),x) -> y
0.15/0.22	 c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
0.15/0.22	 a(y,0()) -> b(y,0())
0.15/0.22	
0.15/0.22	Proof:
0.15/0.22	 Bounds Processor:
0.15/0.22	  bound: 2
0.15/0.22	  enrichment: match
0.15/0.22	  automaton:
0.15/0.22	   final states: {5}
0.15/0.22	   transitions:
0.15/0.22	    b1(6,10) -> 7*
0.15/0.22	    b1(5,6) -> 5*
0.15/0.22	    b1(6,5) -> 7*
0.15/0.22	    b1(6,11) -> 7*
0.15/0.22	    01() -> 6*
0.15/0.22	    c1(10) -> 11*
0.15/0.22	    c1(7) -> 8*
0.15/0.22	    c1(11) -> 5*
0.15/0.22	    a1(9,6) -> 10*
0.15/0.22	    a1(8,6) -> 9*
0.15/0.22	    b2(9,18) -> 10*
0.15/0.22	    b2(8,18) -> 9*
0.15/0.22	    b0(5,5) -> 5*
0.15/0.22	    02() -> 18*
0.15/0.22	    00() -> 5*
0.15/0.22	    c0(5) -> 5*
0.15/0.22	    a0(5,5) -> 5*
0.15/0.22	    6 -> 5*
0.15/0.22	  problem:
0.15/0.22	   
0.15/0.22	  Qed
0.15/0.23	EOF