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