YES(?,O(n^1)) 0.16/0.29 YES(?,O(n^1)) 0.16/0.29 0.16/0.29 Problem: 0.16/0.29 f(a()) -> f(c(a())) 0.16/0.29 f(c(X)) -> X 0.16/0.29 f(c(a())) -> f(d(b())) 0.16/0.29 f(a()) -> f(d(a())) 0.16/0.29 f(d(X)) -> X 0.16/0.29 f(c(b())) -> f(d(a())) 0.16/0.29 e(g(X)) -> e(X) 0.16/0.29 0.16/0.29 Proof: 0.16/0.29 Bounds Processor: 0.16/0.29 bound: 2 0.16/0.29 enrichment: match 0.16/0.29 automaton: 0.16/0.29 final states: {7,6} 0.16/0.29 transitions: 0.16/0.29 e1(30) -> 31* 0.16/0.29 e1(22) -> 23* 0.16/0.29 e1(36) -> 37* 0.16/0.29 e1(38) -> 39* 0.16/0.29 e1(28) -> 29* 0.16/0.29 f1(9) -> 10* 0.16/0.29 d1(20) -> 21* 0.16/0.29 d1(14) -> 15* 0.16/0.29 a1() -> 8* 0.16/0.29 b1() -> 14* 0.16/0.29 c1(8) -> 9* 0.16/0.29 f2(46) -> 47* 0.16/0.29 d2(45) -> 46* 0.16/0.29 f0(5) -> 6* 0.16/0.29 f0(2) -> 6* 0.16/0.29 f0(4) -> 6* 0.16/0.29 f0(1) -> 6* 0.16/0.29 f0(3) -> 6* 0.16/0.29 b2() -> 45* 0.16/0.29 a0() -> 1* 0.16/0.29 c0(5) -> 2* 0.16/0.29 c0(2) -> 2* 0.16/0.29 c0(4) -> 2* 0.16/0.29 c0(1) -> 2* 0.16/0.29 c0(3) -> 2* 0.16/0.29 d0(5) -> 3* 0.16/0.29 d0(2) -> 3* 0.16/0.29 d0(4) -> 3* 0.16/0.29 d0(1) -> 3* 0.16/0.29 d0(3) -> 3* 0.16/0.29 b0() -> 4* 0.16/0.29 e0(5) -> 7* 0.16/0.29 e0(2) -> 7* 0.16/0.29 e0(4) -> 7* 0.16/0.29 e0(1) -> 7* 0.16/0.29 e0(3) -> 7* 0.16/0.29 g0(5) -> 5* 0.16/0.29 g0(2) -> 5* 0.16/0.29 g0(4) -> 5* 0.16/0.29 g0(1) -> 5* 0.16/0.29 g0(3) -> 5* 0.16/0.29 1 -> 36,6 0.16/0.29 2 -> 28,6 0.16/0.29 3 -> 38,6 0.16/0.29 4 -> 30,6 0.16/0.29 5 -> 22,6 0.16/0.29 8 -> 10,6,20 0.16/0.29 10 -> 6* 0.51/0.30 14 -> 10,6 0.51/0.30 15 -> 9* 0.51/0.30 20 -> 10,6 0.51/0.30 21 -> 9* 0.51/0.30 23 -> 7* 0.51/0.30 29 -> 23,7 0.51/0.30 31 -> 23,7 0.51/0.30 37 -> 23,7 0.51/0.30 39 -> 23,7 0.51/0.30 45 -> 47,10 0.51/0.30 47 -> 10,6 0.51/0.30 problem: 0.51/0.30 0.51/0.30 Qed 0.51/0.30 EOF