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