YES(?,O(n^1))
0.15/0.26	YES(?,O(n^1))
0.15/0.26	
0.15/0.26	Problem:
0.15/0.26	 minus(minus(x)) -> x
0.15/0.26	 minux(+(x,y)) -> +(minus(y),minus(x))
0.15/0.26	 +(minus(x),+(x,y)) -> y
0.15/0.26	 +(+(x,y),minus(y)) -> x
0.15/0.26	
0.15/0.26	Proof:
0.15/0.26	 Bounds Processor:
0.15/0.26	  bound: 1
0.15/0.26	  enrichment: match
0.15/0.26	  automaton:
0.15/0.26	   final states: {7,4}
0.15/0.26	   transitions:
0.15/0.26	    minux0(7) -> 7*,4
0.15/0.26	    minux0(4) -> 7*,4
0.15/0.26	    +0(4,4) -> 7*,4
0.15/0.26	    +0(7,7) -> 7*
0.15/0.26	    +0(4,7) -> 7*,4
0.15/0.26	    +0(7,4) -> 7*,4
0.15/0.26	    +1(7,5) -> 7*,4
0.15/0.26	    +1(7,7) -> 7*,4
0.15/0.26	    +1(6,5) -> 7*,4
0.15/0.26	    +1(6,7) -> 7*,4
0.15/0.26	    minus1(5) -> 4,7*,6
0.15/0.26	    minus1(7) -> 4,7*
0.15/0.26	    minus1(4) -> 7*,4,6,5
0.15/0.26	    minus1(6) -> 4,7*,5
0.15/0.26	    4 -> 7*
0.15/0.26	    5 -> 4*
0.15/0.26	    6 -> 4*
0.15/0.26	    7 -> 4*
0.15/0.26	  problem:
0.15/0.26	   
0.15/0.26	  Qed
0.15/0.27	EOF