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 f(x,x) -> a() 0.15/0.21 f(g(x),y) -> f(x,y) 0.15/0.21 0.15/0.21 Proof: 0.15/0.21 Bounds Processor: 0.15/0.21 bound: 2 0.15/0.21 enrichment: match 0.15/0.21 automaton: 0.15/0.21 final states: {4,3} 0.15/0.21 transitions: 0.15/0.21 f1(4,2) -> 3* 0.15/0.21 f1(4,4) -> 3* 0.15/0.21 f1(1,2) -> 3* 0.15/0.21 f1(1,4) -> 3* 0.15/0.21 f1(2,1) -> 3* 0.15/0.21 f1(4,1) -> 3* 0.15/0.21 f1(1,1) -> 3* 0.15/0.21 f1(2,2) -> 3* 0.15/0.21 f1(2,4) -> 3* 0.15/0.21 a2() -> 1,4*,3 0.15/0.21 g0(2) -> 2* 0.15/0.21 g0(4) -> 2* 0.15/0.21 g0(1) -> 2* 0.15/0.21 problem: 0.15/0.21 0.15/0.21 Qed 0.15/0.21 EOF