YES(?,O(n^1)) 0.16/0.55 YES(?,O(n^1)) 0.16/0.55 0.16/0.55 Problem: 0.16/0.55 h(f(x,y)) -> f(f(a(),h(h(y))),x) 0.16/0.55 0.16/0.55 Proof: 0.16/0.55 Bounds Processor: 0.16/0.55 bound: 2 0.16/0.55 enrichment: match 0.16/0.55 automaton: 0.16/0.55 final states: {3} 0.16/0.55 transitions: 0.16/0.55 f1(6,16) -> 17* 0.16/0.55 f1(17,1) -> 18,15,3 0.16/0.55 f1(7,1) -> 18,15,3 0.16/0.55 f1(6,5) -> 7* 0.16/0.55 f1(17,2) -> 18,15,3 0.16/0.55 f1(7,2) -> 18,15,3 0.16/0.55 a1() -> 6* 0.16/0.55 h1(15) -> 16* 0.16/0.55 h1(2) -> 4* 0.16/0.55 h1(4) -> 5* 0.16/0.55 h1(1) -> 15* 0.16/0.55 f2(20,19) -> 21* 0.16/0.55 f2(21,7) -> 19,16 0.16/0.55 f2(21,17) -> 19,16 0.16/0.55 h0(2) -> 3* 0.16/0.55 h0(1) -> 3* 0.16/0.55 a2() -> 20* 0.16/0.55 f0(1,2) -> 1* 0.16/0.55 f0(2,1) -> 1* 0.16/0.55 f0(1,1) -> 1* 0.16/0.55 f0(2,2) -> 1* 0.16/0.55 h2(2) -> 18* 0.16/0.55 h2(1) -> 18* 0.16/0.55 h2(18) -> 19* 0.16/0.55 a0() -> 2* 0.16/0.55 problem: 0.16/0.55 0.16/0.55 Qed 0.16/0.55 EOF