YES(?,O(n^1)) 0.16/0.20 YES(?,O(n^1)) 0.16/0.20 0.16/0.20 Problem: 0.16/0.20 f(a(),f(x,a())) -> f(a(),f(f(a(),a()),f(a(),x))) 0.16/0.20 0.16/0.20 Proof: 0.16/0.20 Bounds Processor: 0.16/0.20 bound: 1 0.16/0.20 enrichment: match 0.16/0.20 automaton: 0.16/0.20 final states: {3} 0.16/0.20 transitions: 0.16/0.20 f1(8,3) -> 9* 0.16/0.20 f1(8,11) -> 9,3 0.16/0.20 f1(10,9) -> 11* 0.16/0.20 f1(8,8) -> 10* 0.16/0.20 a1() -> 8* 0.16/0.20 f0(3,3) -> 3* 0.16/0.20 a0() -> 3* 0.16/0.20 problem: 0.16/0.20 0.16/0.20 Qed 0.16/0.20 EOF