YES(?,O(n^1)) 0.16/0.22 YES(?,O(n^1)) 0.16/0.22 0.16/0.22 Problem: 0.16/0.22 f(0()) -> cons(0(),n__f(s(0()))) 0.16/0.22 f(s(0())) -> f(p(s(0()))) 0.16/0.22 p(s(X)) -> X 0.16/0.22 f(X) -> n__f(X) 0.16/0.22 activate(n__f(X)) -> f(X) 0.16/0.22 activate(X) -> X 0.16/0.22 0.16/0.22 Proof: 0.16/0.22 Bounds Processor: 0.16/0.22 bound: 2 0.16/0.22 enrichment: match 0.16/0.22 automaton: 0.16/0.22 final states: {8} 0.16/0.22 transitions: 0.16/0.22 f1(15) -> 8* 0.16/0.22 f1(8) -> 8* 0.16/0.22 n__f1(13) -> 14* 0.16/0.22 n__f1(8) -> 8* 0.16/0.22 p1(13) -> 15* 0.16/0.22 s1(12) -> 13* 0.16/0.22 01() -> 12* 0.16/0.22 cons1(12,14) -> 8* 0.16/0.22 n__f2(15) -> 8* 0.16/0.22 n__f2(18) -> 19* 0.16/0.22 n__f2(8) -> 8* 0.16/0.22 cons2(17,19) -> 8* 0.16/0.22 f0(8) -> 8* 0.16/0.22 02() -> 17* 0.16/0.22 00() -> 8* 0.16/0.22 s2(17) -> 18* 0.16/0.22 cons0(8,8) -> 8* 0.16/0.22 n__f0(8) -> 8* 0.16/0.22 s0(8) -> 8* 0.16/0.22 p0(8) -> 8* 0.16/0.22 activate0(8) -> 8* 0.16/0.22 12 -> 15* 0.16/0.22 problem: 0.16/0.22 0.16/0.22 Qed 0.16/0.23 EOF