YES(?,O(n^1)) 0.16/0.23 YES(?,O(n^1)) 0.16/0.23 0.16/0.23 Problem: 0.16/0.23 a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) 0.16/0.23 f(a(x),a(y)) -> a(f(x,y)) 0.16/0.23 f(b(x),b(y)) -> b(f(x,y)) 0.16/0.23 0.16/0.23 Proof: 0.16/0.23 Bounds Processor: 0.16/0.23 bound: 1 0.16/0.23 enrichment: match 0.16/0.23 automaton: 0.16/0.23 final states: {3,2} 0.16/0.23 transitions: 0.16/0.23 b1(5) -> 5,3 0.16/0.23 f1(1,1) -> 5* 0.16/0.23 a0(1) -> 2* 0.16/0.23 f0(1,1) -> 3* 0.16/0.23 b0(1) -> 1* 0.16/0.23 problem: 0.16/0.23 0.16/0.23 Qed 0.16/0.23 EOF