YES(?,O(n^1))
0.16/0.28	YES(?,O(n^1))
0.16/0.28	
0.16/0.28	Problem:
0.16/0.28	 f(0()) -> s(0())
0.16/0.28	 f(s(0())) -> s(0())
0.16/0.28	 f(s(s(x))) -> f(f(s(x)))
0.16/0.28	
0.16/0.28	Proof:
0.16/0.28	 Bounds Processor:
0.16/0.28	  bound: 3
0.16/0.28	  enrichment: match
0.16/0.28	  automaton:
0.16/0.28	   final states: {4}
0.16/0.28	   transitions:
0.16/0.28	    s3(37) -> 38*
0.16/0.28	    f1(10) -> 11*
0.16/0.28	    f1(19) -> 20*
0.16/0.28	    f1(11) -> 12*
0.16/0.28	    03() -> 37*
0.16/0.28	    s1(7) -> 8*
0.16/0.28	    s1(9) -> 10*
0.16/0.28	    s1(41) -> 42*
0.16/0.28	    01() -> 7*
0.16/0.28	    f2(45) -> 46*
0.16/0.28	    f2(25) -> 26*
0.16/0.28	    f2(24) -> 25*
0.16/0.28	    f0(4) -> 4*
0.16/0.28	    s2(33) -> 34*
0.16/0.28	    s2(23) -> 24*
0.16/0.28	    00() -> 4*
0.16/0.28	    02() -> 33*
0.16/0.28	    s0(4) -> 4*
0.16/0.28	    4 -> 9*
0.16/0.28	    7 -> 23*
0.16/0.28	    8 -> 11,4
0.16/0.28	    12 -> 11,19,4
0.16/0.28	    20 -> 4*
0.16/0.28	    26 -> 45,11
0.16/0.28	    33 -> 41*
0.16/0.28	    34 -> 20,25,12
0.16/0.28	    38 -> 46,26,11
0.16/0.28	    42 -> 10*
0.16/0.28	    46 -> 11*
0.16/0.28	  problem:
0.16/0.28	   
0.16/0.28	  Qed
0.16/0.30	EOF