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