YES(?,O(n^1)) 0.16/0.25 YES(?,O(n^1)) 0.16/0.25 0.16/0.25 Problem: 0.16/0.25 c(c(c(y))) -> c(c(a(y,0()))) 0.16/0.25 c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) 0.16/0.25 c(y) -> y 0.16/0.25 0.16/0.25 Proof: 0.16/0.25 Bounds Processor: 0.16/0.25 bound: 3 0.16/0.25 enrichment: match 0.16/0.25 automaton: 0.16/0.25 final states: {4} 0.16/0.25 transitions: 0.16/0.25 c3(27) -> 28* 0.16/0.25 c3(28) -> 25* 0.16/0.25 a1(9,8) -> 9* 0.16/0.25 a1(4,8) -> 9* 0.16/0.25 a1(13,4) -> 4* 0.16/0.25 a1(13,8) -> 10* 0.16/0.25 a1(10,8) -> 9* 0.16/0.25 a3(17,26) -> 27* 0.16/0.25 c1(10) -> 4* 0.16/0.25 c1(12) -> 13* 0.16/0.25 c1(9) -> 10* 0.16/0.25 c1(11) -> 12* 0.16/0.25 c1(8) -> 11* 0.16/0.25 03() -> 26* 0.16/0.25 01() -> 8* 0.16/0.25 c2(17) -> 23* 0.16/0.25 c2(24) -> 25* 0.16/0.25 c2(19) -> 13* 0.16/0.25 c2(23) -> 24* 0.16/0.25 c2(18) -> 19* 0.16/0.25 c0(4) -> 4* 0.16/0.25 a2(8,17) -> 18* 0.16/0.25 a2(25,8) -> 10,4 0.16/0.25 a0(4,4) -> 4* 0.16/0.25 02() -> 17* 0.16/0.25 00() -> 4* 0.16/0.25 8 -> 11* 0.16/0.25 9 -> 10* 0.16/0.25 10 -> 4* 0.16/0.25 11 -> 12* 0.16/0.25 12 -> 13* 0.16/0.25 17 -> 23* 0.16/0.25 18 -> 19* 0.16/0.25 19 -> 13* 0.16/0.25 23 -> 24* 0.16/0.25 24 -> 25* 0.16/0.25 27 -> 28* 0.16/0.25 28 -> 25* 0.16/0.25 problem: 0.16/0.25 0.16/0.25 Qed 0.16/0.26 EOF