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 f(0()) -> cons(0()) 0.16/0.23 f(s(0())) -> f(p(s(0()))) 0.16/0.23 p(s(X)) -> 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: {5,4} 0.16/0.23 transitions: 0.16/0.23 f1(12) -> 13* 0.16/0.23 p1(11) -> 12* 0.16/0.23 s1(10) -> 11* 0.16/0.23 01() -> 8* 0.16/0.23 cons1(8) -> 9* 0.16/0.23 cons2(20) -> 21* 0.16/0.23 f0(2) -> 4* 0.16/0.23 f0(1) -> 4* 0.16/0.23 f0(3) -> 4* 0.16/0.23 02() -> 20* 0.16/0.23 00() -> 1* 0.16/0.23 cons0(2) -> 2* 0.16/0.23 cons0(1) -> 2* 0.16/0.23 cons0(3) -> 2* 0.16/0.23 s0(2) -> 3* 0.16/0.23 s0(1) -> 3* 0.16/0.23 s0(3) -> 3* 0.16/0.23 p0(2) -> 5* 0.16/0.23 p0(1) -> 5* 0.16/0.23 p0(3) -> 5* 0.16/0.23 1 -> 5* 0.16/0.23 2 -> 5* 0.16/0.23 3 -> 5* 0.16/0.23 8 -> 10* 0.16/0.23 9 -> 4* 0.16/0.23 10 -> 12* 0.16/0.23 13 -> 4* 0.16/0.23 21 -> 13,4 0.16/0.23 problem: 0.16/0.23 0.16/0.23 Qed 0.16/0.23 EOF