YES(?,O(n^1)) 0.16/0.20 YES(?,O(n^1)) 0.16/0.20 0.16/0.20 Problem: 0.16/0.20 f(0()) -> cons(0()) 0.16/0.20 f(s(0())) -> f(p(s(0()))) 0.16/0.20 p(s(X)) -> X 0.16/0.20 0.16/0.20 Proof: 0.16/0.20 Bounds Processor: 0.16/0.20 bound: 2 0.16/0.20 enrichment: match 0.16/0.20 automaton: 0.16/0.20 final states: {6} 0.16/0.20 transitions: 0.16/0.20 f1(13) -> 14* 0.16/0.20 p1(12) -> 13* 0.16/0.20 s1(11) -> 12* 0.16/0.20 01() -> 9* 0.16/0.20 cons1(9) -> 10* 0.16/0.20 cons2(19) -> 20* 0.16/0.20 f0(6) -> 6* 0.16/0.20 02() -> 19* 0.16/0.20 00() -> 6* 0.16/0.20 cons0(6) -> 6* 0.16/0.20 s0(6) -> 6* 0.16/0.20 p0(6) -> 6* 0.16/0.20 9 -> 11* 0.16/0.20 10 -> 6* 0.16/0.20 11 -> 13* 0.16/0.20 14 -> 6* 0.16/0.20 20 -> 14,6 0.16/0.20 problem: 0.16/0.20 0.16/0.20 Qed 0.16/0.21 EOF