YES(O(1),O(n^1)) 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 We are left with following problem, upon which TcT provides the 29.07/10.23 certificate YES(O(1),O(n^1)). 29.07/10.23 29.07/10.23 Strict Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.23 , fact(X) -> n__fact(X) 29.07/10.23 , if(true(), X, Y) -> activate(X) 29.07/10.23 , if(false(), X, Y) -> activate(Y) 29.07/10.23 , zero(0()) -> true() 29.07/10.23 , zero(s(X)) -> false() 29.07/10.23 , add(0(), X) -> X 29.07/10.23 , add(s(X), Y) -> s(add(X, Y)) 29.07/10.23 , 0() -> n__0() 29.07/10.23 , s(X) -> n__s(X) 29.07/10.23 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.23 , prod(0(), X) -> 0() 29.07/10.23 , prod(s(X), Y) -> add(Y, prod(X, Y)) 29.07/10.23 , activate(X) -> X 29.07/10.23 , activate(n__s(X)) -> s(activate(X)) 29.07/10.23 , activate(n__0()) -> 0() 29.07/10.23 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.23 , activate(n__p(X)) -> p(activate(X)) 29.07/10.23 , p(X) -> n__p(X) 29.07/10.23 , p(s(X)) -> X } 29.07/10.23 Obligation: 29.07/10.23 innermost runtime complexity 29.07/10.23 Answer: 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 Arguments of following rules are not normal-forms: 29.07/10.23 29.07/10.23 { zero(0()) -> true() 29.07/10.23 , zero(s(X)) -> false() 29.07/10.23 , add(0(), X) -> X 29.07/10.23 , add(s(X), Y) -> s(add(X, Y)) 29.07/10.23 , prod(0(), X) -> 0() 29.07/10.23 , prod(s(X), Y) -> add(Y, prod(X, Y)) 29.07/10.23 , p(s(X)) -> X } 29.07/10.23 29.07/10.23 All above mentioned rules can be savely removed. 29.07/10.23 29.07/10.23 We are left with following problem, upon which TcT provides the 29.07/10.23 certificate YES(O(1),O(n^1)). 29.07/10.23 29.07/10.23 Strict Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.23 , fact(X) -> n__fact(X) 29.07/10.23 , if(true(), X, Y) -> activate(X) 29.07/10.23 , if(false(), X, Y) -> activate(Y) 29.07/10.23 , 0() -> n__0() 29.07/10.23 , s(X) -> n__s(X) 29.07/10.23 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.23 , activate(X) -> X 29.07/10.23 , activate(n__s(X)) -> s(activate(X)) 29.07/10.23 , activate(n__0()) -> 0() 29.07/10.23 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.23 , activate(n__p(X)) -> p(activate(X)) 29.07/10.23 , p(X) -> n__p(X) } 29.07/10.23 Obligation: 29.07/10.23 innermost runtime complexity 29.07/10.23 Answer: 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 We use the processor 'polynomial interpretation' to orient 29.07/10.23 following rules strictly. 29.07/10.23 29.07/10.23 Trs: { if(false(), X, Y) -> activate(Y) } 29.07/10.23 29.07/10.23 The induced complexity on above rules (modulo remaining rules) is 29.07/10.23 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.23 component(s). 29.07/10.23 29.07/10.23 Sub-proof: 29.07/10.23 ---------- 29.07/10.23 We consider the following typing: 29.07/10.23 29.07/10.23 fact :: b -> b 29.07/10.23 if :: (a,b,b) -> b 29.07/10.23 zero :: b -> a 29.07/10.23 n__s :: b -> b 29.07/10.23 n__0 :: b 29.07/10.23 n__prod :: (b,b) -> b 29.07/10.23 n__fact :: b -> b 29.07/10.23 n__p :: b -> b 29.07/10.23 0 :: b 29.07/10.23 s :: b -> b 29.07/10.23 prod :: (b,b) -> b 29.07/10.23 true :: a 29.07/10.23 activate :: b -> b 29.07/10.23 false :: a 29.07/10.23 p :: b -> b 29.07/10.23 29.07/10.23 The following argument positions are considered usable: 29.07/10.23 29.07/10.23 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.23 Uargs(p) = {1} 29.07/10.23 29.07/10.23 TcT has computed the following constructor-restricted 29.07/10.23 typedpolynomial interpretation. 29.07/10.23 29.07/10.23 [fact](x1) = x1 29.07/10.23 29.07/10.23 [if](x1, x2, x3) = x1 + 2*x1*x3 + 2*x2 29.07/10.23 29.07/10.23 [zero](x1) = 0 29.07/10.23 29.07/10.23 [n__s](x1) = x1 29.07/10.23 29.07/10.23 [n__0]() = 0 29.07/10.23 29.07/10.23 [n__prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [n__fact](x1) = x1 29.07/10.23 29.07/10.23 [n__p](x1) = x1 29.07/10.23 29.07/10.23 [0]() = 0 29.07/10.23 29.07/10.23 [s](x1) = x1 29.07/10.23 29.07/10.23 [prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [true]() = 0 29.07/10.23 29.07/10.23 [activate](x1) = 2*x1 29.07/10.23 29.07/10.23 [false]() = 2 29.07/10.23 29.07/10.23 [p](x1) = x1 29.07/10.23 29.07/10.23 29.07/10.23 This order satisfies the following ordering constraints. 29.07/10.23 29.07/10.23 [fact(X)] = X 29.07/10.23 >= 29.07/10.23 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.23 29.07/10.23 [fact(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__fact(X)] 29.07/10.23 29.07/10.23 [if(true(), X, Y)] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [activate(X)] 29.07/10.23 29.07/10.23 [if(false(), X, Y)] = 2 + 4*Y + 2*X 29.07/10.23 > 2*Y 29.07/10.23 = [activate(Y)] 29.07/10.23 29.07/10.23 [0()] = 29.07/10.23 >= 29.07/10.23 = [n__0()] 29.07/10.23 29.07/10.23 [s(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__s(X)] 29.07/10.23 29.07/10.23 [prod(X1, X2)] = X1 + X2 29.07/10.23 >= X1 + X2 29.07/10.23 = [n__prod(X1, X2)] 29.07/10.23 29.07/10.23 [activate(X)] = 2*X 29.07/10.23 >= X 29.07/10.23 = [X] 29.07/10.23 29.07/10.23 [activate(n__s(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [s(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__0())] = 29.07/10.23 >= 29.07/10.23 = [0()] 29.07/10.23 29.07/10.23 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.23 >= 2*X1 + 2*X2 29.07/10.23 = [prod(activate(X1), activate(X2))] 29.07/10.23 29.07/10.23 [activate(n__fact(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [fact(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__p(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [p(activate(X))] 29.07/10.23 29.07/10.23 [p(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__p(X)] 29.07/10.23 29.07/10.23 29.07/10.23 We return to the main proof. 29.07/10.23 29.07/10.23 We are left with following problem, upon which TcT provides the 29.07/10.23 certificate YES(O(1),O(n^1)). 29.07/10.23 29.07/10.23 Strict Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.23 , fact(X) -> n__fact(X) 29.07/10.23 , if(true(), X, Y) -> activate(X) 29.07/10.23 , 0() -> n__0() 29.07/10.23 , s(X) -> n__s(X) 29.07/10.23 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.23 , activate(X) -> X 29.07/10.23 , activate(n__s(X)) -> s(activate(X)) 29.07/10.23 , activate(n__0()) -> 0() 29.07/10.23 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.23 , activate(n__p(X)) -> p(activate(X)) 29.07/10.23 , p(X) -> n__p(X) } 29.07/10.23 Weak Trs: { if(false(), X, Y) -> activate(Y) } 29.07/10.23 Obligation: 29.07/10.23 innermost runtime complexity 29.07/10.23 Answer: 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 We use the processor 'polynomial interpretation' to orient 29.07/10.23 following rules strictly. 29.07/10.23 29.07/10.23 Trs: 29.07/10.23 { if(true(), X, Y) -> activate(X) 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) } 29.07/10.23 29.07/10.23 The induced complexity on above rules (modulo remaining rules) is 29.07/10.23 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.23 component(s). 29.07/10.23 29.07/10.23 Sub-proof: 29.07/10.23 ---------- 29.07/10.23 We consider the following typing: 29.07/10.23 29.07/10.23 fact :: b -> b 29.07/10.23 if :: (a,b,b) -> b 29.07/10.23 zero :: b -> a 29.07/10.23 n__s :: b -> b 29.07/10.23 n__0 :: b 29.07/10.23 n__prod :: (b,b) -> b 29.07/10.23 n__fact :: b -> b 29.07/10.23 n__p :: b -> b 29.07/10.23 0 :: b 29.07/10.23 s :: b -> b 29.07/10.23 prod :: (b,b) -> b 29.07/10.23 true :: a 29.07/10.23 activate :: b -> b 29.07/10.23 false :: a 29.07/10.23 p :: b -> b 29.07/10.23 29.07/10.23 The following argument positions are considered usable: 29.07/10.23 29.07/10.23 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.23 Uargs(p) = {1} 29.07/10.23 29.07/10.23 TcT has computed the following constructor-restricted 29.07/10.23 typedpolynomial interpretation. 29.07/10.23 29.07/10.23 [fact](x1) = 1 + x1 29.07/10.23 29.07/10.23 [if](x1, x2, x3) = 1 + 2*x1*x3 + 2*x2 29.07/10.23 29.07/10.23 [zero](x1) = 0 29.07/10.23 29.07/10.23 [n__s](x1) = x1 29.07/10.23 29.07/10.23 [n__0]() = 0 29.07/10.23 29.07/10.23 [n__prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [n__fact](x1) = 1 + x1 29.07/10.23 29.07/10.23 [n__p](x1) = x1 29.07/10.23 29.07/10.23 [0]() = 0 29.07/10.23 29.07/10.23 [s](x1) = x1 29.07/10.23 29.07/10.23 [prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [true]() = 0 29.07/10.23 29.07/10.23 [activate](x1) = 2*x1 29.07/10.23 29.07/10.23 [false]() = 1 29.07/10.23 29.07/10.23 [p](x1) = x1 29.07/10.23 29.07/10.23 29.07/10.23 This order satisfies the following ordering constraints. 29.07/10.23 29.07/10.23 [fact(X)] = 1 + X 29.07/10.23 >= 1 29.07/10.23 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.23 29.07/10.23 [fact(X)] = 1 + X 29.07/10.23 >= 1 + X 29.07/10.23 = [n__fact(X)] 29.07/10.23 29.07/10.23 [if(true(), X, Y)] = 1 + 2*X 29.07/10.23 > 2*X 29.07/10.23 = [activate(X)] 29.07/10.23 29.07/10.23 [if(false(), X, Y)] = 1 + 2*Y + 2*X 29.07/10.23 > 2*Y 29.07/10.23 = [activate(Y)] 29.07/10.23 29.07/10.23 [0()] = 29.07/10.23 >= 29.07/10.23 = [n__0()] 29.07/10.23 29.07/10.23 [s(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__s(X)] 29.07/10.23 29.07/10.23 [prod(X1, X2)] = X1 + X2 29.07/10.23 >= X1 + X2 29.07/10.23 = [n__prod(X1, X2)] 29.07/10.23 29.07/10.23 [activate(X)] = 2*X 29.07/10.23 >= X 29.07/10.23 = [X] 29.07/10.23 29.07/10.23 [activate(n__s(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [s(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__0())] = 29.07/10.23 >= 29.07/10.23 = [0()] 29.07/10.23 29.07/10.23 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.23 >= 2*X1 + 2*X2 29.07/10.23 = [prod(activate(X1), activate(X2))] 29.07/10.23 29.07/10.23 [activate(n__fact(X))] = 2 + 2*X 29.07/10.23 > 1 + 2*X 29.07/10.23 = [fact(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__p(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [p(activate(X))] 29.07/10.23 29.07/10.23 [p(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__p(X)] 29.07/10.23 29.07/10.23 29.07/10.23 We return to the main proof. 29.07/10.23 29.07/10.23 We are left with following problem, upon which TcT provides the 29.07/10.23 certificate YES(O(1),O(n^1)). 29.07/10.23 29.07/10.23 Strict Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.23 , fact(X) -> n__fact(X) 29.07/10.23 , 0() -> n__0() 29.07/10.23 , s(X) -> n__s(X) 29.07/10.23 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.23 , activate(X) -> X 29.07/10.23 , activate(n__s(X)) -> s(activate(X)) 29.07/10.23 , activate(n__0()) -> 0() 29.07/10.23 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.23 , activate(n__p(X)) -> p(activate(X)) 29.07/10.23 , p(X) -> n__p(X) } 29.07/10.23 Weak Trs: 29.07/10.23 { if(true(), X, Y) -> activate(X) 29.07/10.23 , if(false(), X, Y) -> activate(Y) 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) } 29.07/10.23 Obligation: 29.07/10.23 innermost runtime complexity 29.07/10.23 Answer: 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 We use the processor 'polynomial interpretation' to orient 29.07/10.23 following rules strictly. 29.07/10.23 29.07/10.23 Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) } 29.07/10.23 29.07/10.23 The induced complexity on above rules (modulo remaining rules) is 29.07/10.23 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.23 component(s). 29.07/10.23 29.07/10.23 Sub-proof: 29.07/10.23 ---------- 29.07/10.23 We consider the following typing: 29.07/10.23 29.07/10.23 fact :: b -> b 29.07/10.23 if :: (a,b,b) -> b 29.07/10.23 zero :: b -> a 29.07/10.23 n__s :: b -> b 29.07/10.23 n__0 :: b 29.07/10.23 n__prod :: (b,b) -> b 29.07/10.23 n__fact :: b -> b 29.07/10.23 n__p :: b -> b 29.07/10.23 0 :: b 29.07/10.23 s :: b -> b 29.07/10.23 prod :: (b,b) -> b 29.07/10.23 true :: a 29.07/10.23 activate :: b -> b 29.07/10.23 false :: a 29.07/10.23 p :: b -> b 29.07/10.23 29.07/10.23 The following argument positions are considered usable: 29.07/10.23 29.07/10.23 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.23 Uargs(p) = {1} 29.07/10.23 29.07/10.23 TcT has computed the following constructor-restricted 29.07/10.23 typedpolynomial interpretation. 29.07/10.23 29.07/10.23 [fact](x1) = 1 + x1 29.07/10.23 29.07/10.23 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 29.07/10.23 29.07/10.23 [zero](x1) = 0 29.07/10.23 29.07/10.23 [n__s](x1) = x1 29.07/10.23 29.07/10.23 [n__0]() = 0 29.07/10.23 29.07/10.23 [n__prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [n__fact](x1) = 1 + x1 29.07/10.23 29.07/10.23 [n__p](x1) = x1 29.07/10.23 29.07/10.23 [0]() = 0 29.07/10.23 29.07/10.23 [s](x1) = x1 29.07/10.23 29.07/10.23 [prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [true]() = 0 29.07/10.23 29.07/10.23 [activate](x1) = 2*x1 29.07/10.23 29.07/10.23 [false]() = 1 29.07/10.23 29.07/10.23 [p](x1) = x1 29.07/10.23 29.07/10.23 29.07/10.23 This order satisfies the following ordering constraints. 29.07/10.23 29.07/10.23 [fact(X)] = 1 + X 29.07/10.23 > 29.07/10.23 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.23 29.07/10.23 [fact(X)] = 1 + X 29.07/10.23 >= 1 + X 29.07/10.23 = [n__fact(X)] 29.07/10.23 29.07/10.23 [if(true(), X, Y)] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [activate(X)] 29.07/10.23 29.07/10.23 [if(false(), X, Y)] = 2*Y + 2*X 29.07/10.23 >= 2*Y 29.07/10.23 = [activate(Y)] 29.07/10.23 29.07/10.23 [0()] = 29.07/10.23 >= 29.07/10.23 = [n__0()] 29.07/10.23 29.07/10.23 [s(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__s(X)] 29.07/10.23 29.07/10.23 [prod(X1, X2)] = X1 + X2 29.07/10.23 >= X1 + X2 29.07/10.23 = [n__prod(X1, X2)] 29.07/10.23 29.07/10.23 [activate(X)] = 2*X 29.07/10.23 >= X 29.07/10.23 = [X] 29.07/10.23 29.07/10.23 [activate(n__s(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [s(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__0())] = 29.07/10.23 >= 29.07/10.23 = [0()] 29.07/10.23 29.07/10.23 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.23 >= 2*X1 + 2*X2 29.07/10.23 = [prod(activate(X1), activate(X2))] 29.07/10.23 29.07/10.23 [activate(n__fact(X))] = 2 + 2*X 29.07/10.23 > 1 + 2*X 29.07/10.23 = [fact(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__p(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [p(activate(X))] 29.07/10.23 29.07/10.23 [p(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__p(X)] 29.07/10.23 29.07/10.23 29.07/10.23 We return to the main proof. 29.07/10.23 29.07/10.23 We are left with following problem, upon which TcT provides the 29.07/10.23 certificate YES(O(1),O(n^1)). 29.07/10.23 29.07/10.23 Strict Trs: 29.07/10.23 { fact(X) -> n__fact(X) 29.07/10.23 , 0() -> n__0() 29.07/10.23 , s(X) -> n__s(X) 29.07/10.23 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.23 , activate(X) -> X 29.07/10.23 , activate(n__s(X)) -> s(activate(X)) 29.07/10.23 , activate(n__0()) -> 0() 29.07/10.23 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.23 , activate(n__p(X)) -> p(activate(X)) 29.07/10.23 , p(X) -> n__p(X) } 29.07/10.23 Weak Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.23 , if(true(), X, Y) -> activate(X) 29.07/10.23 , if(false(), X, Y) -> activate(Y) 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) } 29.07/10.23 Obligation: 29.07/10.23 innermost runtime complexity 29.07/10.23 Answer: 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 We use the processor 'polynomial interpretation' to orient 29.07/10.23 following rules strictly. 29.07/10.23 29.07/10.23 Trs: 29.07/10.23 { fact(X) -> n__fact(X) 29.07/10.23 , 0() -> n__0() } 29.07/10.23 29.07/10.23 The induced complexity on above rules (modulo remaining rules) is 29.07/10.23 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.23 component(s). 29.07/10.23 29.07/10.23 Sub-proof: 29.07/10.23 ---------- 29.07/10.23 We consider the following typing: 29.07/10.23 29.07/10.23 fact :: b -> b 29.07/10.23 if :: (a,b,b) -> b 29.07/10.23 zero :: b -> a 29.07/10.23 n__s :: b -> b 29.07/10.23 n__0 :: b 29.07/10.23 n__prod :: (b,b) -> b 29.07/10.23 n__fact :: b -> b 29.07/10.23 n__p :: b -> b 29.07/10.23 0 :: b 29.07/10.23 s :: b -> b 29.07/10.23 prod :: (b,b) -> b 29.07/10.23 true :: a 29.07/10.23 activate :: b -> b 29.07/10.23 false :: a 29.07/10.23 p :: b -> b 29.07/10.23 29.07/10.23 The following argument positions are considered usable: 29.07/10.23 29.07/10.23 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.23 Uargs(p) = {1} 29.07/10.23 29.07/10.23 TcT has computed the following constructor-restricted 29.07/10.23 typedpolynomial interpretation. 29.07/10.23 29.07/10.23 [fact](x1) = 2 + x1 29.07/10.23 29.07/10.23 [if](x1, x2, x3) = x1*x3 + 2*x2 29.07/10.23 29.07/10.23 [zero](x1) = 0 29.07/10.23 29.07/10.23 [n__s](x1) = x1 29.07/10.23 29.07/10.23 [n__0]() = 1 29.07/10.23 29.07/10.23 [n__prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [n__fact](x1) = 1 + x1 29.07/10.23 29.07/10.23 [n__p](x1) = x1 29.07/10.23 29.07/10.23 [0]() = 2 29.07/10.23 29.07/10.23 [s](x1) = x1 29.07/10.23 29.07/10.23 [prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [true]() = 0 29.07/10.23 29.07/10.23 [activate](x1) = 2*x1 29.07/10.23 29.07/10.23 [false]() = 2 29.07/10.23 29.07/10.23 [p](x1) = x1 29.07/10.23 29.07/10.23 29.07/10.23 This order satisfies the following ordering constraints. 29.07/10.23 29.07/10.23 [fact(X)] = 2 + X 29.07/10.23 >= 2 29.07/10.23 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.23 29.07/10.23 [fact(X)] = 2 + X 29.07/10.23 > 1 + X 29.07/10.23 = [n__fact(X)] 29.07/10.23 29.07/10.23 [if(true(), X, Y)] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [activate(X)] 29.07/10.23 29.07/10.23 [if(false(), X, Y)] = 2*Y + 2*X 29.07/10.23 >= 2*Y 29.07/10.23 = [activate(Y)] 29.07/10.23 29.07/10.23 [0()] = 2 29.07/10.23 > 1 29.07/10.23 = [n__0()] 29.07/10.23 29.07/10.23 [s(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__s(X)] 29.07/10.23 29.07/10.23 [prod(X1, X2)] = X1 + X2 29.07/10.23 >= X1 + X2 29.07/10.23 = [n__prod(X1, X2)] 29.07/10.23 29.07/10.23 [activate(X)] = 2*X 29.07/10.23 >= X 29.07/10.23 = [X] 29.07/10.23 29.07/10.23 [activate(n__s(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [s(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__0())] = 2 29.07/10.23 >= 2 29.07/10.23 = [0()] 29.07/10.23 29.07/10.23 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.23 >= 2*X1 + 2*X2 29.07/10.23 = [prod(activate(X1), activate(X2))] 29.07/10.23 29.07/10.23 [activate(n__fact(X))] = 2 + 2*X 29.07/10.23 >= 2 + 2*X 29.07/10.23 = [fact(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__p(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [p(activate(X))] 29.07/10.23 29.07/10.23 [p(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__p(X)] 29.07/10.23 29.07/10.23 29.07/10.23 We return to the main proof. 29.07/10.23 29.07/10.23 We are left with following problem, upon which TcT provides the 29.07/10.23 certificate YES(O(1),O(n^1)). 29.07/10.23 29.07/10.23 Strict Trs: 29.07/10.23 { s(X) -> n__s(X) 29.07/10.23 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.23 , activate(X) -> X 29.07/10.23 , activate(n__s(X)) -> s(activate(X)) 29.07/10.23 , activate(n__0()) -> 0() 29.07/10.23 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.23 , activate(n__p(X)) -> p(activate(X)) 29.07/10.23 , p(X) -> n__p(X) } 29.07/10.23 Weak Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.23 , fact(X) -> n__fact(X) 29.07/10.23 , if(true(), X, Y) -> activate(X) 29.07/10.23 , if(false(), X, Y) -> activate(Y) 29.07/10.23 , 0() -> n__0() 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) } 29.07/10.23 Obligation: 29.07/10.23 innermost runtime complexity 29.07/10.23 Answer: 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 We use the processor 'polynomial interpretation' to orient 29.07/10.23 following rules strictly. 29.07/10.23 29.07/10.23 Trs: { activate(n__p(X)) -> p(activate(X)) } 29.07/10.23 29.07/10.23 The induced complexity on above rules (modulo remaining rules) is 29.07/10.23 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.23 component(s). 29.07/10.23 29.07/10.23 Sub-proof: 29.07/10.23 ---------- 29.07/10.23 We consider the following typing: 29.07/10.23 29.07/10.23 fact :: b -> b 29.07/10.23 if :: (a,b,b) -> b 29.07/10.23 zero :: b -> a 29.07/10.23 n__s :: b -> b 29.07/10.23 n__0 :: b 29.07/10.23 n__prod :: (b,b) -> b 29.07/10.23 n__fact :: b -> b 29.07/10.23 n__p :: b -> b 29.07/10.23 0 :: b 29.07/10.23 s :: b -> b 29.07/10.23 prod :: (b,b) -> b 29.07/10.23 true :: a 29.07/10.23 activate :: b -> b 29.07/10.23 false :: a 29.07/10.23 p :: b -> b 29.07/10.23 29.07/10.23 The following argument positions are considered usable: 29.07/10.23 29.07/10.23 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.23 Uargs(p) = {1} 29.07/10.23 29.07/10.23 TcT has computed the following constructor-restricted 29.07/10.23 typedpolynomial interpretation. 29.07/10.23 29.07/10.23 [fact](x1) = x1 29.07/10.23 29.07/10.23 [if](x1, x2, x3) = x1*x3 + 2*x2 29.07/10.23 29.07/10.23 [zero](x1) = 0 29.07/10.23 29.07/10.23 [n__s](x1) = x1 29.07/10.23 29.07/10.23 [n__0]() = 0 29.07/10.23 29.07/10.23 [n__prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [n__fact](x1) = x1 29.07/10.23 29.07/10.23 [n__p](x1) = 1 + x1 29.07/10.23 29.07/10.23 [0]() = 0 29.07/10.23 29.07/10.23 [s](x1) = x1 29.07/10.23 29.07/10.23 [prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [true]() = 0 29.07/10.23 29.07/10.23 [activate](x1) = 2*x1 29.07/10.23 29.07/10.23 [false]() = 2 29.07/10.23 29.07/10.23 [p](x1) = 1 + x1 29.07/10.23 29.07/10.23 29.07/10.23 This order satisfies the following ordering constraints. 29.07/10.23 29.07/10.23 [fact(X)] = X 29.07/10.23 >= 29.07/10.23 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.23 29.07/10.23 [fact(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__fact(X)] 29.07/10.23 29.07/10.23 [if(true(), X, Y)] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [activate(X)] 29.07/10.23 29.07/10.23 [if(false(), X, Y)] = 2*Y + 2*X 29.07/10.23 >= 2*Y 29.07/10.23 = [activate(Y)] 29.07/10.23 29.07/10.23 [0()] = 29.07/10.23 >= 29.07/10.23 = [n__0()] 29.07/10.23 29.07/10.23 [s(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__s(X)] 29.07/10.23 29.07/10.23 [prod(X1, X2)] = X1 + X2 29.07/10.23 >= X1 + X2 29.07/10.23 = [n__prod(X1, X2)] 29.07/10.23 29.07/10.23 [activate(X)] = 2*X 29.07/10.23 >= X 29.07/10.23 = [X] 29.07/10.23 29.07/10.23 [activate(n__s(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [s(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__0())] = 29.07/10.23 >= 29.07/10.23 = [0()] 29.07/10.23 29.07/10.23 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.23 >= 2*X1 + 2*X2 29.07/10.23 = [prod(activate(X1), activate(X2))] 29.07/10.23 29.07/10.23 [activate(n__fact(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [fact(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__p(X))] = 2 + 2*X 29.07/10.23 > 1 + 2*X 29.07/10.23 = [p(activate(X))] 29.07/10.23 29.07/10.23 [p(X)] = 1 + X 29.07/10.23 >= 1 + X 29.07/10.23 = [n__p(X)] 29.07/10.23 29.07/10.23 29.07/10.23 We return to the main proof. 29.07/10.23 29.07/10.23 We are left with following problem, upon which TcT provides the 29.07/10.23 certificate YES(O(1),O(n^1)). 29.07/10.23 29.07/10.23 Strict Trs: 29.07/10.23 { s(X) -> n__s(X) 29.07/10.23 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.23 , activate(X) -> X 29.07/10.23 , activate(n__s(X)) -> s(activate(X)) 29.07/10.23 , activate(n__0()) -> 0() 29.07/10.23 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.23 , p(X) -> n__p(X) } 29.07/10.23 Weak Trs: 29.07/10.23 { fact(X) -> 29.07/10.23 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.23 , fact(X) -> n__fact(X) 29.07/10.23 , if(true(), X, Y) -> activate(X) 29.07/10.23 , if(false(), X, Y) -> activate(Y) 29.07/10.23 , 0() -> n__0() 29.07/10.23 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.23 , activate(n__p(X)) -> p(activate(X)) } 29.07/10.23 Obligation: 29.07/10.23 innermost runtime complexity 29.07/10.23 Answer: 29.07/10.23 YES(O(1),O(n^1)) 29.07/10.23 29.07/10.23 We use the processor 'polynomial interpretation' to orient 29.07/10.23 following rules strictly. 29.07/10.23 29.07/10.23 Trs: { activate(n__0()) -> 0() } 29.07/10.23 29.07/10.23 The induced complexity on above rules (modulo remaining rules) is 29.07/10.23 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.23 component(s). 29.07/10.23 29.07/10.23 Sub-proof: 29.07/10.23 ---------- 29.07/10.23 We consider the following typing: 29.07/10.23 29.07/10.23 fact :: b -> b 29.07/10.23 if :: (a,b,b) -> b 29.07/10.23 zero :: b -> a 29.07/10.23 n__s :: b -> b 29.07/10.23 n__0 :: b 29.07/10.23 n__prod :: (b,b) -> b 29.07/10.23 n__fact :: b -> b 29.07/10.23 n__p :: b -> b 29.07/10.23 0 :: b 29.07/10.23 s :: b -> b 29.07/10.23 prod :: (b,b) -> b 29.07/10.23 true :: a 29.07/10.23 activate :: b -> b 29.07/10.23 false :: a 29.07/10.23 p :: b -> b 29.07/10.23 29.07/10.23 The following argument positions are considered usable: 29.07/10.23 29.07/10.23 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.23 Uargs(p) = {1} 29.07/10.23 29.07/10.23 TcT has computed the following constructor-restricted 29.07/10.23 typedpolynomial interpretation. 29.07/10.23 29.07/10.23 [fact](x1) = 2 + x1 29.07/10.23 29.07/10.23 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 29.07/10.23 29.07/10.23 [zero](x1) = 0 29.07/10.23 29.07/10.23 [n__s](x1) = x1 29.07/10.23 29.07/10.23 [n__0]() = 1 29.07/10.23 29.07/10.23 [n__prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [n__fact](x1) = 1 + x1 29.07/10.23 29.07/10.23 [n__p](x1) = x1 29.07/10.23 29.07/10.23 [0]() = 1 29.07/10.23 29.07/10.23 [s](x1) = x1 29.07/10.23 29.07/10.23 [prod](x1, x2) = x1 + x2 29.07/10.23 29.07/10.23 [true]() = 0 29.07/10.23 29.07/10.23 [activate](x1) = 2*x1 29.07/10.23 29.07/10.23 [false]() = 2 29.07/10.23 29.07/10.23 [p](x1) = x1 29.07/10.23 29.07/10.23 29.07/10.23 This order satisfies the following ordering constraints. 29.07/10.23 29.07/10.23 [fact(X)] = 2 + X 29.07/10.23 >= 2 29.07/10.23 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.23 29.07/10.23 [fact(X)] = 2 + X 29.07/10.23 > 1 + X 29.07/10.23 = [n__fact(X)] 29.07/10.23 29.07/10.23 [if(true(), X, Y)] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [activate(X)] 29.07/10.23 29.07/10.23 [if(false(), X, Y)] = 4*Y + 2*X 29.07/10.23 >= 2*Y 29.07/10.23 = [activate(Y)] 29.07/10.23 29.07/10.23 [0()] = 1 29.07/10.23 >= 1 29.07/10.23 = [n__0()] 29.07/10.23 29.07/10.23 [s(X)] = X 29.07/10.23 >= X 29.07/10.23 = [n__s(X)] 29.07/10.23 29.07/10.23 [prod(X1, X2)] = X1 + X2 29.07/10.23 >= X1 + X2 29.07/10.23 = [n__prod(X1, X2)] 29.07/10.23 29.07/10.23 [activate(X)] = 2*X 29.07/10.23 >= X 29.07/10.23 = [X] 29.07/10.23 29.07/10.23 [activate(n__s(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.23 = [s(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__0())] = 2 29.07/10.23 > 1 29.07/10.23 = [0()] 29.07/10.23 29.07/10.23 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.23 >= 2*X1 + 2*X2 29.07/10.23 = [prod(activate(X1), activate(X2))] 29.07/10.23 29.07/10.23 [activate(n__fact(X))] = 2 + 2*X 29.07/10.23 >= 2 + 2*X 29.07/10.23 = [fact(activate(X))] 29.07/10.23 29.07/10.23 [activate(n__p(X))] = 2*X 29.07/10.23 >= 2*X 29.07/10.24 = [p(activate(X))] 29.07/10.24 29.07/10.24 [p(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__p(X)] 29.07/10.24 29.07/10.24 29.07/10.24 We return to the main proof. 29.07/10.24 29.07/10.24 We are left with following problem, upon which TcT provides the 29.07/10.24 certificate YES(O(1),O(n^1)). 29.07/10.24 29.07/10.24 Strict Trs: 29.07/10.24 { s(X) -> n__s(X) 29.07/10.24 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.24 , activate(X) -> X 29.07/10.24 , activate(n__s(X)) -> s(activate(X)) 29.07/10.24 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.24 , p(X) -> n__p(X) } 29.07/10.24 Weak Trs: 29.07/10.24 { fact(X) -> 29.07/10.24 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.24 , fact(X) -> n__fact(X) 29.07/10.24 , if(true(), X, Y) -> activate(X) 29.07/10.24 , if(false(), X, Y) -> activate(Y) 29.07/10.24 , 0() -> n__0() 29.07/10.24 , activate(n__0()) -> 0() 29.07/10.24 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.24 , activate(n__p(X)) -> p(activate(X)) } 29.07/10.24 Obligation: 29.07/10.24 innermost runtime complexity 29.07/10.24 Answer: 29.07/10.24 YES(O(1),O(n^1)) 29.07/10.24 29.07/10.24 We use the processor 'polynomial interpretation' to orient 29.07/10.24 following rules strictly. 29.07/10.24 29.07/10.24 Trs: { p(X) -> n__p(X) } 29.07/10.24 29.07/10.24 The induced complexity on above rules (modulo remaining rules) is 29.07/10.24 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.24 component(s). 29.07/10.24 29.07/10.24 Sub-proof: 29.07/10.24 ---------- 29.07/10.24 We consider the following typing: 29.07/10.24 29.07/10.24 fact :: b -> b 29.07/10.24 if :: (a,b,b) -> b 29.07/10.24 zero :: b -> a 29.07/10.24 n__s :: b -> b 29.07/10.24 n__0 :: b 29.07/10.24 n__prod :: (b,b) -> b 29.07/10.24 n__fact :: b -> b 29.07/10.24 n__p :: b -> b 29.07/10.24 0 :: b 29.07/10.24 s :: b -> b 29.07/10.24 prod :: (b,b) -> b 29.07/10.24 true :: a 29.07/10.24 activate :: b -> b 29.07/10.24 false :: a 29.07/10.24 p :: b -> b 29.07/10.24 29.07/10.24 The following argument positions are considered usable: 29.07/10.24 29.07/10.24 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.24 Uargs(p) = {1} 29.07/10.24 29.07/10.24 TcT has computed the following constructor-restricted 29.07/10.24 typedpolynomial interpretation. 29.07/10.24 29.07/10.24 [fact](x1) = x1 29.07/10.24 29.07/10.24 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 29.07/10.24 29.07/10.24 [zero](x1) = 0 29.07/10.24 29.07/10.24 [n__s](x1) = x1 29.07/10.24 29.07/10.24 [n__0]() = 0 29.07/10.24 29.07/10.24 [n__prod](x1, x2) = x1 + x2 29.07/10.24 29.07/10.24 [n__fact](x1) = x1 29.07/10.24 29.07/10.24 [n__p](x1) = 2 + x1 29.07/10.24 29.07/10.24 [0]() = 0 29.07/10.24 29.07/10.24 [s](x1) = x1 29.07/10.24 29.07/10.24 [prod](x1, x2) = x1 + x2 29.07/10.24 29.07/10.24 [true]() = 0 29.07/10.24 29.07/10.24 [activate](x1) = 2*x1 29.07/10.24 29.07/10.24 [false]() = 2 29.07/10.24 29.07/10.24 [p](x1) = 3 + x1 29.07/10.24 29.07/10.24 29.07/10.24 This order satisfies the following ordering constraints. 29.07/10.24 29.07/10.24 [fact(X)] = X 29.07/10.24 >= 29.07/10.24 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.24 29.07/10.24 [fact(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__fact(X)] 29.07/10.24 29.07/10.24 [if(true(), X, Y)] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [activate(X)] 29.07/10.24 29.07/10.24 [if(false(), X, Y)] = 4*Y + 2*X 29.07/10.24 >= 2*Y 29.07/10.24 = [activate(Y)] 29.07/10.24 29.07/10.24 [0()] = 29.07/10.24 >= 29.07/10.24 = [n__0()] 29.07/10.24 29.07/10.24 [s(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__s(X)] 29.07/10.24 29.07/10.24 [prod(X1, X2)] = X1 + X2 29.07/10.24 >= X1 + X2 29.07/10.24 = [n__prod(X1, X2)] 29.07/10.24 29.07/10.24 [activate(X)] = 2*X 29.07/10.24 >= X 29.07/10.24 = [X] 29.07/10.24 29.07/10.24 [activate(n__s(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [s(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__0())] = 29.07/10.24 >= 29.07/10.24 = [0()] 29.07/10.24 29.07/10.24 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.24 >= 2*X1 + 2*X2 29.07/10.24 = [prod(activate(X1), activate(X2))] 29.07/10.24 29.07/10.24 [activate(n__fact(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [fact(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__p(X))] = 4 + 2*X 29.07/10.24 > 3 + 2*X 29.07/10.24 = [p(activate(X))] 29.07/10.24 29.07/10.24 [p(X)] = 3 + X 29.07/10.24 > 2 + X 29.07/10.24 = [n__p(X)] 29.07/10.24 29.07/10.24 29.07/10.24 We return to the main proof. 29.07/10.24 29.07/10.24 We are left with following problem, upon which TcT provides the 29.07/10.24 certificate YES(O(1),O(n^1)). 29.07/10.24 29.07/10.24 Strict Trs: 29.07/10.24 { s(X) -> n__s(X) 29.07/10.24 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.24 , activate(X) -> X 29.07/10.24 , activate(n__s(X)) -> s(activate(X)) 29.07/10.24 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) } 29.07/10.24 Weak Trs: 29.07/10.24 { fact(X) -> 29.07/10.24 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.24 , fact(X) -> n__fact(X) 29.07/10.24 , if(true(), X, Y) -> activate(X) 29.07/10.24 , if(false(), X, Y) -> activate(Y) 29.07/10.24 , 0() -> n__0() 29.07/10.24 , activate(n__0()) -> 0() 29.07/10.24 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.24 , activate(n__p(X)) -> p(activate(X)) 29.07/10.24 , p(X) -> n__p(X) } 29.07/10.24 Obligation: 29.07/10.24 innermost runtime complexity 29.07/10.24 Answer: 29.07/10.24 YES(O(1),O(n^1)) 29.07/10.24 29.07/10.24 We use the processor 'polynomial interpretation' to orient 29.07/10.24 following rules strictly. 29.07/10.24 29.07/10.24 Trs: { s(X) -> n__s(X) } 29.07/10.24 29.07/10.24 The induced complexity on above rules (modulo remaining rules) is 29.07/10.24 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.24 component(s). 29.07/10.24 29.07/10.24 Sub-proof: 29.07/10.24 ---------- 29.07/10.24 We consider the following typing: 29.07/10.24 29.07/10.24 fact :: b -> b 29.07/10.24 if :: (a,b,b) -> b 29.07/10.24 zero :: b -> a 29.07/10.24 n__s :: b -> b 29.07/10.24 n__0 :: b 29.07/10.24 n__prod :: (b,b) -> b 29.07/10.24 n__fact :: b -> b 29.07/10.24 n__p :: b -> b 29.07/10.24 0 :: b 29.07/10.24 s :: b -> b 29.07/10.24 prod :: (b,b) -> b 29.07/10.24 true :: a 29.07/10.24 activate :: b -> b 29.07/10.24 false :: a 29.07/10.24 p :: b -> b 29.07/10.24 29.07/10.24 The following argument positions are considered usable: 29.07/10.24 29.07/10.24 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.24 Uargs(p) = {1} 29.07/10.24 29.07/10.24 TcT has computed the following constructor-restricted 29.07/10.24 typedpolynomial interpretation. 29.07/10.24 29.07/10.24 [fact](x1) = 2 + x1 29.07/10.24 29.07/10.24 [if](x1, x2, x3) = x1*x3 + 2*x2 29.07/10.24 29.07/10.24 [zero](x1) = 0 29.07/10.24 29.07/10.24 [n__s](x1) = 1 + x1 29.07/10.24 29.07/10.24 [n__0]() = 0 29.07/10.24 29.07/10.24 [n__prod](x1, x2) = x1 + x2 29.07/10.24 29.07/10.24 [n__fact](x1) = 1 + x1 29.07/10.24 29.07/10.24 [n__p](x1) = x1 29.07/10.24 29.07/10.24 [0]() = 0 29.07/10.24 29.07/10.24 [s](x1) = 2 + x1 29.07/10.24 29.07/10.24 [prod](x1, x2) = x1 + x2 29.07/10.24 29.07/10.24 [true]() = 0 29.07/10.24 29.07/10.24 [activate](x1) = 2*x1 29.07/10.24 29.07/10.24 [false]() = 2 29.07/10.24 29.07/10.24 [p](x1) = x1 29.07/10.24 29.07/10.24 29.07/10.24 This order satisfies the following ordering constraints. 29.07/10.24 29.07/10.24 [fact(X)] = 2 + X 29.07/10.24 >= 2 29.07/10.24 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.24 29.07/10.24 [fact(X)] = 2 + X 29.07/10.24 > 1 + X 29.07/10.24 = [n__fact(X)] 29.07/10.24 29.07/10.24 [if(true(), X, Y)] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [activate(X)] 29.07/10.24 29.07/10.24 [if(false(), X, Y)] = 2*Y + 2*X 29.07/10.24 >= 2*Y 29.07/10.24 = [activate(Y)] 29.07/10.24 29.07/10.24 [0()] = 29.07/10.24 >= 29.07/10.24 = [n__0()] 29.07/10.24 29.07/10.24 [s(X)] = 2 + X 29.07/10.24 > 1 + X 29.07/10.24 = [n__s(X)] 29.07/10.24 29.07/10.24 [prod(X1, X2)] = X1 + X2 29.07/10.24 >= X1 + X2 29.07/10.24 = [n__prod(X1, X2)] 29.07/10.24 29.07/10.24 [activate(X)] = 2*X 29.07/10.24 >= X 29.07/10.24 = [X] 29.07/10.24 29.07/10.24 [activate(n__s(X))] = 2 + 2*X 29.07/10.24 >= 2 + 2*X 29.07/10.24 = [s(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__0())] = 29.07/10.24 >= 29.07/10.24 = [0()] 29.07/10.24 29.07/10.24 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.24 >= 2*X1 + 2*X2 29.07/10.24 = [prod(activate(X1), activate(X2))] 29.07/10.24 29.07/10.24 [activate(n__fact(X))] = 2 + 2*X 29.07/10.24 >= 2 + 2*X 29.07/10.24 = [fact(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__p(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [p(activate(X))] 29.07/10.24 29.07/10.24 [p(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__p(X)] 29.07/10.24 29.07/10.24 29.07/10.24 We return to the main proof. 29.07/10.24 29.07/10.24 We are left with following problem, upon which TcT provides the 29.07/10.24 certificate YES(O(1),O(n^1)). 29.07/10.24 29.07/10.24 Strict Trs: 29.07/10.24 { prod(X1, X2) -> n__prod(X1, X2) 29.07/10.24 , activate(X) -> X 29.07/10.24 , activate(n__s(X)) -> s(activate(X)) 29.07/10.24 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) } 29.07/10.24 Weak Trs: 29.07/10.24 { fact(X) -> 29.07/10.24 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.24 , fact(X) -> n__fact(X) 29.07/10.24 , if(true(), X, Y) -> activate(X) 29.07/10.24 , if(false(), X, Y) -> activate(Y) 29.07/10.24 , 0() -> n__0() 29.07/10.24 , s(X) -> n__s(X) 29.07/10.24 , activate(n__0()) -> 0() 29.07/10.24 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.24 , activate(n__p(X)) -> p(activate(X)) 29.07/10.24 , p(X) -> n__p(X) } 29.07/10.24 Obligation: 29.07/10.24 innermost runtime complexity 29.07/10.24 Answer: 29.07/10.24 YES(O(1),O(n^1)) 29.07/10.24 29.07/10.24 We use the processor 'polynomial interpretation' to orient 29.07/10.24 following rules strictly. 29.07/10.24 29.07/10.24 Trs: { activate(n__s(X)) -> s(activate(X)) } 29.07/10.24 29.07/10.24 The induced complexity on above rules (modulo remaining rules) is 29.07/10.24 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.24 component(s). 29.07/10.24 29.07/10.24 Sub-proof: 29.07/10.24 ---------- 29.07/10.24 We consider the following typing: 29.07/10.24 29.07/10.24 fact :: b -> b 29.07/10.24 if :: (a,b,b) -> b 29.07/10.24 zero :: b -> a 29.07/10.24 n__s :: b -> b 29.07/10.24 n__0 :: b 29.07/10.24 n__prod :: (b,b) -> b 29.07/10.24 n__fact :: b -> b 29.07/10.24 n__p :: b -> b 29.07/10.24 0 :: b 29.07/10.24 s :: b -> b 29.07/10.24 prod :: (b,b) -> b 29.07/10.24 true :: a 29.07/10.24 activate :: b -> b 29.07/10.24 false :: a 29.07/10.24 p :: b -> b 29.07/10.24 29.07/10.24 The following argument positions are considered usable: 29.07/10.24 29.07/10.24 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.24 Uargs(p) = {1} 29.07/10.24 29.07/10.24 TcT has computed the following constructor-restricted 29.07/10.24 typedpolynomial interpretation. 29.07/10.24 29.07/10.24 [fact](x1) = 2 + x1 29.07/10.24 29.07/10.24 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 29.07/10.24 29.07/10.24 [zero](x1) = 0 29.07/10.24 29.07/10.24 [n__s](x1) = 1 + x1 29.07/10.24 29.07/10.24 [n__0]() = 0 29.07/10.24 29.07/10.24 [n__prod](x1, x2) = x1 + x2 29.07/10.24 29.07/10.24 [n__fact](x1) = 1 + x1 29.07/10.24 29.07/10.24 [n__p](x1) = x1 29.07/10.24 29.07/10.24 [0]() = 0 29.07/10.24 29.07/10.24 [s](x1) = 1 + x1 29.07/10.24 29.07/10.24 [prod](x1, x2) = x1 + x2 29.07/10.24 29.07/10.24 [true]() = 0 29.07/10.24 29.07/10.24 [activate](x1) = 2*x1 29.07/10.24 29.07/10.24 [false]() = 2 29.07/10.24 29.07/10.24 [p](x1) = x1 29.07/10.24 29.07/10.24 29.07/10.24 This order satisfies the following ordering constraints. 29.07/10.24 29.07/10.24 [fact(X)] = 2 + X 29.07/10.24 >= 2 29.07/10.24 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.24 29.07/10.24 [fact(X)] = 2 + X 29.07/10.24 > 1 + X 29.07/10.24 = [n__fact(X)] 29.07/10.24 29.07/10.24 [if(true(), X, Y)] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [activate(X)] 29.07/10.24 29.07/10.24 [if(false(), X, Y)] = 4*Y + 2*X 29.07/10.24 >= 2*Y 29.07/10.24 = [activate(Y)] 29.07/10.24 29.07/10.24 [0()] = 29.07/10.24 >= 29.07/10.24 = [n__0()] 29.07/10.24 29.07/10.24 [s(X)] = 1 + X 29.07/10.24 >= 1 + X 29.07/10.24 = [n__s(X)] 29.07/10.24 29.07/10.24 [prod(X1, X2)] = X1 + X2 29.07/10.24 >= X1 + X2 29.07/10.24 = [n__prod(X1, X2)] 29.07/10.24 29.07/10.24 [activate(X)] = 2*X 29.07/10.24 >= X 29.07/10.24 = [X] 29.07/10.24 29.07/10.24 [activate(n__s(X))] = 2 + 2*X 29.07/10.24 > 1 + 2*X 29.07/10.24 = [s(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__0())] = 29.07/10.24 >= 29.07/10.24 = [0()] 29.07/10.24 29.07/10.24 [activate(n__prod(X1, X2))] = 2*X1 + 2*X2 29.07/10.24 >= 2*X1 + 2*X2 29.07/10.24 = [prod(activate(X1), activate(X2))] 29.07/10.24 29.07/10.24 [activate(n__fact(X))] = 2 + 2*X 29.07/10.24 >= 2 + 2*X 29.07/10.24 = [fact(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__p(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [p(activate(X))] 29.07/10.24 29.07/10.24 [p(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__p(X)] 29.07/10.24 29.07/10.24 29.07/10.24 We return to the main proof. 29.07/10.24 29.07/10.24 We are left with following problem, upon which TcT provides the 29.07/10.24 certificate YES(O(1),O(n^1)). 29.07/10.24 29.07/10.24 Strict Trs: 29.07/10.24 { prod(X1, X2) -> n__prod(X1, X2) 29.07/10.24 , activate(X) -> X 29.07/10.24 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) } 29.07/10.24 Weak Trs: 29.07/10.24 { fact(X) -> 29.07/10.24 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.24 , fact(X) -> n__fact(X) 29.07/10.24 , if(true(), X, Y) -> activate(X) 29.07/10.24 , if(false(), X, Y) -> activate(Y) 29.07/10.24 , 0() -> n__0() 29.07/10.24 , s(X) -> n__s(X) 29.07/10.24 , activate(n__s(X)) -> s(activate(X)) 29.07/10.24 , activate(n__0()) -> 0() 29.07/10.24 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.24 , activate(n__p(X)) -> p(activate(X)) 29.07/10.24 , p(X) -> n__p(X) } 29.07/10.24 Obligation: 29.07/10.24 innermost runtime complexity 29.07/10.24 Answer: 29.07/10.24 YES(O(1),O(n^1)) 29.07/10.24 29.07/10.24 We use the processor 'polynomial interpretation' to orient 29.07/10.24 following rules strictly. 29.07/10.24 29.07/10.24 Trs: 29.07/10.24 { activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) } 29.07/10.24 29.07/10.24 The induced complexity on above rules (modulo remaining rules) is 29.07/10.24 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.24 component(s). 29.07/10.24 29.07/10.24 Sub-proof: 29.07/10.24 ---------- 29.07/10.24 We consider the following typing: 29.07/10.24 29.07/10.24 fact :: b -> b 29.07/10.24 if :: (a,b,b) -> b 29.07/10.24 zero :: b -> a 29.07/10.24 n__s :: b -> b 29.07/10.24 n__0 :: b 29.07/10.24 n__prod :: (b,b) -> b 29.07/10.24 n__fact :: b -> b 29.07/10.24 n__p :: b -> b 29.07/10.24 0 :: b 29.07/10.24 s :: b -> b 29.07/10.24 prod :: (b,b) -> b 29.07/10.24 true :: a 29.07/10.24 activate :: b -> b 29.07/10.24 false :: a 29.07/10.24 p :: b -> b 29.07/10.24 29.07/10.24 The following argument positions are considered usable: 29.07/10.24 29.07/10.24 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.24 Uargs(p) = {1} 29.07/10.24 29.07/10.24 TcT has computed the following constructor-restricted 29.07/10.24 typedpolynomial interpretation. 29.07/10.24 29.07/10.24 [fact](x1) = x1 29.07/10.24 29.07/10.24 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 29.07/10.24 29.07/10.24 [zero](x1) = 0 29.07/10.24 29.07/10.24 [n__s](x1) = x1 29.07/10.24 29.07/10.24 [n__0]() = 0 29.07/10.24 29.07/10.24 [n__prod](x1, x2) = 1 + x1 + x2 29.07/10.24 29.07/10.24 [n__fact](x1) = x1 29.07/10.24 29.07/10.24 [n__p](x1) = x1 29.07/10.24 29.07/10.24 [0]() = 0 29.07/10.24 29.07/10.24 [s](x1) = x1 29.07/10.24 29.07/10.24 [prod](x1, x2) = 1 + x1 + x2 29.07/10.24 29.07/10.24 [true]() = 0 29.07/10.24 29.07/10.24 [activate](x1) = 2*x1 29.07/10.24 29.07/10.24 [false]() = 1 29.07/10.24 29.07/10.24 [p](x1) = x1 29.07/10.24 29.07/10.24 29.07/10.24 This order satisfies the following ordering constraints. 29.07/10.24 29.07/10.24 [fact(X)] = X 29.07/10.24 >= 29.07/10.24 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.24 29.07/10.24 [fact(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__fact(X)] 29.07/10.24 29.07/10.24 [if(true(), X, Y)] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [activate(X)] 29.07/10.24 29.07/10.24 [if(false(), X, Y)] = 2*Y + 2*X 29.07/10.24 >= 2*Y 29.07/10.24 = [activate(Y)] 29.07/10.24 29.07/10.24 [0()] = 29.07/10.24 >= 29.07/10.24 = [n__0()] 29.07/10.24 29.07/10.24 [s(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__s(X)] 29.07/10.24 29.07/10.24 [prod(X1, X2)] = 1 + X1 + X2 29.07/10.24 >= 1 + X1 + X2 29.07/10.24 = [n__prod(X1, X2)] 29.07/10.24 29.07/10.24 [activate(X)] = 2*X 29.07/10.24 >= X 29.07/10.24 = [X] 29.07/10.24 29.07/10.24 [activate(n__s(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [s(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__0())] = 29.07/10.24 >= 29.07/10.24 = [0()] 29.07/10.24 29.07/10.24 [activate(n__prod(X1, X2))] = 2 + 2*X1 + 2*X2 29.07/10.24 > 1 + 2*X1 + 2*X2 29.07/10.24 = [prod(activate(X1), activate(X2))] 29.07/10.24 29.07/10.24 [activate(n__fact(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [fact(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__p(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [p(activate(X))] 29.07/10.24 29.07/10.24 [p(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__p(X)] 29.07/10.24 29.07/10.24 29.07/10.24 We return to the main proof. 29.07/10.24 29.07/10.24 We are left with following problem, upon which TcT provides the 29.07/10.24 certificate YES(O(1),O(n^1)). 29.07/10.24 29.07/10.24 Strict Trs: 29.07/10.24 { prod(X1, X2) -> n__prod(X1, X2) 29.07/10.24 , activate(X) -> X } 29.07/10.24 Weak Trs: 29.07/10.24 { fact(X) -> 29.07/10.24 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.24 , fact(X) -> n__fact(X) 29.07/10.24 , if(true(), X, Y) -> activate(X) 29.07/10.24 , if(false(), X, Y) -> activate(Y) 29.07/10.24 , 0() -> n__0() 29.07/10.24 , s(X) -> n__s(X) 29.07/10.24 , activate(n__s(X)) -> s(activate(X)) 29.07/10.24 , activate(n__0()) -> 0() 29.07/10.24 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.24 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.24 , activate(n__p(X)) -> p(activate(X)) 29.07/10.24 , p(X) -> n__p(X) } 29.07/10.24 Obligation: 29.07/10.24 innermost runtime complexity 29.07/10.24 Answer: 29.07/10.24 YES(O(1),O(n^1)) 29.07/10.24 29.07/10.24 We use the processor 'polynomial interpretation' to orient 29.07/10.24 following rules strictly. 29.07/10.24 29.07/10.24 Trs: { prod(X1, X2) -> n__prod(X1, X2) } 29.07/10.24 29.07/10.24 The induced complexity on above rules (modulo remaining rules) is 29.07/10.24 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.24 component(s). 29.07/10.24 29.07/10.24 Sub-proof: 29.07/10.24 ---------- 29.07/10.24 We consider the following typing: 29.07/10.24 29.07/10.24 fact :: b -> b 29.07/10.24 if :: (a,b,b) -> b 29.07/10.24 zero :: b -> a 29.07/10.24 n__s :: b -> b 29.07/10.24 n__0 :: b 29.07/10.24 n__prod :: (b,b) -> b 29.07/10.24 n__fact :: b -> b 29.07/10.24 n__p :: b -> b 29.07/10.24 0 :: b 29.07/10.24 s :: b -> b 29.07/10.24 prod :: (b,b) -> b 29.07/10.24 true :: a 29.07/10.24 activate :: b -> b 29.07/10.24 false :: a 29.07/10.24 p :: b -> b 29.07/10.24 29.07/10.24 The following argument positions are considered usable: 29.07/10.24 29.07/10.24 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.24 Uargs(p) = {1} 29.07/10.24 29.07/10.24 TcT has computed the following constructor-restricted 29.07/10.24 typedpolynomial interpretation. 29.07/10.24 29.07/10.24 [fact](x1) = x1 29.07/10.24 29.07/10.24 [if](x1, x2, x3) = 2*x1*x3 + 2*x2 29.07/10.24 29.07/10.24 [zero](x1) = 0 29.07/10.24 29.07/10.24 [n__s](x1) = x1 29.07/10.24 29.07/10.24 [n__0]() = 0 29.07/10.24 29.07/10.24 [n__prod](x1, x2) = 2 + x1 + x2 29.07/10.24 29.07/10.24 [n__fact](x1) = x1 29.07/10.24 29.07/10.24 [n__p](x1) = x1 29.07/10.24 29.07/10.24 [0]() = 0 29.07/10.24 29.07/10.24 [s](x1) = x1 29.07/10.24 29.07/10.24 [prod](x1, x2) = 3 + x1 + x2 29.07/10.24 29.07/10.24 [true]() = 0 29.07/10.24 29.07/10.24 [activate](x1) = 2*x1 29.07/10.24 29.07/10.24 [false]() = 1 29.07/10.24 29.07/10.24 [p](x1) = x1 29.07/10.24 29.07/10.24 29.07/10.24 This order satisfies the following ordering constraints. 29.07/10.24 29.07/10.24 [fact(X)] = X 29.07/10.24 >= 29.07/10.24 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.24 29.07/10.24 [fact(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__fact(X)] 29.07/10.24 29.07/10.24 [if(true(), X, Y)] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [activate(X)] 29.07/10.24 29.07/10.24 [if(false(), X, Y)] = 2*Y + 2*X 29.07/10.24 >= 2*Y 29.07/10.24 = [activate(Y)] 29.07/10.24 29.07/10.24 [0()] = 29.07/10.24 >= 29.07/10.24 = [n__0()] 29.07/10.24 29.07/10.24 [s(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__s(X)] 29.07/10.24 29.07/10.24 [prod(X1, X2)] = 3 + X1 + X2 29.07/10.24 > 2 + X1 + X2 29.07/10.24 = [n__prod(X1, X2)] 29.07/10.24 29.07/10.24 [activate(X)] = 2*X 29.07/10.24 >= X 29.07/10.24 = [X] 29.07/10.24 29.07/10.24 [activate(n__s(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [s(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__0())] = 29.07/10.24 >= 29.07/10.24 = [0()] 29.07/10.24 29.07/10.24 [activate(n__prod(X1, X2))] = 4 + 2*X1 + 2*X2 29.07/10.24 > 3 + 2*X1 + 2*X2 29.07/10.24 = [prod(activate(X1), activate(X2))] 29.07/10.24 29.07/10.24 [activate(n__fact(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [fact(activate(X))] 29.07/10.24 29.07/10.24 [activate(n__p(X))] = 2*X 29.07/10.24 >= 2*X 29.07/10.24 = [p(activate(X))] 29.07/10.24 29.07/10.24 [p(X)] = X 29.07/10.24 >= X 29.07/10.24 = [n__p(X)] 29.07/10.24 29.07/10.24 29.07/10.24 We return to the main proof. 29.07/10.24 29.07/10.24 We are left with following problem, upon which TcT provides the 29.07/10.24 certificate YES(O(1),O(n^1)). 29.07/10.24 29.07/10.24 Strict Trs: { activate(X) -> X } 29.07/10.24 Weak Trs: 29.07/10.24 { fact(X) -> 29.07/10.24 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.24 , fact(X) -> n__fact(X) 29.07/10.24 , if(true(), X, Y) -> activate(X) 29.07/10.24 , if(false(), X, Y) -> activate(Y) 29.07/10.24 , 0() -> n__0() 29.07/10.24 , s(X) -> n__s(X) 29.07/10.24 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.24 , activate(n__s(X)) -> s(activate(X)) 29.07/10.24 , activate(n__0()) -> 0() 29.07/10.24 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.24 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.24 , activate(n__p(X)) -> p(activate(X)) 29.07/10.24 , p(X) -> n__p(X) } 29.07/10.24 Obligation: 29.07/10.24 innermost runtime complexity 29.07/10.24 Answer: 29.07/10.24 YES(O(1),O(n^1)) 29.07/10.24 29.07/10.24 We use the processor 'polynomial interpretation' to orient 29.07/10.24 following rules strictly. 29.07/10.24 29.07/10.24 Trs: { activate(X) -> X } 29.07/10.24 29.07/10.24 The induced complexity on above rules (modulo remaining rules) is 29.07/10.24 YES(?,O(n^1)) . These rules are moved into the corresponding weak 29.07/10.24 component(s). 29.07/10.24 29.07/10.24 Sub-proof: 29.07/10.24 ---------- 29.07/10.24 We consider the following typing: 29.07/10.24 29.07/10.24 fact :: b -> b 29.07/10.24 if :: (a,b,b) -> b 29.07/10.24 zero :: b -> a 29.07/10.24 n__s :: b -> b 29.07/10.24 n__0 :: b 29.07/10.24 n__prod :: (b,b) -> b 29.07/10.24 n__fact :: b -> b 29.07/10.24 n__p :: b -> b 29.07/10.24 0 :: b 29.07/10.24 s :: b -> b 29.07/10.24 prod :: (b,b) -> b 29.07/10.24 true :: a 29.07/10.24 activate :: b -> b 29.07/10.24 false :: a 29.07/10.24 p :: b -> b 29.07/10.24 29.07/10.24 The following argument positions are considered usable: 29.07/10.24 29.07/10.24 Uargs(fact) = {1}, Uargs(s) = {1}, Uargs(prod) = {1, 2}, 29.07/10.24 Uargs(p) = {1} 29.07/10.24 29.07/10.24 TcT has computed the following constructor-restricted 29.07/10.24 typedpolynomial interpretation. 29.07/10.24 29.07/10.24 [fact](x1) = 3 + x1 29.07/10.24 29.07/10.24 [if](x1, x2, x3) = 1 + 2*x1*x3 + 2*x2 29.07/10.24 29.07/10.24 [zero](x1) = 0 29.07/10.24 29.07/10.24 [n__s](x1) = x1 29.07/10.24 29.07/10.24 [n__0]() = 0 29.07/10.24 29.07/10.24 [n__prod](x1, x2) = 1 + x1 + x2 29.07/10.24 29.07/10.24 [n__fact](x1) = 2 + x1 29.07/10.24 29.07/10.24 [n__p](x1) = x1 29.07/10.24 29.07/10.24 [0]() = 1 29.07/10.24 29.07/10.24 [s](x1) = x1 29.07/10.24 29.07/10.24 [prod](x1, x2) = 1 + x1 + x2 29.07/10.24 29.07/10.24 [true]() = 0 29.07/10.24 29.07/10.24 [activate](x1) = 1 + 2*x1 29.07/10.24 29.07/10.24 [false]() = 2 29.07/10.24 29.07/10.24 [p](x1) = x1 29.07/10.24 29.07/10.24 29.07/10.24 This order satisfies the following ordering constraints. 29.07/10.24 29.07/10.24 [fact(X)] = 3 + X 29.07/10.24 > 1 29.07/10.24 = [if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))] 29.07/10.24 29.07/10.25 [fact(X)] = 3 + X 29.07/10.25 > 2 + X 29.07/10.25 = [n__fact(X)] 29.07/10.25 29.07/10.25 [if(true(), X, Y)] = 1 + 2*X 29.07/10.25 >= 1 + 2*X 29.07/10.25 = [activate(X)] 29.07/10.25 29.07/10.25 [if(false(), X, Y)] = 1 + 4*Y + 2*X 29.07/10.25 >= 1 + 2*Y 29.07/10.25 = [activate(Y)] 29.07/10.25 29.07/10.25 [0()] = 1 29.07/10.25 > 29.07/10.25 = [n__0()] 29.07/10.25 29.07/10.25 [s(X)] = X 29.07/10.25 >= X 29.07/10.25 = [n__s(X)] 29.07/10.25 29.07/10.25 [prod(X1, X2)] = 1 + X1 + X2 29.07/10.25 >= 1 + X1 + X2 29.07/10.25 = [n__prod(X1, X2)] 29.07/10.25 29.07/10.25 [activate(X)] = 1 + 2*X 29.07/10.25 > X 29.07/10.25 = [X] 29.07/10.25 29.07/10.25 [activate(n__s(X))] = 1 + 2*X 29.07/10.25 >= 1 + 2*X 29.07/10.25 = [s(activate(X))] 29.07/10.25 29.07/10.25 [activate(n__0())] = 1 29.07/10.25 >= 1 29.07/10.25 = [0()] 29.07/10.25 29.07/10.25 [activate(n__prod(X1, X2))] = 3 + 2*X1 + 2*X2 29.07/10.25 >= 3 + 2*X1 + 2*X2 29.07/10.25 = [prod(activate(X1), activate(X2))] 29.07/10.25 29.07/10.25 [activate(n__fact(X))] = 5 + 2*X 29.07/10.25 > 4 + 2*X 29.07/10.25 = [fact(activate(X))] 29.07/10.25 29.07/10.25 [activate(n__p(X))] = 1 + 2*X 29.07/10.25 >= 1 + 2*X 29.07/10.25 = [p(activate(X))] 29.07/10.25 29.07/10.25 [p(X)] = X 29.07/10.25 >= X 29.07/10.25 = [n__p(X)] 29.07/10.25 29.07/10.25 29.07/10.25 We return to the main proof. 29.07/10.25 29.07/10.25 We are left with following problem, upon which TcT provides the 29.07/10.25 certificate YES(O(1),O(1)). 29.07/10.25 29.07/10.25 Weak Trs: 29.07/10.25 { fact(X) -> 29.07/10.25 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 29.07/10.25 , fact(X) -> n__fact(X) 29.07/10.25 , if(true(), X, Y) -> activate(X) 29.07/10.25 , if(false(), X, Y) -> activate(Y) 29.07/10.25 , 0() -> n__0() 29.07/10.25 , s(X) -> n__s(X) 29.07/10.25 , prod(X1, X2) -> n__prod(X1, X2) 29.07/10.25 , activate(X) -> X 29.07/10.25 , activate(n__s(X)) -> s(activate(X)) 29.07/10.25 , activate(n__0()) -> 0() 29.07/10.25 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 29.07/10.25 , activate(n__fact(X)) -> fact(activate(X)) 29.07/10.25 , activate(n__p(X)) -> p(activate(X)) 29.07/10.25 , p(X) -> n__p(X) } 29.07/10.25 Obligation: 29.07/10.25 innermost runtime complexity 29.07/10.25 Answer: 29.07/10.25 YES(O(1),O(1)) 29.07/10.25 29.07/10.25 Empty rules are trivially bounded 29.07/10.25 29.07/10.25 Hurray, we answered YES(O(1),O(n^1)) 29.07/10.26 EOF