YES(?,O(n^1)) 0.16/0.22 YES(?,O(n^1)) 0.16/0.22 0.16/0.22 Problem: 0.16/0.22 f(f(X)) -> f(a(b(f(X)))) 0.16/0.22 f(a(g(X))) -> b(X) 0.16/0.22 b(X) -> 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: {4,3} 0.16/0.22 transitions: 0.16/0.22 a1(19) -> 20* 0.16/0.22 a1(13) -> 14* 0.16/0.22 b1(5) -> 6* 0.16/0.22 b1(11) -> 12* 0.16/0.22 a2(27) -> 28* 0.16/0.22 a2(21) -> 22* 0.16/0.22 f0(2) -> 3* 0.16/0.22 f0(1) -> 3* 0.16/0.22 a0(2) -> 1* 0.16/0.22 a0(1) -> 1* 0.16/0.22 b0(2) -> 4* 0.16/0.22 b0(1) -> 4* 0.16/0.22 g0(2) -> 2* 0.16/0.22 g0(1) -> 2* 0.16/0.22 1 -> 13,11 0.16/0.22 2 -> 19,5 0.16/0.22 5 -> 27* 0.16/0.22 6 -> 3* 0.16/0.22 11 -> 21* 0.16/0.22 12 -> 3* 0.16/0.22 14 -> 4* 0.16/0.22 20 -> 4* 0.16/0.22 22 -> 12* 0.16/0.22 28 -> 6,3 0.16/0.22 problem: 0.16/0.22 0.16/0.22 Qed 0.16/0.22 EOF