YES(?,O(n^2)) 26.31/10.56 YES(?,O(n^2)) 26.31/10.56 26.31/10.56 Problem: 26.31/10.56 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.56 f(s(0())) -> f(p(s(0()))) 26.31/10.56 p(s(X)) -> X 26.31/10.56 f(X) -> n__f(X) 26.31/10.56 s(X) -> n__s(X) 26.31/10.56 0() -> n__0() 26.31/10.56 activate(n__f(X)) -> f(activate(X)) 26.31/10.56 activate(n__s(X)) -> s(activate(X)) 26.31/10.56 activate(n__0()) -> 0() 26.31/10.56 activate(X) -> X 26.31/10.56 26.31/10.56 Proof: 26.31/10.56 Complexity Transformation Processor: 26.31/10.56 strict: 26.31/10.56 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.56 f(s(0())) -> f(p(s(0()))) 26.31/10.56 p(s(X)) -> X 26.31/10.56 f(X) -> n__f(X) 26.31/10.56 s(X) -> n__s(X) 26.31/10.56 0() -> n__0() 26.31/10.56 activate(n__f(X)) -> f(activate(X)) 26.31/10.56 activate(n__s(X)) -> s(activate(X)) 26.31/10.56 activate(n__0()) -> 0() 26.31/10.56 activate(X) -> X 26.31/10.56 weak: 26.31/10.56 26.31/10.56 Matrix Interpretation Processor: dim=1 26.31/10.56 26.31/10.56 max_matrix: 26.31/10.56 1 26.31/10.56 interpretation: 26.31/10.56 [activate](x0) = x0 + 13, 26.31/10.56 26.31/10.56 [p](x0) = x0 + 4, 26.31/10.56 26.31/10.56 [s](x0) = x0 + 2, 26.31/10.56 26.31/10.56 [cons](x0, x1) = x0 + x1 + 4, 26.31/10.56 26.31/10.56 [n__f](x0) = x0 + 7, 26.31/10.56 26.31/10.56 [n__s](x0) = x0 + 3, 26.31/10.56 26.31/10.56 [n__0] = 0, 26.31/10.56 26.31/10.56 [f](x0) = x0 + 6, 26.31/10.56 26.31/10.56 [0] = 3 26.31/10.56 orientation: 26.31/10.56 f(0()) = 9 >= 17 = cons(0(),n__f(n__s(n__0()))) 26.31/10.56 26.31/10.56 f(s(0())) = 11 >= 15 = f(p(s(0()))) 26.31/10.57 26.31/10.57 p(s(X)) = X + 6 >= X = X 26.31/10.57 26.31/10.57 f(X) = X + 6 >= X + 7 = n__f(X) 26.31/10.57 26.31/10.57 s(X) = X + 2 >= X + 3 = n__s(X) 26.31/10.57 26.31/10.57 0() = 3 >= 0 = n__0() 26.31/10.57 26.31/10.57 activate(n__f(X)) = X + 20 >= X + 19 = f(activate(X)) 26.31/10.57 26.31/10.57 activate(n__s(X)) = X + 16 >= X + 15 = s(activate(X)) 26.31/10.57 26.31/10.57 activate(n__0()) = 13 >= 3 = 0() 26.31/10.57 26.31/10.57 activate(X) = X + 13 >= X = X 26.31/10.57 problem: 26.31/10.57 strict: 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 weak: 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 Splitting Processor: 26.31/10.57 strict: 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 weak: 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 Splitting Processor: 26.31/10.57 strict: 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 weak: 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 Bounds Processor: 26.31/10.57 bound: 2 26.31/10.57 enrichment: match 26.31/10.57 automaton: 26.31/10.57 final states: {10} 26.31/10.57 transitions: 26.31/10.57 f1(21) -> 22* 26.31/10.57 p1(20) -> 21* 26.31/10.57 s1(19) -> 20* 26.31/10.57 01() -> 18* 26.31/10.57 n__01() -> 15* 26.31/10.57 n__s1(25) -> 26* 26.31/10.57 n__s1(15) -> 16* 26.31/10.57 n__f1(16) -> 17* 26.31/10.57 n__f1(23) -> 24* 26.31/10.57 cons1(18,17) -> 10* 26.31/10.57 activate1(31) -> 32* 26.31/10.57 cons2(30,29) -> 22* 26.31/10.57 f0(10) -> 10* 26.31/10.57 02() -> 30* 26.31/10.57 s0(10) -> 10* 26.31/10.57 n__f2(28) -> 29* 26.31/10.57 00() -> 10* 26.31/10.57 n__s2(27) -> 28* 26.31/10.57 p0(10) -> 10* 26.31/10.57 n__02() -> 27* 26.31/10.57 cons0(10,10) -> 10* 26.31/10.57 n__f0(10) -> 10* 26.31/10.57 n__s0(10) -> 10* 26.31/10.57 n__00() -> 10* 26.31/10.57 activate0(10) -> 10* 26.31/10.57 15 -> 18* 26.31/10.57 18 -> 32,19 26.31/10.57 19 -> 21,25 26.31/10.57 21 -> 23* 26.31/10.57 22 -> 10* 26.31/10.57 23 -> 31* 26.31/10.57 24 -> 22* 26.31/10.57 26 -> 20* 26.31/10.57 27 -> 30* 26.31/10.57 31 -> 32* 26.31/10.57 32 -> 21* 26.31/10.57 problem: 26.31/10.57 strict: 26.31/10.57 26.31/10.57 weak: 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 Qed 26.31/10.57 26.31/10.57 strict: 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 weak: 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 Bounds Processor: 26.31/10.57 bound: 1 26.31/10.57 enrichment: match 26.31/10.57 automaton: 26.31/10.57 final states: {10} 26.31/10.57 transitions: 26.31/10.57 f1(17) -> 18* 26.31/10.57 p1(16) -> 17* 26.31/10.57 s1(15) -> 16* 26.31/10.57 01() -> 15* 26.31/10.57 n__01() -> 15,19 26.31/10.57 n__s1(15) -> 16* 26.31/10.57 n__s1(19) -> 20* 26.31/10.57 n__f1(20) -> 21* 26.31/10.57 n__f1(17) -> 18* 26.31/10.57 cons1(15,21) -> 18,10 26.31/10.57 activate1(17) -> 17* 26.31/10.57 f0(10) -> 10* 26.31/10.57 s0(10) -> 10* 26.31/10.57 00() -> 10* 26.31/10.57 p0(10) -> 10* 26.31/10.57 cons0(10,10) -> 10* 26.31/10.57 n__f0(10) -> 10* 26.31/10.57 n__s0(10) -> 10* 26.31/10.57 n__00() -> 10* 26.31/10.57 activate0(10) -> 10* 26.31/10.57 15 -> 17* 26.31/10.57 18 -> 10* 26.31/10.57 problem: 26.31/10.57 strict: 26.31/10.57 26.31/10.57 weak: 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 Qed 26.31/10.57 26.31/10.57 strict: 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 weak: 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 Matrix Interpretation Processor: dim=2 26.31/10.57 26.31/10.57 max_matrix: 26.31/10.57 [1 1] 26.31/10.57 [0 1] 26.31/10.57 interpretation: 26.31/10.57 [1 1] 26.31/10.57 [activate](x0) = [0 1]x0, 26.31/10.57 26.31/10.57 26.31/10.57 [p](x0) = x0, 26.31/10.57 26.31/10.57 26.31/10.57 [s](x0) = x0, 26.31/10.57 26.31/10.57 [1 0] [1 0] [1] 26.31/10.57 [cons](x0, x1) = [0 0]x0 + [0 0]x1 + [1], 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [n__f](x0) = x0 + [1], 26.31/10.57 26.31/10.57 26.31/10.57 [n__s](x0) = x0, 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [n__0] = [0], 26.31/10.57 26.31/10.57 [1] 26.31/10.57 [f](x0) = x0 + [1], 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [0] = [0] 26.31/10.57 orientation: 26.31/10.57 [1] [0] 26.31/10.57 f(X) = X + [1] >= X + [1] = n__f(X) 26.31/10.57 26.31/10.57 26.31/10.57 s(X) = X >= X = n__s(X) 26.31/10.57 26.31/10.57 26.31/10.57 p(s(X)) = X >= X = X 26.31/10.57 26.31/10.57 [0] [0] 26.31/10.57 0() = [0] >= [0] = n__0() 26.31/10.57 26.31/10.57 [1 1] [1] [1 1] [1] 26.31/10.57 activate(n__f(X)) = [0 1]X + [1] >= [0 1]X + [1] = f(activate(X)) 26.31/10.57 26.31/10.57 [1 1] [1 1] 26.31/10.57 activate(n__s(X)) = [0 1]X >= [0 1]X = s(activate(X)) 26.31/10.57 26.31/10.57 [0] [0] 26.31/10.57 activate(n__0()) = [0] >= [0] = 0() 26.31/10.57 26.31/10.57 [1 1] 26.31/10.57 activate(X) = [0 1]X >= X = X 26.31/10.57 26.31/10.57 [1] [1] 26.31/10.57 f(0()) = [1] >= [1] = cons(0(),n__f(n__s(n__0()))) 26.31/10.57 26.31/10.57 [1] [1] 26.31/10.57 f(s(0())) = [1] >= [1] = f(p(s(0()))) 26.31/10.57 problem: 26.31/10.57 strict: 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 weak: 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 Matrix Interpretation Processor: dim=2 26.31/10.57 26.31/10.57 max_matrix: 26.31/10.57 [1 2] 26.31/10.57 [0 1] 26.31/10.57 interpretation: 26.31/10.57 [1 2] [1] 26.31/10.57 [activate](x0) = [0 1]x0 + [0], 26.31/10.57 26.31/10.57 26.31/10.57 [p](x0) = x0, 26.31/10.57 26.31/10.57 [1] 26.31/10.57 [s](x0) = x0 + [2], 26.31/10.57 26.31/10.57 [1 0] [0] 26.31/10.57 [cons](x0, x1) = x0 + [0 0]x1 + [2], 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [n__f](x0) = x0 + [2], 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [n__s](x0) = x0 + [2], 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [n__0] = [1], 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [f](x0) = x0 + [2], 26.31/10.57 26.31/10.57 [0] 26.31/10.57 [0] = [1] 26.31/10.57 orientation: 26.31/10.57 [1] [0] 26.31/10.57 s(X) = X + [2] >= X + [2] = n__s(X) 26.31/10.57 26.31/10.57 [0] [0] 26.31/10.57 f(X) = X + [2] >= X + [2] = n__f(X) 26.31/10.57 26.31/10.57 [1] 26.31/10.57 p(s(X)) = X + [2] >= X = X 26.31/10.57 26.31/10.57 [0] [0] 26.31/10.57 0() = [1] >= [1] = n__0() 26.31/10.57 26.31/10.57 [1 2] [5] [1 2] [1] 26.31/10.57 activate(n__f(X)) = [0 1]X + [2] >= [0 1]X + [2] = f(activate(X)) 26.31/10.57 26.31/10.57 [1 2] [5] [1 2] [2] 26.31/10.57 activate(n__s(X)) = [0 1]X + [2] >= [0 1]X + [2] = s(activate(X)) 26.31/10.57 26.31/10.57 [3] [0] 26.31/10.57 activate(n__0()) = [1] >= [1] = 0() 26.31/10.57 26.31/10.57 [1 2] [1] 26.31/10.57 activate(X) = [0 1]X + [0] >= X = X 26.31/10.57 26.31/10.57 [0] [0] 26.31/10.57 f(0()) = [3] >= [3] = cons(0(),n__f(n__s(n__0()))) 26.31/10.57 26.31/10.57 [1] [1] 26.31/10.57 f(s(0())) = [5] >= [5] = f(p(s(0()))) 26.31/10.57 problem: 26.31/10.57 strict: 26.31/10.57 26.31/10.57 weak: 26.31/10.57 s(X) -> n__s(X) 26.31/10.57 f(X) -> n__f(X) 26.31/10.57 p(s(X)) -> X 26.31/10.57 0() -> n__0() 26.31/10.57 activate(n__f(X)) -> f(activate(X)) 26.31/10.57 activate(n__s(X)) -> s(activate(X)) 26.31/10.57 activate(n__0()) -> 0() 26.31/10.57 activate(X) -> X 26.31/10.57 f(0()) -> cons(0(),n__f(n__s(n__0()))) 26.31/10.57 f(s(0())) -> f(p(s(0()))) 26.31/10.57 Qed 26.31/10.58 EOF