YES(?,O(n^1)) 0.15/0.20 YES(?,O(n^1)) 0.15/0.20 0.15/0.20 Problem: 0.15/0.20 minus(minus(x)) -> x 0.15/0.20 minus(h(x)) -> h(minus(x)) 0.15/0.20 minus(f(x,y)) -> f(minus(y),minus(x)) 0.15/0.20 0.15/0.20 Proof: 0.15/0.20 Bounds Processor: 0.15/0.20 bound: 1 0.15/0.20 enrichment: match 0.15/0.20 automaton: 0.15/0.20 final states: {3} 0.15/0.20 transitions: 0.15/0.20 f1(4,4) -> 4,3 0.15/0.20 minus1(2) -> 4* 0.15/0.20 minus1(1) -> 4* 0.15/0.20 h1(4) -> 4,3 0.15/0.20 minus0(2) -> 3* 0.15/0.20 minus0(1) -> 3* 0.15/0.20 h0(2) -> 1* 0.15/0.20 h0(1) -> 1* 0.15/0.20 f0(1,2) -> 2* 0.15/0.20 f0(2,1) -> 2* 0.15/0.20 f0(1,1) -> 2* 0.15/0.20 f0(2,2) -> 2* 0.15/0.20 problem: 0.15/0.20 0.15/0.20 Qed 0.15/0.20 EOF