YES(?,O(n^1)) 0.16/0.26 YES(?,O(n^1)) 0.16/0.26 0.16/0.26 Problem: 0.16/0.26 f(a()) -> f(c(a())) 0.16/0.26 f(c(X)) -> X 0.16/0.26 f(c(a())) -> f(d(b())) 0.16/0.26 f(a()) -> f(d(a())) 0.16/0.26 f(d(X)) -> X 0.16/0.26 f(c(b())) -> f(d(a())) 0.16/0.26 e(g(X)) -> e(X) 0.16/0.26 0.16/0.26 Proof: 0.16/0.26 Bounds Processor: 0.16/0.26 bound: 2 0.16/0.26 enrichment: match 0.16/0.26 automaton: 0.16/0.26 final states: {9,8} 0.16/0.26 transitions: 0.16/0.26 e1(20) -> 21* 0.16/0.26 e1(22) -> 23* 0.16/0.26 f1(14) -> 15* 0.16/0.26 d1(16) -> 17* 0.16/0.26 d1(18) -> 19* 0.16/0.26 a1() -> 13* 0.16/0.26 b1() -> 16* 0.16/0.26 c1(13) -> 14* 0.16/0.26 f2(29) -> 30* 0.16/0.26 d2(28) -> 29* 0.16/0.26 f0(9) -> 8* 0.16/0.26 f0(8) -> 8* 0.16/0.26 b2() -> 28* 0.16/0.26 a0() -> 8* 0.16/0.26 c0(9) -> 8* 0.16/0.26 c0(8) -> 8* 0.16/0.26 d0(9) -> 8* 0.16/0.26 d0(8) -> 8* 0.16/0.26 b0() -> 8* 0.16/0.26 e0(9) -> 8* 0.16/0.26 e0(8) -> 8* 0.16/0.26 g0(9) -> 9* 0.16/0.26 g0(8) -> 9* 0.16/0.26 8 -> 22* 0.16/0.26 9 -> 20,8 0.16/0.26 13 -> 15,8,18 0.16/0.26 15 -> 8* 0.16/0.26 16 -> 15,8 0.16/0.26 17 -> 14* 0.16/0.26 18 -> 15,8 0.16/0.26 19 -> 14* 0.16/0.26 21 -> 8* 0.16/0.26 23 -> 21,8 0.16/0.26 28 -> 30,15 0.16/0.26 30 -> 15,8 0.16/0.26 problem: 0.16/0.26 0.16/0.26 Qed 0.16/0.26 EOF