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