YES(?,O(n^1)) 0.16/0.24 YES(?,O(n^1)) 0.16/0.24 0.16/0.24 Problem: 0.16/0.24 f(f(x)) -> f(c(f(x))) 0.16/0.24 f(f(x)) -> f(d(f(x))) 0.16/0.24 g(c(x)) -> x 0.16/0.24 g(d(x)) -> x 0.16/0.24 g(c(0())) -> g(d(1())) 0.16/0.24 g(c(1())) -> g(d(0())) 0.16/0.24 0.16/0.24 Proof: 0.16/0.24 Bounds Processor: 0.16/0.24 bound: 2 0.16/0.24 enrichment: match 0.16/0.24 automaton: 0.16/0.24 final states: {7} 0.16/0.24 transitions: 0.16/0.24 g1(23) -> 24* 0.16/0.24 d1(22) -> 23* 0.16/0.24 d1(16) -> 17* 0.16/0.24 01() -> 25* 0.16/0.24 11() -> 22* 0.16/0.24 f1(12) -> 13* 0.16/0.24 f1(14) -> 15* 0.16/0.24 c1(38) -> 39* 0.16/0.24 c1(13) -> 14* 0.16/0.24 f2(30) -> 31* 0.16/0.24 f2(32) -> 33* 0.16/0.24 f0(7) -> 7* 0.16/0.24 d2(40) -> 41* 0.16/0.24 c0(7) -> 7* 0.16/0.24 c2(31) -> 32* 0.16/0.24 d0(7) -> 7* 0.16/0.24 g0(7) -> 7* 0.16/0.24 00() -> 7* 0.16/0.24 10() -> 7* 0.16/0.24 7 -> 12* 0.16/0.24 13 -> 16* 0.16/0.24 14 -> 30* 0.16/0.24 15 -> 13,38,16,7 0.16/0.24 17 -> 14* 0.16/0.24 22 -> 24,7 0.16/0.24 24 -> 7* 0.16/0.24 25 -> 22* 0.16/0.24 31 -> 40* 0.16/0.24 33 -> 13,16 0.16/0.24 39 -> 14* 0.16/0.24 41 -> 32* 0.16/0.24 problem: 0.16/0.24 0.16/0.24 Qed 0.16/0.24 EOF