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(a())) -> c(n__f(g(f(a())))) 0.16/0.22 f(X) -> n__f(X) 0.16/0.22 activate(n__f(X)) -> f(X) 0.16/0.22 activate(X) -> 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: {6,5} 0.16/0.22 transitions: 0.16/0.22 f1(35) -> 36* 0.16/0.22 f1(25) -> 26* 0.16/0.22 f1(27) -> 28* 0.16/0.22 f1(33) -> 34* 0.16/0.22 n__f1(17) -> 18* 0.16/0.22 n__f1(19) -> 20* 0.16/0.22 n__f1(9) -> 10* 0.16/0.22 n__f1(11) -> 12* 0.16/0.22 n__f2(49) -> 50* 0.16/0.22 n__f2(51) -> 52* 0.16/0.22 n__f2(41) -> 42* 0.16/0.22 n__f2(43) -> 44* 0.16/0.22 f0(2) -> 5* 0.16/0.22 f0(4) -> 5* 0.16/0.22 f0(1) -> 5* 0.16/0.22 f0(3) -> 5* 0.16/0.22 a0() -> 1* 0.16/0.22 c0(2) -> 2* 0.16/0.22 c0(4) -> 2* 0.16/0.22 c0(1) -> 2* 0.16/0.22 c0(3) -> 2* 0.16/0.22 n__f0(2) -> 3* 0.16/0.22 n__f0(4) -> 3* 0.16/0.22 n__f0(1) -> 3* 0.16/0.22 n__f0(3) -> 3* 0.16/0.22 g0(2) -> 4* 0.16/0.22 g0(4) -> 4* 0.16/0.22 g0(1) -> 4* 0.16/0.22 g0(3) -> 4* 0.16/0.22 activate0(2) -> 6* 0.16/0.22 activate0(4) -> 6* 0.16/0.22 activate0(1) -> 6* 0.16/0.22 activate0(3) -> 6* 0.16/0.22 1 -> 6,33,11 0.16/0.22 2 -> 6,25,19 0.16/0.22 3 -> 6,35,9 0.16/0.22 4 -> 6,27,17 0.16/0.22 10 -> 5* 0.16/0.22 12 -> 5* 0.16/0.22 18 -> 5* 0.16/0.22 20 -> 5* 0.16/0.22 25 -> 41* 0.16/0.22 26 -> 6* 0.16/0.22 27 -> 49* 0.16/0.22 28 -> 6* 0.16/0.22 33 -> 43* 0.16/0.22 34 -> 6* 0.16/0.22 35 -> 51* 0.16/0.22 36 -> 6* 0.16/0.22 42 -> 26* 0.16/0.22 44 -> 34* 0.16/0.22 50 -> 28,6 0.16/0.22 52 -> 36,6 0.16/0.22 problem: 0.16/0.22 0.16/0.22 Qed 0.16/0.23 EOF