YES(?,O(n^1)) 0.16/0.21 YES(?,O(n^1)) 0.16/0.21 0.16/0.21 Problem: 0.16/0.21 +(0(),y) -> y 0.16/0.21 +(s(x),y) -> s(+(x,y)) 0.16/0.21 +(s(x),y) -> +(x,s(y)) 0.16/0.21 0.16/0.21 Proof: 0.16/0.21 Bounds Processor: 0.16/0.21 bound: 1 0.16/0.21 enrichment: match 0.16/0.21 automaton: 0.16/0.21 final states: {3} 0.16/0.21 transitions: 0.16/0.21 +1(1,2) -> 4* 0.16/0.21 +1(1,6) -> 3* 0.16/0.21 +1(2,1) -> 4* 0.16/0.21 +1(2,3) -> 4,3 0.16/0.21 +1(1,1) -> 4* 0.16/0.21 +1(1,3) -> 4,3 0.16/0.21 +1(2,2) -> 4* 0.16/0.21 +1(2,6) -> 3* 0.16/0.21 s1(2) -> 6* 0.16/0.21 s1(4) -> 4,3 0.16/0.21 s1(1) -> 6* 0.16/0.21 s1(3) -> 3* 0.16/0.21 +0(1,2) -> 3* 0.16/0.21 +0(2,1) -> 3* 0.16/0.21 +0(1,1) -> 3* 0.16/0.21 +0(2,2) -> 3* 0.16/0.21 00() -> 1* 0.16/0.21 s0(2) -> 2* 0.16/0.21 s0(1) -> 2* 0.16/0.21 1 -> 4,3 0.16/0.21 2 -> 4,3 0.16/0.21 3 -> 4* 0.16/0.21 6 -> 3* 0.16/0.21 problem: 0.16/0.21 0.16/0.21 Qed 0.16/0.22 EOF