YES(?,O(n^1)) 0.16/0.23 YES(?,O(n^1)) 0.16/0.23 0.16/0.23 Problem: 0.16/0.23 c(c(b(c(x)))) -> b(a(0(),c(x))) 0.16/0.23 c(c(x)) -> b(c(b(c(x)))) 0.16/0.23 a(0(),x) -> c(c(x)) 0.16/0.23 0.16/0.23 Proof: 0.16/0.23 Bounds Processor: 0.16/0.23 bound: 2 0.16/0.23 enrichment: match 0.16/0.23 automaton: 0.16/0.23 final states: {4,3} 0.16/0.23 transitions: 0.16/0.23 c1(2) -> 6* 0.16/0.23 c1(6) -> 4* 0.16/0.23 c1(1) -> 6* 0.16/0.23 b2(10) -> 11* 0.16/0.23 b2(12) -> 4* 0.16/0.23 c2(2) -> 10* 0.16/0.23 c2(11) -> 12* 0.16/0.23 c2(1) -> 10* 0.16/0.23 c0(2) -> 3* 0.16/0.23 c0(1) -> 3* 0.16/0.23 b0(2) -> 1* 0.16/0.23 b0(1) -> 1* 0.16/0.23 a0(1,2) -> 4* 0.16/0.23 a0(2,1) -> 4* 0.16/0.23 a0(1,1) -> 4* 0.16/0.23 a0(2,2) -> 4* 0.16/0.23 00() -> 2* 0.16/0.23 problem: 0.16/0.23 0.16/0.23 Qed 0.16/0.23 EOF