YES(O(1),O(n^1)) 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 We are left with following problem, upon which TcT provides the 10.98/3.42 certificate YES(O(1),O(n^1)). 10.98/3.42 10.98/3.42 Strict Trs: 10.98/3.42 { p(X) -> n__p(X) 10.98/3.42 , p(0()) -> 0() 10.98/3.42 , p(s(X)) -> X 10.98/3.42 , 0() -> n__0() 10.98/3.42 , s(X) -> n__s(X) 10.98/3.42 , leq(0(), Y) -> true() 10.98/3.42 , leq(s(X), 0()) -> false() 10.98/3.42 , leq(s(X), s(Y)) -> leq(X, Y) 10.98/3.42 , if(true(), X, Y) -> activate(X) 10.98/3.42 , if(false(), X, Y) -> activate(Y) 10.98/3.42 , activate(X) -> X 10.98/3.42 , activate(n__0()) -> 0() 10.98/3.42 , activate(n__s(X)) -> s(activate(X)) 10.98/3.42 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.42 , activate(n__p(X)) -> p(activate(X)) 10.98/3.42 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) 10.98/3.42 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.42 Obligation: 10.98/3.42 innermost runtime complexity 10.98/3.42 Answer: 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 Arguments of following rules are not normal-forms: 10.98/3.42 10.98/3.42 { p(0()) -> 0() 10.98/3.42 , p(s(X)) -> X 10.98/3.42 , leq(0(), Y) -> true() 10.98/3.42 , leq(s(X), 0()) -> false() 10.98/3.42 , leq(s(X), s(Y)) -> leq(X, Y) } 10.98/3.42 10.98/3.42 All above mentioned rules can be savely removed. 10.98/3.42 10.98/3.42 We are left with following problem, upon which TcT provides the 10.98/3.42 certificate YES(O(1),O(n^1)). 10.98/3.42 10.98/3.42 Strict Trs: 10.98/3.42 { p(X) -> n__p(X) 10.98/3.42 , 0() -> n__0() 10.98/3.42 , s(X) -> n__s(X) 10.98/3.42 , if(true(), X, Y) -> activate(X) 10.98/3.42 , if(false(), X, Y) -> activate(Y) 10.98/3.42 , activate(X) -> X 10.98/3.42 , activate(n__0()) -> 0() 10.98/3.42 , activate(n__s(X)) -> s(activate(X)) 10.98/3.42 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.42 , activate(n__p(X)) -> p(activate(X)) 10.98/3.42 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) 10.98/3.42 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.42 Obligation: 10.98/3.42 innermost runtime complexity 10.98/3.42 Answer: 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 The weightgap principle applies (using the following nonconstant 10.98/3.42 growth matrix-interpretation) 10.98/3.42 10.98/3.42 The following argument positions are usable: 10.98/3.42 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.42 10.98/3.42 TcT has computed the following matrix interpretation satisfying 10.98/3.42 not(EDA) and not(IDA(1)). 10.98/3.42 10.98/3.42 [p](x1) = [1] x1 + [7] 10.98/3.42 10.98/3.42 [0] = [7] 10.98/3.42 10.98/3.42 [s](x1) = [1] x1 + [7] 10.98/3.42 10.98/3.42 [leq](x1, x2) = [0] 10.98/3.42 10.98/3.42 [true] = [7] 10.98/3.42 10.98/3.42 [false] = [7] 10.98/3.42 10.98/3.42 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 10.98/3.42 10.98/3.42 [activate](x1) = [1] x1 + [7] 10.98/3.42 10.98/3.42 [diff](x1, x2) = [1] x1 + [1] x2 + [1] 10.98/3.42 10.98/3.42 [n__0] = [1] 10.98/3.42 10.98/3.42 [n__s](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [n__diff](x1, x2) = [1] x1 + [1] x2 + [7] 10.98/3.42 10.98/3.42 [n__p](x1) = [1] x1 + [7] 10.98/3.42 10.98/3.42 The order satisfies the following ordering constraints: 10.98/3.42 10.98/3.42 [p(X)] = [1] X + [7] 10.98/3.42 >= [1] X + [7] 10.98/3.42 = [n__p(X)] 10.98/3.42 10.98/3.42 [0()] = [7] 10.98/3.42 > [1] 10.98/3.42 = [n__0()] 10.98/3.42 10.98/3.42 [s(X)] = [1] X + [7] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [n__s(X)] 10.98/3.42 10.98/3.42 [if(true(), X, Y)] = [1] X + [1] Y + [7] 10.98/3.42 >= [1] X + [7] 10.98/3.42 = [activate(X)] 10.98/3.42 10.98/3.42 [if(false(), X, Y)] = [1] X + [1] Y + [7] 10.98/3.42 >= [1] Y + [7] 10.98/3.42 = [activate(Y)] 10.98/3.42 10.98/3.42 [activate(X)] = [1] X + [7] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [X] 10.98/3.42 10.98/3.42 [activate(n__0())] = [8] 10.98/3.42 > [7] 10.98/3.42 = [0()] 10.98/3.42 10.98/3.42 [activate(n__s(X))] = [1] X + [7] 10.98/3.42 ? [1] X + [14] 10.98/3.42 = [s(activate(X))] 10.98/3.42 10.98/3.42 [activate(n__diff(X1, X2))] = [1] X1 + [1] X2 + [14] 10.98/3.42 ? [1] X1 + [1] X2 + [15] 10.98/3.42 = [diff(activate(X1), activate(X2))] 10.98/3.42 10.98/3.42 [activate(n__p(X))] = [1] X + [14] 10.98/3.42 >= [1] X + [14] 10.98/3.42 = [p(activate(X))] 10.98/3.42 10.98/3.42 [diff(X, Y)] = [1] X + [1] Y + [1] 10.98/3.42 ? [1] X + [1] Y + [15] 10.98/3.42 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.42 10.98/3.42 [diff(X1, X2)] = [1] X1 + [1] X2 + [1] 10.98/3.42 ? [1] X1 + [1] X2 + [7] 10.98/3.42 = [n__diff(X1, X2)] 10.98/3.42 10.98/3.42 10.98/3.42 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 10.98/3.42 10.98/3.42 We are left with following problem, upon which TcT provides the 10.98/3.42 certificate YES(O(1),O(n^1)). 10.98/3.42 10.98/3.42 Strict Trs: 10.98/3.42 { p(X) -> n__p(X) 10.98/3.42 , if(true(), X, Y) -> activate(X) 10.98/3.42 , if(false(), X, Y) -> activate(Y) 10.98/3.42 , activate(n__s(X)) -> s(activate(X)) 10.98/3.42 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.42 , activate(n__p(X)) -> p(activate(X)) 10.98/3.42 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) 10.98/3.42 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.42 Weak Trs: 10.98/3.42 { 0() -> n__0() 10.98/3.42 , s(X) -> n__s(X) 10.98/3.42 , activate(X) -> X 10.98/3.42 , activate(n__0()) -> 0() } 10.98/3.42 Obligation: 10.98/3.42 innermost runtime complexity 10.98/3.42 Answer: 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 The weightgap principle applies (using the following nonconstant 10.98/3.42 growth matrix-interpretation) 10.98/3.42 10.98/3.42 The following argument positions are usable: 10.98/3.42 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.42 10.98/3.42 TcT has computed the following matrix interpretation satisfying 10.98/3.42 not(EDA) and not(IDA(1)). 10.98/3.42 10.98/3.42 [p](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [0] = [0] 10.98/3.42 10.98/3.42 [s](x1) = [1] x1 + [4] 10.98/3.42 10.98/3.42 [leq](x1, x2) = [0] 10.98/3.42 10.98/3.42 [true] = [7] 10.98/3.42 10.98/3.42 [false] = [7] 10.98/3.42 10.98/3.42 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 10.98/3.42 10.98/3.42 [activate](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [diff](x1, x2) = [1] x1 + [1] x2 + [0] 10.98/3.42 10.98/3.42 [n__0] = [0] 10.98/3.42 10.98/3.42 [n__s](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [n__diff](x1, x2) = [1] x1 + [1] x2 + [0] 10.98/3.42 10.98/3.42 [n__p](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 The order satisfies the following ordering constraints: 10.98/3.42 10.98/3.42 [p(X)] = [1] X + [0] 10.98/3.42 >= [1] X + [0] 10.98/3.42 = [n__p(X)] 10.98/3.42 10.98/3.42 [0()] = [0] 10.98/3.42 >= [0] 10.98/3.42 = [n__0()] 10.98/3.42 10.98/3.42 [s(X)] = [1] X + [4] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [n__s(X)] 10.98/3.42 10.98/3.42 [if(true(), X, Y)] = [1] X + [1] Y + [7] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [activate(X)] 10.98/3.42 10.98/3.42 [if(false(), X, Y)] = [1] X + [1] Y + [7] 10.98/3.42 > [1] Y + [0] 10.98/3.42 = [activate(Y)] 10.98/3.42 10.98/3.42 [activate(X)] = [1] X + [0] 10.98/3.42 >= [1] X + [0] 10.98/3.42 = [X] 10.98/3.42 10.98/3.42 [activate(n__0())] = [0] 10.98/3.42 >= [0] 10.98/3.42 = [0()] 10.98/3.42 10.98/3.42 [activate(n__s(X))] = [1] X + [0] 10.98/3.42 ? [1] X + [4] 10.98/3.42 = [s(activate(X))] 10.98/3.42 10.98/3.42 [activate(n__diff(X1, X2))] = [1] X1 + [1] X2 + [0] 10.98/3.42 >= [1] X1 + [1] X2 + [0] 10.98/3.42 = [diff(activate(X1), activate(X2))] 10.98/3.42 10.98/3.42 [activate(n__p(X))] = [1] X + [0] 10.98/3.42 >= [1] X + [0] 10.98/3.42 = [p(activate(X))] 10.98/3.42 10.98/3.42 [diff(X, Y)] = [1] X + [1] Y + [0] 10.98/3.42 >= [1] X + [1] Y + [0] 10.98/3.42 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.42 10.98/3.42 [diff(X1, X2)] = [1] X1 + [1] X2 + [0] 10.98/3.42 >= [1] X1 + [1] X2 + [0] 10.98/3.42 = [n__diff(X1, X2)] 10.98/3.42 10.98/3.42 10.98/3.42 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 10.98/3.42 10.98/3.42 We are left with following problem, upon which TcT provides the 10.98/3.42 certificate YES(O(1),O(n^1)). 10.98/3.42 10.98/3.42 Strict Trs: 10.98/3.42 { p(X) -> n__p(X) 10.98/3.42 , activate(n__s(X)) -> s(activate(X)) 10.98/3.42 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.42 , activate(n__p(X)) -> p(activate(X)) 10.98/3.42 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) 10.98/3.42 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.42 Weak Trs: 10.98/3.42 { 0() -> n__0() 10.98/3.42 , s(X) -> n__s(X) 10.98/3.42 , if(true(), X, Y) -> activate(X) 10.98/3.42 , if(false(), X, Y) -> activate(Y) 10.98/3.42 , activate(X) -> X 10.98/3.42 , activate(n__0()) -> 0() } 10.98/3.42 Obligation: 10.98/3.42 innermost runtime complexity 10.98/3.42 Answer: 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 The weightgap principle applies (using the following nonconstant 10.98/3.42 growth matrix-interpretation) 10.98/3.42 10.98/3.42 The following argument positions are usable: 10.98/3.42 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.42 10.98/3.42 TcT has computed the following matrix interpretation satisfying 10.98/3.42 not(EDA) and not(IDA(1)). 10.98/3.42 10.98/3.42 [p](x1) = [1] x1 + [1] 10.98/3.42 10.98/3.42 [0] = [0] 10.98/3.42 10.98/3.42 [s](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [leq](x1, x2) = [7] 10.98/3.42 10.98/3.42 [true] = [7] 10.98/3.42 10.98/3.42 [false] = [7] 10.98/3.42 10.98/3.42 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4] 10.98/3.42 10.98/3.42 [activate](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [diff](x1, x2) = [1] x1 + [1] x2 + [0] 10.98/3.42 10.98/3.42 [n__0] = [0] 10.98/3.42 10.98/3.42 [n__s](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [n__diff](x1, x2) = [1] x1 + [1] x2 + [0] 10.98/3.42 10.98/3.42 [n__p](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 The order satisfies the following ordering constraints: 10.98/3.42 10.98/3.42 [p(X)] = [1] X + [1] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [n__p(X)] 10.98/3.42 10.98/3.42 [0()] = [0] 10.98/3.42 >= [0] 10.98/3.42 = [n__0()] 10.98/3.42 10.98/3.42 [s(X)] = [1] X + [0] 10.98/3.42 >= [1] X + [0] 10.98/3.42 = [n__s(X)] 10.98/3.42 10.98/3.42 [if(true(), X, Y)] = [1] X + [1] Y + [11] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [activate(X)] 10.98/3.42 10.98/3.42 [if(false(), X, Y)] = [1] X + [1] Y + [11] 10.98/3.42 > [1] Y + [0] 10.98/3.42 = [activate(Y)] 10.98/3.42 10.98/3.42 [activate(X)] = [1] X + [0] 10.98/3.42 >= [1] X + [0] 10.98/3.42 = [X] 10.98/3.42 10.98/3.42 [activate(n__0())] = [0] 10.98/3.42 >= [0] 10.98/3.42 = [0()] 10.98/3.42 10.98/3.42 [activate(n__s(X))] = [1] X + [0] 10.98/3.42 >= [1] X + [0] 10.98/3.42 = [s(activate(X))] 10.98/3.42 10.98/3.42 [activate(n__diff(X1, X2))] = [1] X1 + [1] X2 + [0] 10.98/3.42 >= [1] X1 + [1] X2 + [0] 10.98/3.42 = [diff(activate(X1), activate(X2))] 10.98/3.42 10.98/3.42 [activate(n__p(X))] = [1] X + [0] 10.98/3.42 ? [1] X + [1] 10.98/3.42 = [p(activate(X))] 10.98/3.42 10.98/3.42 [diff(X, Y)] = [1] X + [1] Y + [0] 10.98/3.42 ? [1] X + [1] Y + [11] 10.98/3.42 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.42 10.98/3.42 [diff(X1, X2)] = [1] X1 + [1] X2 + [0] 10.98/3.42 >= [1] X1 + [1] X2 + [0] 10.98/3.42 = [n__diff(X1, X2)] 10.98/3.42 10.98/3.42 10.98/3.42 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 10.98/3.42 10.98/3.42 We are left with following problem, upon which TcT provides the 10.98/3.42 certificate YES(O(1),O(n^1)). 10.98/3.42 10.98/3.42 Strict Trs: 10.98/3.42 { activate(n__s(X)) -> s(activate(X)) 10.98/3.42 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.42 , activate(n__p(X)) -> p(activate(X)) 10.98/3.42 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) 10.98/3.42 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.42 Weak Trs: 10.98/3.42 { p(X) -> n__p(X) 10.98/3.42 , 0() -> n__0() 10.98/3.42 , s(X) -> n__s(X) 10.98/3.42 , if(true(), X, Y) -> activate(X) 10.98/3.42 , if(false(), X, Y) -> activate(Y) 10.98/3.42 , activate(X) -> X 10.98/3.42 , activate(n__0()) -> 0() } 10.98/3.42 Obligation: 10.98/3.42 innermost runtime complexity 10.98/3.42 Answer: 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 The weightgap principle applies (using the following nonconstant 10.98/3.42 growth matrix-interpretation) 10.98/3.42 10.98/3.42 The following argument positions are usable: 10.98/3.42 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.42 10.98/3.42 TcT has computed the following matrix interpretation satisfying 10.98/3.42 not(EDA) and not(IDA(1)). 10.98/3.42 10.98/3.42 [p](x1) = [1] x1 + [4] 10.98/3.42 10.98/3.42 [0] = [0] 10.98/3.42 10.98/3.42 [s](x1) = [1] x1 + [4] 10.98/3.42 10.98/3.42 [leq](x1, x2) = [3] 10.98/3.42 10.98/3.42 [true] = [7] 10.98/3.42 10.98/3.42 [false] = [7] 10.98/3.42 10.98/3.42 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 10.98/3.42 10.98/3.42 [activate](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [diff](x1, x2) = [1] x1 + [1] x2 + [0] 10.98/3.42 10.98/3.42 [n__0] = [0] 10.98/3.42 10.98/3.42 [n__s](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 [n__diff](x1, x2) = [1] x1 + [1] x2 + [1] 10.98/3.42 10.98/3.42 [n__p](x1) = [1] x1 + [0] 10.98/3.42 10.98/3.42 The order satisfies the following ordering constraints: 10.98/3.42 10.98/3.42 [p(X)] = [1] X + [4] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [n__p(X)] 10.98/3.42 10.98/3.42 [0()] = [0] 10.98/3.42 >= [0] 10.98/3.42 = [n__0()] 10.98/3.42 10.98/3.42 [s(X)] = [1] X + [4] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [n__s(X)] 10.98/3.42 10.98/3.42 [if(true(), X, Y)] = [1] X + [1] Y + [14] 10.98/3.42 > [1] X + [0] 10.98/3.42 = [activate(X)] 10.98/3.42 10.98/3.42 [if(false(), X, Y)] = [1] X + [1] Y + [14] 10.98/3.42 > [1] Y + [0] 10.98/3.42 = [activate(Y)] 10.98/3.42 10.98/3.42 [activate(X)] = [1] X + [0] 10.98/3.42 >= [1] X + [0] 10.98/3.42 = [X] 10.98/3.42 10.98/3.42 [activate(n__0())] = [0] 10.98/3.42 >= [0] 10.98/3.42 = [0()] 10.98/3.42 10.98/3.42 [activate(n__s(X))] = [1] X + [0] 10.98/3.42 ? [1] X + [4] 10.98/3.42 = [s(activate(X))] 10.98/3.42 10.98/3.42 [activate(n__diff(X1, X2))] = [1] X1 + [1] X2 + [1] 10.98/3.42 > [1] X1 + [1] X2 + [0] 10.98/3.42 = [diff(activate(X1), activate(X2))] 10.98/3.42 10.98/3.42 [activate(n__p(X))] = [1] X + [0] 10.98/3.42 ? [1] X + [4] 10.98/3.42 = [p(activate(X))] 10.98/3.42 10.98/3.42 [diff(X, Y)] = [1] X + [1] Y + [0] 10.98/3.42 ? [1] X + [1] Y + [11] 10.98/3.42 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.42 10.98/3.42 [diff(X1, X2)] = [1] X1 + [1] X2 + [0] 10.98/3.42 ? [1] X1 + [1] X2 + [1] 10.98/3.42 = [n__diff(X1, X2)] 10.98/3.42 10.98/3.42 10.98/3.42 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 10.98/3.42 10.98/3.42 We are left with following problem, upon which TcT provides the 10.98/3.42 certificate YES(O(1),O(n^1)). 10.98/3.42 10.98/3.42 Strict Trs: 10.98/3.42 { activate(n__s(X)) -> s(activate(X)) 10.98/3.42 , activate(n__p(X)) -> p(activate(X)) 10.98/3.42 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) 10.98/3.42 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.42 Weak Trs: 10.98/3.42 { p(X) -> n__p(X) 10.98/3.42 , 0() -> n__0() 10.98/3.42 , s(X) -> n__s(X) 10.98/3.42 , if(true(), X, Y) -> activate(X) 10.98/3.42 , if(false(), X, Y) -> activate(Y) 10.98/3.42 , activate(X) -> X 10.98/3.42 , activate(n__0()) -> 0() 10.98/3.42 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) } 10.98/3.42 Obligation: 10.98/3.42 innermost runtime complexity 10.98/3.42 Answer: 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 We use the processor 'polynomial interpretation' to orient 10.98/3.42 following rules strictly. 10.98/3.42 10.98/3.42 Trs: 10.98/3.42 { diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) } 10.98/3.42 10.98/3.42 The induced complexity on above rules (modulo remaining rules) is 10.98/3.42 YES(?,O(n^1)) . These rules are moved into the corresponding weak 10.98/3.42 component(s). 10.98/3.42 10.98/3.42 Sub-proof: 10.98/3.42 ---------- 10.98/3.42 We consider the following typing: 10.98/3.42 10.98/3.42 p :: a -> a 10.98/3.42 0 :: a 10.98/3.42 s :: a -> a 10.98/3.42 leq :: (a,a) -> b 10.98/3.42 true :: b 10.98/3.42 false :: b 10.98/3.42 if :: (b,a,a) -> a 10.98/3.42 activate :: a -> a 10.98/3.42 diff :: (a,a) -> a 10.98/3.42 n__0 :: a 10.98/3.42 n__s :: a -> a 10.98/3.42 n__diff :: (a,a) -> a 10.98/3.42 n__p :: a -> a 10.98/3.42 10.98/3.42 The following argument positions are considered usable: 10.98/3.42 10.98/3.42 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.42 10.98/3.42 TcT has computed the following constructor-restricted 10.98/3.42 typedpolynomial interpretation. 10.98/3.42 10.98/3.42 [p](x1) = x1 10.98/3.42 10.98/3.42 [0]() = 0 10.98/3.42 10.98/3.42 [s](x1) = x1 10.98/3.42 10.98/3.42 [leq](x1, x2) = 0 10.98/3.42 10.98/3.42 [true]() = 0 10.98/3.42 10.98/3.42 [false]() = 2 10.98/3.42 10.98/3.42 [if](x1, x2, x3) = 2*x1*x3 + x2 10.98/3.42 10.98/3.42 [activate](x1) = x1 10.98/3.42 10.98/3.42 [diff](x1, x2) = 1 + x1 + x2 10.98/3.42 10.98/3.42 [n__0]() = 0 10.98/3.42 10.98/3.42 [n__s](x1) = x1 10.98/3.42 10.98/3.42 [n__diff](x1, x2) = 1 + x1 + x2 10.98/3.42 10.98/3.42 [n__p](x1) = x1 10.98/3.42 10.98/3.42 10.98/3.42 This order satisfies the following ordering constraints. 10.98/3.42 10.98/3.42 [p(X)] = X 10.98/3.42 >= X 10.98/3.42 = [n__p(X)] 10.98/3.42 10.98/3.42 [0()] = 10.98/3.42 >= 10.98/3.42 = [n__0()] 10.98/3.42 10.98/3.42 [s(X)] = X 10.98/3.42 >= X 10.98/3.42 = [n__s(X)] 10.98/3.42 10.98/3.42 [if(true(), X, Y)] = X 10.98/3.42 >= X 10.98/3.42 = [activate(X)] 10.98/3.42 10.98/3.42 [if(false(), X, Y)] = 4*Y + X 10.98/3.42 >= Y 10.98/3.42 = [activate(Y)] 10.98/3.42 10.98/3.42 [activate(X)] = X 10.98/3.42 >= X 10.98/3.42 = [X] 10.98/3.42 10.98/3.42 [activate(n__0())] = 10.98/3.42 >= 10.98/3.42 = [0()] 10.98/3.42 10.98/3.42 [activate(n__s(X))] = X 10.98/3.42 >= X 10.98/3.42 = [s(activate(X))] 10.98/3.42 10.98/3.42 [activate(n__diff(X1, X2))] = 1 + X1 + X2 10.98/3.42 >= 1 + X1 + X2 10.98/3.42 = [diff(activate(X1), activate(X2))] 10.98/3.42 10.98/3.42 [activate(n__p(X))] = X 10.98/3.42 >= X 10.98/3.42 = [p(activate(X))] 10.98/3.42 10.98/3.42 [diff(X, Y)] = 1 + X + Y 10.98/3.42 > 10.98/3.42 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.42 10.98/3.42 [diff(X1, X2)] = 1 + X1 + X2 10.98/3.42 >= 1 + X1 + X2 10.98/3.42 = [n__diff(X1, X2)] 10.98/3.42 10.98/3.42 10.98/3.42 We return to the main proof. 10.98/3.42 10.98/3.42 We are left with following problem, upon which TcT provides the 10.98/3.42 certificate YES(O(1),O(n^1)). 10.98/3.42 10.98/3.42 Strict Trs: 10.98/3.42 { activate(n__s(X)) -> s(activate(X)) 10.98/3.42 , activate(n__p(X)) -> p(activate(X)) 10.98/3.42 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.42 Weak Trs: 10.98/3.42 { p(X) -> n__p(X) 10.98/3.42 , 0() -> n__0() 10.98/3.42 , s(X) -> n__s(X) 10.98/3.42 , if(true(), X, Y) -> activate(X) 10.98/3.42 , if(false(), X, Y) -> activate(Y) 10.98/3.42 , activate(X) -> X 10.98/3.42 , activate(n__0()) -> 0() 10.98/3.42 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.42 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) } 10.98/3.42 Obligation: 10.98/3.42 innermost runtime complexity 10.98/3.42 Answer: 10.98/3.42 YES(O(1),O(n^1)) 10.98/3.42 10.98/3.42 We use the processor 'polynomial interpretation' to orient 10.98/3.42 following rules strictly. 10.98/3.42 10.98/3.42 Trs: { activate(n__s(X)) -> s(activate(X)) } 10.98/3.42 10.98/3.42 The induced complexity on above rules (modulo remaining rules) is 10.98/3.42 YES(?,O(n^1)) . These rules are moved into the corresponding weak 10.98/3.42 component(s). 10.98/3.42 10.98/3.42 Sub-proof: 10.98/3.42 ---------- 10.98/3.42 We consider the following typing: 10.98/3.42 10.98/3.42 p :: a -> a 10.98/3.42 0 :: a 10.98/3.42 s :: a -> a 10.98/3.42 leq :: (a,a) -> b 10.98/3.42 true :: b 10.98/3.42 false :: b 10.98/3.42 if :: (b,a,a) -> a 10.98/3.42 activate :: a -> a 10.98/3.42 diff :: (a,a) -> a 10.98/3.42 n__0 :: a 10.98/3.42 n__s :: a -> a 10.98/3.42 n__diff :: (a,a) -> a 10.98/3.42 n__p :: a -> a 10.98/3.42 10.98/3.43 The following argument positions are considered usable: 10.98/3.43 10.98/3.43 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.43 10.98/3.43 TcT has computed the following constructor-restricted 10.98/3.43 typedpolynomial interpretation. 10.98/3.43 10.98/3.43 [p](x1) = x1 10.98/3.43 10.98/3.43 [0]() = 0 10.98/3.43 10.98/3.43 [s](x1) = 2 + x1 10.98/3.43 10.98/3.43 [leq](x1, x2) = 0 10.98/3.43 10.98/3.43 [true]() = 0 10.98/3.43 10.98/3.43 [false]() = 2 10.98/3.43 10.98/3.43 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 10.98/3.43 10.98/3.43 [activate](x1) = 2*x1 10.98/3.43 10.98/3.43 [diff](x1, x2) = 2 + x1 + x2 10.98/3.43 10.98/3.43 [n__0]() = 0 10.98/3.43 10.98/3.43 [n__s](x1) = 2 + x1 10.98/3.43 10.98/3.43 [n__diff](x1, x2) = 2 + x1 + x2 10.98/3.43 10.98/3.43 [n__p](x1) = x1 10.98/3.43 10.98/3.43 10.98/3.43 This order satisfies the following ordering constraints. 10.98/3.43 10.98/3.43 [p(X)] = X 10.98/3.43 >= X 10.98/3.43 = [n__p(X)] 10.98/3.43 10.98/3.43 [0()] = 10.98/3.43 >= 10.98/3.43 = [n__0()] 10.98/3.43 10.98/3.43 [s(X)] = 2 + X 10.98/3.43 >= 2 + X 10.98/3.43 = [n__s(X)] 10.98/3.43 10.98/3.43 [if(true(), X, Y)] = 2*X 10.98/3.43 >= 2*X 10.98/3.43 = [activate(X)] 10.98/3.43 10.98/3.43 [if(false(), X, Y)] = 4*Y + 2*X 10.98/3.43 >= 2*Y 10.98/3.43 = [activate(Y)] 10.98/3.43 10.98/3.43 [activate(X)] = 2*X 10.98/3.43 >= X 10.98/3.43 = [X] 10.98/3.43 10.98/3.43 [activate(n__0())] = 10.98/3.43 >= 10.98/3.43 = [0()] 10.98/3.43 10.98/3.43 [activate(n__s(X))] = 4 + 2*X 10.98/3.43 > 2 + 2*X 10.98/3.43 = [s(activate(X))] 10.98/3.43 10.98/3.43 [activate(n__diff(X1, X2))] = 4 + 2*X1 + 2*X2 10.98/3.43 > 2 + 2*X1 + 2*X2 10.98/3.43 = [diff(activate(X1), activate(X2))] 10.98/3.43 10.98/3.43 [activate(n__p(X))] = 2*X 10.98/3.43 >= 2*X 10.98/3.43 = [p(activate(X))] 10.98/3.43 10.98/3.43 [diff(X, Y)] = 2 + X + Y 10.98/3.43 > 10.98/3.43 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.43 10.98/3.43 [diff(X1, X2)] = 2 + X1 + X2 10.98/3.43 >= 2 + X1 + X2 10.98/3.43 = [n__diff(X1, X2)] 10.98/3.43 10.98/3.43 10.98/3.43 We return to the main proof. 10.98/3.43 10.98/3.43 We are left with following problem, upon which TcT provides the 10.98/3.43 certificate YES(O(1),O(n^1)). 10.98/3.43 10.98/3.43 Strict Trs: 10.98/3.43 { activate(n__p(X)) -> p(activate(X)) 10.98/3.43 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.43 Weak Trs: 10.98/3.43 { p(X) -> n__p(X) 10.98/3.43 , 0() -> n__0() 10.98/3.43 , s(X) -> n__s(X) 10.98/3.43 , if(true(), X, Y) -> activate(X) 10.98/3.43 , if(false(), X, Y) -> activate(Y) 10.98/3.43 , activate(X) -> X 10.98/3.43 , activate(n__0()) -> 0() 10.98/3.43 , activate(n__s(X)) -> s(activate(X)) 10.98/3.43 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.43 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) } 10.98/3.43 Obligation: 10.98/3.43 innermost runtime complexity 10.98/3.43 Answer: 10.98/3.43 YES(O(1),O(n^1)) 10.98/3.43 10.98/3.43 We use the processor 'polynomial interpretation' to orient 10.98/3.43 following rules strictly. 10.98/3.43 10.98/3.43 Trs: { activate(n__p(X)) -> p(activate(X)) } 10.98/3.43 10.98/3.43 The induced complexity on above rules (modulo remaining rules) is 10.98/3.43 YES(?,O(n^1)) . These rules are moved into the corresponding weak 10.98/3.43 component(s). 10.98/3.43 10.98/3.43 Sub-proof: 10.98/3.43 ---------- 10.98/3.43 We consider the following typing: 10.98/3.43 10.98/3.43 p :: a -> a 10.98/3.43 0 :: a 10.98/3.43 s :: a -> a 10.98/3.43 leq :: (a,a) -> b 10.98/3.43 true :: b 10.98/3.43 false :: b 10.98/3.43 if :: (b,a,a) -> a 10.98/3.43 activate :: a -> a 10.98/3.43 diff :: (a,a) -> a 10.98/3.43 n__0 :: a 10.98/3.43 n__s :: a -> a 10.98/3.43 n__diff :: (a,a) -> a 10.98/3.43 n__p :: a -> a 10.98/3.43 10.98/3.43 The following argument positions are considered usable: 10.98/3.43 10.98/3.43 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.43 10.98/3.43 TcT has computed the following constructor-restricted 10.98/3.43 typedpolynomial interpretation. 10.98/3.43 10.98/3.43 [p](x1) = 2 + x1 10.98/3.43 10.98/3.43 [0]() = 0 10.98/3.43 10.98/3.43 [s](x1) = x1 10.98/3.43 10.98/3.43 [leq](x1, x2) = 0 10.98/3.43 10.98/3.43 [true]() = 1 10.98/3.43 10.98/3.43 [false]() = 2 10.98/3.43 10.98/3.43 [if](x1, x2, x3) = 3*x1*x2 + 2*x1*x3 + x2 10.98/3.43 10.98/3.43 [activate](x1) = 2*x1 10.98/3.43 10.98/3.43 [diff](x1, x2) = x1 + x2 10.98/3.43 10.98/3.43 [n__0]() = 0 10.98/3.43 10.98/3.43 [n__s](x1) = x1 10.98/3.43 10.98/3.43 [n__diff](x1, x2) = x1 + x2 10.98/3.43 10.98/3.43 [n__p](x1) = 2 + x1 10.98/3.43 10.98/3.43 10.98/3.43 This order satisfies the following ordering constraints. 10.98/3.43 10.98/3.43 [p(X)] = 2 + X 10.98/3.43 >= 2 + X 10.98/3.43 = [n__p(X)] 10.98/3.43 10.98/3.43 [0()] = 10.98/3.43 >= 10.98/3.43 = [n__0()] 10.98/3.43 10.98/3.43 [s(X)] = X 10.98/3.43 >= X 10.98/3.43 = [n__s(X)] 10.98/3.43 10.98/3.43 [if(true(), X, Y)] = 4*X + 2*Y 10.98/3.43 >= 2*X 10.98/3.43 = [activate(X)] 10.98/3.43 10.98/3.43 [if(false(), X, Y)] = 7*X + 4*Y 10.98/3.43 >= 2*Y 10.98/3.43 = [activate(Y)] 10.98/3.43 10.98/3.43 [activate(X)] = 2*X 10.98/3.43 >= X 10.98/3.43 = [X] 10.98/3.43 10.98/3.43 [activate(n__0())] = 10.98/3.43 >= 10.98/3.43 = [0()] 10.98/3.43 10.98/3.43 [activate(n__s(X))] = 2*X 10.98/3.43 >= 2*X 10.98/3.43 = [s(activate(X))] 10.98/3.43 10.98/3.43 [activate(n__diff(X1, X2))] = 2*X1 + 2*X2 10.98/3.43 >= 2*X1 + 2*X2 10.98/3.43 = [diff(activate(X1), activate(X2))] 10.98/3.43 10.98/3.43 [activate(n__p(X))] = 4 + 2*X 10.98/3.43 > 2 + 2*X 10.98/3.43 = [p(activate(X))] 10.98/3.43 10.98/3.43 [diff(X, Y)] = X + Y 10.98/3.43 >= 10.98/3.43 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.43 10.98/3.43 [diff(X1, X2)] = X1 + X2 10.98/3.43 >= X1 + X2 10.98/3.43 = [n__diff(X1, X2)] 10.98/3.43 10.98/3.43 10.98/3.43 We return to the main proof. 10.98/3.43 10.98/3.43 We are left with following problem, upon which TcT provides the 10.98/3.43 certificate YES(O(1),O(n^1)). 10.98/3.43 10.98/3.43 Strict Trs: { diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.43 Weak Trs: 10.98/3.43 { p(X) -> n__p(X) 10.98/3.43 , 0() -> n__0() 10.98/3.43 , s(X) -> n__s(X) 10.98/3.43 , if(true(), X, Y) -> activate(X) 10.98/3.43 , if(false(), X, Y) -> activate(Y) 10.98/3.43 , activate(X) -> X 10.98/3.43 , activate(n__0()) -> 0() 10.98/3.43 , activate(n__s(X)) -> s(activate(X)) 10.98/3.43 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.43 , activate(n__p(X)) -> p(activate(X)) 10.98/3.43 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) } 10.98/3.43 Obligation: 10.98/3.43 innermost runtime complexity 10.98/3.43 Answer: 10.98/3.43 YES(O(1),O(n^1)) 10.98/3.43 10.98/3.43 We use the processor 'polynomial interpretation' to orient 10.98/3.43 following rules strictly. 10.98/3.43 10.98/3.43 Trs: { diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.43 10.98/3.43 The induced complexity on above rules (modulo remaining rules) is 10.98/3.43 YES(?,O(n^1)) . These rules are moved into the corresponding weak 10.98/3.43 component(s). 10.98/3.43 10.98/3.43 Sub-proof: 10.98/3.43 ---------- 10.98/3.43 We consider the following typing: 10.98/3.43 10.98/3.43 p :: a -> a 10.98/3.43 0 :: a 10.98/3.43 s :: a -> a 10.98/3.43 leq :: (a,a) -> b 10.98/3.43 true :: b 10.98/3.43 false :: b 10.98/3.43 if :: (b,a,a) -> a 10.98/3.43 activate :: a -> a 10.98/3.43 diff :: (a,a) -> a 10.98/3.43 n__0 :: a 10.98/3.43 n__s :: a -> a 10.98/3.43 n__diff :: (a,a) -> a 10.98/3.43 n__p :: a -> a 10.98/3.43 10.98/3.43 The following argument positions are considered usable: 10.98/3.43 10.98/3.43 Uargs(p) = {1}, Uargs(s) = {1}, Uargs(diff) = {1, 2} 10.98/3.43 10.98/3.43 TcT has computed the following constructor-restricted 10.98/3.43 typedpolynomial interpretation. 10.98/3.43 10.98/3.43 [p](x1) = x1 10.98/3.43 10.98/3.43 [0]() = 0 10.98/3.43 10.98/3.43 [s](x1) = x1 10.98/3.43 10.98/3.43 [leq](x1, x2) = 0 10.98/3.43 10.98/3.43 [true]() = 0 10.98/3.43 10.98/3.43 [false]() = 2 10.98/3.43 10.98/3.43 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 10.98/3.43 10.98/3.43 [activate](x1) = 2*x1 10.98/3.43 10.98/3.43 [diff](x1, x2) = 3 + x1 + x2 10.98/3.43 10.98/3.43 [n__0]() = 0 10.98/3.43 10.98/3.43 [n__s](x1) = x1 10.98/3.43 10.98/3.43 [n__diff](x1, x2) = 2 + x1 + x2 10.98/3.43 10.98/3.43 [n__p](x1) = x1 10.98/3.43 10.98/3.43 10.98/3.43 This order satisfies the following ordering constraints. 10.98/3.43 10.98/3.43 [p(X)] = X 10.98/3.43 >= X 10.98/3.43 = [n__p(X)] 10.98/3.43 10.98/3.43 [0()] = 10.98/3.43 >= 10.98/3.43 = [n__0()] 10.98/3.43 10.98/3.43 [s(X)] = X 10.98/3.43 >= X 10.98/3.43 = [n__s(X)] 10.98/3.43 10.98/3.43 [if(true(), X, Y)] = 2*X 10.98/3.43 >= 2*X 10.98/3.43 = [activate(X)] 10.98/3.43 10.98/3.43 [if(false(), X, Y)] = 4*Y + 2*X 10.98/3.43 >= 2*Y 10.98/3.43 = [activate(Y)] 10.98/3.43 10.98/3.43 [activate(X)] = 2*X 10.98/3.43 >= X 10.98/3.43 = [X] 10.98/3.43 10.98/3.43 [activate(n__0())] = 10.98/3.43 >= 10.98/3.43 = [0()] 10.98/3.43 10.98/3.43 [activate(n__s(X))] = 2*X 10.98/3.43 >= 2*X 10.98/3.43 = [s(activate(X))] 10.98/3.43 10.98/3.43 [activate(n__diff(X1, X2))] = 4 + 2*X1 + 2*X2 10.98/3.43 > 3 + 2*X1 + 2*X2 10.98/3.43 = [diff(activate(X1), activate(X2))] 10.98/3.43 10.98/3.43 [activate(n__p(X))] = 2*X 10.98/3.43 >= 2*X 10.98/3.43 = [p(activate(X))] 10.98/3.43 10.98/3.43 [diff(X, Y)] = 3 + X + Y 10.98/3.43 > 10.98/3.43 = [if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))] 10.98/3.43 10.98/3.43 [diff(X1, X2)] = 3 + X1 + X2 10.98/3.43 > 2 + X1 + X2 10.98/3.43 = [n__diff(X1, X2)] 10.98/3.43 10.98/3.43 10.98/3.43 We return to the main proof. 10.98/3.43 10.98/3.43 We are left with following problem, upon which TcT provides the 10.98/3.43 certificate YES(O(1),O(1)). 10.98/3.43 10.98/3.43 Weak Trs: 10.98/3.43 { p(X) -> n__p(X) 10.98/3.43 , 0() -> n__0() 10.98/3.43 , s(X) -> n__s(X) 10.98/3.43 , if(true(), X, Y) -> activate(X) 10.98/3.43 , if(false(), X, Y) -> activate(Y) 10.98/3.43 , activate(X) -> X 10.98/3.43 , activate(n__0()) -> 0() 10.98/3.43 , activate(n__s(X)) -> s(activate(X)) 10.98/3.43 , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) 10.98/3.43 , activate(n__p(X)) -> p(activate(X)) 10.98/3.43 , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) 10.98/3.43 , diff(X1, X2) -> n__diff(X1, X2) } 10.98/3.43 Obligation: 10.98/3.43 innermost runtime complexity 10.98/3.43 Answer: 10.98/3.43 YES(O(1),O(1)) 10.98/3.43 10.98/3.43 Empty rules are trivially bounded 10.98/3.43 10.98/3.43 Hurray, we answered YES(O(1),O(n^1)) 10.98/3.44 EOF