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 f(f(a(),a()),x) -> f(f(x,a()),f(a(),f(a(),a()))) 0.16/0.23 0.16/0.23 Proof: 0.16/0.23 Bounds Processor: 0.16/0.23 bound: 2 0.16/0.23 enrichment: match 0.16/0.23 automaton: 0.16/0.23 final states: {3} 0.16/0.23 transitions: 0.16/0.23 f1(8,9) -> 10* 0.16/0.23 f1(9,10) -> 11* 0.16/0.23 f1(11,10) -> 3* 0.16/0.23 f1(8,8) -> 9* 0.16/0.23 f1(3,8) -> 11* 0.16/0.23 f1(10,8) -> 11* 0.16/0.23 a1() -> 8* 0.16/0.23 f2(12,13) -> 14* 0.16/0.23 f2(10,12) -> 15* 0.16/0.23 f2(15,14) -> 11* 0.16/0.23 f2(12,12) -> 13* 0.16/0.23 f0(3,3) -> 3* 0.16/0.23 a2() -> 12* 0.16/0.23 a0() -> 3* 0.16/0.23 problem: 0.16/0.23 0.16/0.23 Qed 0.16/0.23 EOF