YES(?,O(n^1)) 0.16/0.30 YES(?,O(n^1)) 0.16/0.30 0.16/0.30 Problem: 0.16/0.30 a__f(f(a())) -> c(f(g(f(a())))) 0.16/0.30 mark(f(X)) -> a__f(mark(X)) 0.16/0.30 mark(a()) -> a() 0.16/0.30 mark(c(X)) -> c(X) 0.16/0.30 mark(g(X)) -> g(mark(X)) 0.16/0.30 a__f(X) -> f(X) 0.16/0.30 0.16/0.30 Proof: 0.16/0.30 Bounds Processor: 0.16/0.30 bound: 2 0.16/0.30 enrichment: match 0.16/0.30 automaton: 0.16/0.30 final states: {6,5} 0.16/0.30 transitions: 0.16/0.30 f1(55) -> 56* 0.16/0.30 f1(12) -> 13* 0.16/0.30 f1(69) -> 70* 0.16/0.30 f1(14) -> 15* 0.16/0.30 f1(61) -> 62* 0.16/0.30 f1(63) -> 64* 0.16/0.30 g1(53) -> 54* 0.16/0.30 g1(13) -> 14* 0.16/0.30 mark1(25) -> 26* 0.16/0.30 mark1(27) -> 28* 0.16/0.30 mark1(17) -> 18* 0.16/0.30 mark1(33) -> 34* 0.16/0.30 c1(45) -> 46* 0.16/0.30 c1(15) -> 16* 0.16/0.30 c1(47) -> 48* 0.16/0.30 c1(37) -> 38* 0.16/0.30 c1(39) -> 40* 0.16/0.30 a1() -> 12* 0.16/0.30 a__f1(18) -> 19* 0.16/0.30 f2(75) -> 76* 0.16/0.30 f2(77) -> 78* 0.16/0.30 f2(71) -> 72* 0.16/0.30 a__f0(2) -> 5* 0.16/0.30 a__f0(4) -> 5* 0.16/0.30 a__f0(1) -> 5* 0.16/0.30 a__f0(3) -> 5* 0.16/0.30 c2(78) -> 79* 0.16/0.30 f0(2) -> 1* 0.16/0.30 f0(4) -> 1* 0.16/0.30 f0(1) -> 1* 0.16/0.30 f0(3) -> 1* 0.16/0.30 g2(76) -> 77* 0.16/0.30 a0() -> 2* 0.16/0.30 a2() -> 75* 0.16/0.30 c0(2) -> 3* 0.16/0.30 c0(4) -> 3* 0.16/0.30 c0(1) -> 3* 0.16/0.30 c0(3) -> 3* 0.16/0.30 g0(2) -> 4* 0.16/0.30 g0(4) -> 4* 0.16/0.30 g0(1) -> 4* 0.16/0.30 g0(3) -> 4* 0.16/0.30 mark0(2) -> 6* 0.16/0.30 mark0(4) -> 6* 0.16/0.30 mark0(1) -> 6* 0.16/0.30 mark0(3) -> 6* 0.16/0.30 1 -> 61,45,27 0.16/0.30 2 -> 69,37,17 0.16/0.30 3 -> 55,47,33 0.16/0.30 4 -> 63,39,25 0.16/0.30 12 -> 18,53,6 0.16/0.30 16 -> 5* 0.16/0.30 18 -> 71,53 0.16/0.30 19 -> 28,18,53,6 0.16/0.30 26 -> 18* 0.16/0.30 28 -> 18* 0.16/0.30 34 -> 18* 0.16/0.30 38 -> 34,18,53,6 0.16/0.30 40 -> 34,18,53,6 0.16/0.30 46 -> 34,18,53,6 0.16/0.30 48 -> 34,18,53,6 0.16/0.30 54 -> 26,18,53,6 0.16/0.30 56 -> 5* 0.16/0.30 62 -> 5* 0.16/0.30 64 -> 5* 0.16/0.30 70 -> 5* 0.16/0.30 72 -> 19,6 0.16/0.30 79 -> 19,28,6,18,71 0.16/0.30 problem: 0.16/0.30 0.16/0.30 Qed 0.16/0.31 EOF