YES(?,O(n^1))
0.15/0.29	YES(?,O(n^1))
0.15/0.29	
0.15/0.29	Problem:
0.15/0.29	 not(true()) -> false()
0.15/0.29	 not(false()) -> true()
0.15/0.29	 odd(0()) -> false()
0.15/0.29	 odd(s(x)) -> not(odd(x))
0.15/0.29	 +(x,0()) -> x
0.15/0.29	 +(x,s(y)) -> s(+(x,y))
0.15/0.29	 +(s(x),y) -> s(+(x,y))
0.15/0.29	
0.15/0.29	Proof:
0.15/0.29	 Bounds Processor:
0.15/0.29	  bound: 2
0.15/0.29	  enrichment: match
0.15/0.29	  automaton:
0.15/0.29	   final states: {7,6,5}
0.15/0.29	   transitions:
0.15/0.29	    s1(10) -> 10,7
0.15/0.29	    +1(3,1) -> 10*
0.15/0.29	    +1(3,3) -> 10*
0.15/0.29	    +1(4,2) -> 10*
0.15/0.29	    +1(4,4) -> 10*
0.15/0.29	    +1(1,2) -> 10*
0.15/0.29	    +1(1,4) -> 10*
0.15/0.29	    +1(2,1) -> 10*
0.15/0.29	    +1(2,3) -> 10*
0.15/0.29	    +1(3,2) -> 10*
0.15/0.29	    +1(3,4) -> 10*
0.15/0.29	    +1(4,1) -> 10*
0.15/0.29	    +1(4,3) -> 10*
0.15/0.29	    +1(1,1) -> 10*
0.15/0.29	    +1(1,3) -> 10*
0.15/0.29	    +1(2,2) -> 10*
0.15/0.29	    +1(2,4) -> 10*
0.15/0.29	    not1(8) -> 8,6
0.15/0.29	    odd1(2) -> 8*
0.15/0.29	    odd1(4) -> 8*
0.15/0.29	    odd1(1) -> 8*
0.15/0.29	    odd1(3) -> 8*
0.15/0.29	    false1() -> 8,6,5
0.15/0.29	    true1() -> 5*
0.15/0.29	    true2() -> 6,8
0.15/0.29	    false2() -> 6,8
0.15/0.29	    not0(2) -> 5*
0.15/0.29	    not0(4) -> 5*
0.15/0.29	    not0(1) -> 5*
0.15/0.29	    not0(3) -> 5*
0.15/0.29	    true0() -> 1*
0.15/0.29	    false0() -> 2*
0.15/0.29	    odd0(2) -> 6*
0.15/0.29	    odd0(4) -> 6*
0.15/0.29	    odd0(1) -> 6*
0.15/0.29	    odd0(3) -> 6*
0.15/0.29	    00() -> 3*
0.15/0.29	    s0(2) -> 4*
0.15/0.29	    s0(4) -> 4*
0.15/0.29	    s0(1) -> 4*
0.15/0.29	    s0(3) -> 4*
0.15/0.29	    +0(3,1) -> 7*
0.15/0.29	    +0(3,3) -> 7*
0.15/0.29	    +0(4,2) -> 7*
0.15/0.29	    +0(4,4) -> 7*
0.15/0.29	    +0(1,2) -> 7*
0.15/0.29	    +0(1,4) -> 7*
0.15/0.29	    +0(2,1) -> 7*
0.15/0.29	    +0(2,3) -> 7*
0.15/0.29	    +0(3,2) -> 7*
0.15/0.29	    +0(3,4) -> 7*
0.15/0.29	    +0(4,1) -> 7*
0.15/0.29	    +0(4,3) -> 7*
0.15/0.29	    +0(1,1) -> 7*
0.15/0.29	    +0(1,3) -> 7*
0.15/0.29	    +0(2,2) -> 7*
0.15/0.29	    +0(2,4) -> 7*
0.15/0.29	    1 -> 10,7
0.15/0.29	    2 -> 10,7
0.15/0.29	    3 -> 10,7
0.15/0.29	    4 -> 10,7
0.15/0.29	  problem:
0.15/0.29	   
0.15/0.29	  Qed
0.57/0.30	EOF