YES(?,O(n^1)) 0.15/0.21 YES(?,O(n^1)) 0.15/0.21 0.15/0.21 Problem: 0.15/0.21 p(m,n,s(r)) -> p(m,r,n) 0.15/0.21 p(m,s(n),0()) -> p(0(),n,m) 0.15/0.21 p(m,0(),0()) -> m 0.15/0.21 0.15/0.21 Proof: 0.15/0.21 Bounds Processor: 0.15/0.21 bound: 1 0.15/0.21 enrichment: match 0.15/0.21 automaton: 0.15/0.21 final states: {3} 0.15/0.21 transitions: 0.15/0.21 p1(1,1,1) -> 3* 0.15/0.21 p1(2,2,1) -> 3* 0.15/0.21 p1(1,1,2) -> 3* 0.15/0.21 p1(2,2,2) -> 3* 0.15/0.21 p1(1,2,1) -> 3* 0.15/0.21 p1(2,1,1) -> 3* 0.15/0.21 p1(1,2,2) -> 3* 0.15/0.21 p1(2,1,2) -> 3* 0.15/0.21 01() -> 1* 0.15/0.21 p0(1,1,1) -> 3* 0.15/0.21 p0(2,2,1) -> 3* 0.15/0.21 p0(1,1,2) -> 3* 0.15/0.21 p0(2,2,2) -> 3* 0.15/0.21 p0(1,2,1) -> 3* 0.15/0.21 p0(2,1,1) -> 3* 0.15/0.21 p0(1,2,2) -> 3* 0.15/0.21 p0(2,1,2) -> 3* 0.15/0.21 s0(2) -> 1* 0.15/0.21 s0(1) -> 1* 0.15/0.21 00() -> 2* 0.15/0.21 1 -> 3* 0.15/0.21 2 -> 3* 0.15/0.21 problem: 0.15/0.21 0.15/0.21 Qed 0.15/0.21 EOF