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(a(),f(a(),x)) -> f(a(),f(f(a(),a()),f(a(),x))) 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: {3} 0.15/0.21 transitions: 0.15/0.21 f1(8,3) -> 9* 0.15/0.21 f1(8,11) -> 9,3 0.15/0.21 f1(10,3) -> 11* 0.15/0.21 f1(10,9) -> 11* 0.15/0.21 f1(8,8) -> 10* 0.15/0.21 a1() -> 8* 0.15/0.21 f2(12,11) -> 13* 0.15/0.21 f2(12,15) -> 9* 0.15/0.21 f2(14,13) -> 15* 0.15/0.21 f2(12,12) -> 14* 0.15/0.21 f0(3,3) -> 3* 0.15/0.21 a2() -> 12* 0.15/0.21 a0() -> 3* 0.15/0.21 problem: 0.15/0.21 0.15/0.21 Qed 0.15/0.21 EOF