YES(?,O(n^1))
0.16/0.30	YES(?,O(n^1))
0.16/0.30	
0.16/0.30	Problem:
0.16/0.30	 not(true()) -> false()
0.16/0.30	 not(false()) -> true()
0.16/0.30	 evenodd(x,0()) -> not(evenodd(x,s(0())))
0.16/0.30	 evenodd(0(),s(0())) -> false()
0.16/0.30	 evenodd(s(x),s(0())) -> evenodd(x,0())
0.16/0.30	
0.16/0.30	Proof:
0.16/0.30	 Bounds Processor:
0.16/0.30	  bound: 3
0.16/0.30	  enrichment: match
0.16/0.30	  automaton:
0.16/0.30	   final states: {7}
0.16/0.30	   transitions:
0.16/0.30	    false3() -> 7,16,13
0.16/0.30	    evenodd1(7,12) -> 13*
0.16/0.30	    evenodd1(7,11) -> 16,13,7
0.16/0.30	    true3() -> 13,7,16
0.16/0.30	    01() -> 11*
0.16/0.30	    false1() -> 16,13,7
0.16/0.30	    not1(13) -> 7*
0.16/0.30	    s1(11) -> 12*
0.16/0.30	    true1() -> 7*
0.16/0.30	    not2(16) -> 16,13,7
0.16/0.30	    not0(7) -> 7*
0.16/0.30	    evenodd2(7,15) -> 16*
0.16/0.30	    true0() -> 7*
0.16/0.30	    s2(14) -> 15*
0.16/0.30	    false0() -> 7*
0.16/0.30	    02() -> 14*
0.16/0.30	    evenodd0(7,7) -> 7*
0.16/0.30	    true2() -> 16,13,7
0.16/0.30	    00() -> 7*
0.16/0.30	    false2() -> 7*
0.16/0.30	    s0(7) -> 7*
0.16/0.30	  problem:
0.16/0.30	   
0.16/0.30	  Qed
0.16/0.30	EOF