YES(O(1),O(n^2)) 208.08/59.08 YES(O(1),O(n^2)) 208.08/59.08 208.08/59.08 We are left with following problem, upon which TcT provides the 208.08/59.08 certificate YES(O(1),O(n^2)). 208.08/59.08 208.08/59.08 Strict Trs: 208.08/59.08 { min(X, 0()) -> X 208.08/59.08 , min(s(X), s(Y)) -> min(X, Y) 208.08/59.08 , quot(0(), s(Y)) -> 0() 208.08/59.08 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) 208.08/59.08 , log(s(0())) -> 0() 208.08/59.08 , log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) } 208.08/59.08 Obligation: 208.08/59.08 innermost runtime complexity 208.08/59.08 Answer: 208.08/59.08 YES(O(1),O(n^2)) 208.08/59.08 208.08/59.08 The weightgap principle applies (using the following nonconstant 208.08/59.08 growth matrix-interpretation) 208.08/59.08 208.08/59.08 The following argument positions are usable: 208.08/59.08 Uargs(s) = {1}, Uargs(quot) = {1}, Uargs(log) = {1} 208.08/59.08 208.08/59.08 TcT has computed the following matrix interpretation satisfying 208.08/59.08 not(EDA) and not(IDA(1)). 208.08/59.08 208.08/59.08 [min](x1, x2) = [1] x1 + [1] 208.08/59.08 208.08/59.08 [0] = [0] 208.08/59.08 208.08/59.08 [s](x1) = [1] x1 + [0] 208.08/59.08 208.08/59.08 [quot](x1, x2) = [1] x1 + [0] 208.08/59.08 208.08/59.08 [log](x1) = [1] x1 + [0] 208.08/59.08 208.08/59.08 The order satisfies the following ordering constraints: 208.08/59.08 208.08/59.08 [min(X, 0())] = [1] X + [1] 208.08/59.08 > [1] X + [0] 208.08/59.08 = [X] 208.08/59.08 208.08/59.08 [min(s(X), s(Y))] = [1] X + [1] 208.08/59.08 >= [1] X + [1] 208.08/59.08 = [min(X, Y)] 208.08/59.08 208.08/59.08 [quot(0(), s(Y))] = [0] 208.08/59.08 >= [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [quot(s(X), s(Y))] = [1] X + [0] 208.08/59.08 ? [1] X + [1] 208.08/59.08 = [s(quot(min(X, Y), s(Y)))] 208.08/59.08 208.08/59.08 [log(s(0()))] = [0] 208.08/59.08 >= [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [log(s(s(X)))] = [1] X + [0] 208.08/59.08 >= [1] X + [0] 208.08/59.08 = [s(log(s(quot(X, s(s(0()))))))] 208.08/59.08 208.08/59.08 208.08/59.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 208.08/59.08 208.08/59.08 We are left with following problem, upon which TcT provides the 208.08/59.08 certificate YES(O(1),O(n^2)). 208.08/59.08 208.08/59.08 Strict Trs: 208.08/59.08 { min(s(X), s(Y)) -> min(X, Y) 208.08/59.08 , quot(0(), s(Y)) -> 0() 208.08/59.08 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) 208.08/59.08 , log(s(0())) -> 0() 208.08/59.08 , log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) } 208.08/59.08 Weak Trs: { min(X, 0()) -> X } 208.08/59.08 Obligation: 208.08/59.08 innermost runtime complexity 208.08/59.08 Answer: 208.08/59.08 YES(O(1),O(n^2)) 208.08/59.08 208.08/59.08 The weightgap principle applies (using the following nonconstant 208.08/59.08 growth matrix-interpretation) 208.08/59.08 208.08/59.08 The following argument positions are usable: 208.08/59.08 Uargs(s) = {1}, Uargs(quot) = {1}, Uargs(log) = {1} 208.08/59.08 208.08/59.08 TcT has computed the following matrix interpretation satisfying 208.08/59.08 not(EDA) and not(IDA(1)). 208.08/59.08 208.08/59.08 [min](x1, x2) = [1] x1 + [0] 208.08/59.08 208.08/59.08 [0] = [0] 208.08/59.08 208.08/59.08 [s](x1) = [1] x1 + [0] 208.08/59.08 208.08/59.08 [quot](x1, x2) = [1] x1 + [1] 208.08/59.08 208.08/59.08 [log](x1) = [1] x1 + [0] 208.08/59.08 208.08/59.08 The order satisfies the following ordering constraints: 208.08/59.08 208.08/59.08 [min(X, 0())] = [1] X + [0] 208.08/59.08 >= [1] X + [0] 208.08/59.08 = [X] 208.08/59.08 208.08/59.08 [min(s(X), s(Y))] = [1] X + [0] 208.08/59.08 >= [1] X + [0] 208.08/59.08 = [min(X, Y)] 208.08/59.08 208.08/59.08 [quot(0(), s(Y))] = [1] 208.08/59.08 > [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [quot(s(X), s(Y))] = [1] X + [1] 208.08/59.08 >= [1] X + [1] 208.08/59.08 = [s(quot(min(X, Y), s(Y)))] 208.08/59.08 208.08/59.08 [log(s(0()))] = [0] 208.08/59.08 >= [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [log(s(s(X)))] = [1] X + [0] 208.08/59.08 ? [1] X + [1] 208.08/59.08 = [s(log(s(quot(X, s(s(0()))))))] 208.08/59.08 208.08/59.08 208.08/59.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 208.08/59.08 208.08/59.08 We are left with following problem, upon which TcT provides the 208.08/59.08 certificate YES(O(1),O(n^2)). 208.08/59.08 208.08/59.08 Strict Trs: 208.08/59.08 { min(s(X), s(Y)) -> min(X, Y) 208.08/59.08 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) 208.08/59.08 , log(s(0())) -> 0() 208.08/59.08 , log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) } 208.08/59.08 Weak Trs: 208.08/59.08 { min(X, 0()) -> X 208.08/59.08 , quot(0(), s(Y)) -> 0() } 208.08/59.08 Obligation: 208.08/59.08 innermost runtime complexity 208.08/59.08 Answer: 208.08/59.08 YES(O(1),O(n^2)) 208.08/59.08 208.08/59.08 The weightgap principle applies (using the following nonconstant 208.08/59.08 growth matrix-interpretation) 208.08/59.08 208.08/59.08 The following argument positions are usable: 208.08/59.08 Uargs(s) = {1}, Uargs(quot) = {1}, Uargs(log) = {1} 208.08/59.08 208.08/59.08 TcT has computed the following matrix interpretation satisfying 208.08/59.08 not(EDA) and not(IDA(1)). 208.08/59.08 208.08/59.08 [min](x1, x2) = [1] x1 + [3] 208.08/59.08 208.08/59.08 [0] = [0] 208.08/59.08 208.08/59.08 [s](x1) = [1] x1 + [4] 208.08/59.08 208.08/59.08 [quot](x1, x2) = [1] x1 + [5] 208.08/59.08 208.08/59.08 [log](x1) = [1] x1 + [0] 208.08/59.08 208.08/59.08 The order satisfies the following ordering constraints: 208.08/59.08 208.08/59.08 [min(X, 0())] = [1] X + [3] 208.08/59.08 > [1] X + [0] 208.08/59.08 = [X] 208.08/59.08 208.08/59.08 [min(s(X), s(Y))] = [1] X + [7] 208.08/59.08 > [1] X + [3] 208.08/59.08 = [min(X, Y)] 208.08/59.08 208.08/59.08 [quot(0(), s(Y))] = [5] 208.08/59.08 > [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [quot(s(X), s(Y))] = [1] X + [9] 208.08/59.08 ? [1] X + [12] 208.08/59.08 = [s(quot(min(X, Y), s(Y)))] 208.08/59.08 208.08/59.08 [log(s(0()))] = [4] 208.08/59.08 > [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [log(s(s(X)))] = [1] X + [8] 208.08/59.08 ? [1] X + [13] 208.08/59.08 = [s(log(s(quot(X, s(s(0()))))))] 208.08/59.08 208.08/59.08 208.08/59.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 208.08/59.08 208.08/59.08 We are left with following problem, upon which TcT provides the 208.08/59.08 certificate YES(O(1),O(n^2)). 208.08/59.08 208.08/59.08 Strict Trs: 208.08/59.08 { quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) 208.08/59.08 , log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) } 208.08/59.08 Weak Trs: 208.08/59.08 { min(X, 0()) -> X 208.08/59.08 , min(s(X), s(Y)) -> min(X, Y) 208.08/59.08 , quot(0(), s(Y)) -> 0() 208.08/59.08 , log(s(0())) -> 0() } 208.08/59.08 Obligation: 208.08/59.08 innermost runtime complexity 208.08/59.08 Answer: 208.08/59.08 YES(O(1),O(n^2)) 208.08/59.08 208.08/59.08 We use the processor 'matrix interpretation of dimension 1' to 208.08/59.08 orient following rules strictly. 208.08/59.08 208.08/59.08 Trs: { log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) } 208.08/59.08 208.08/59.08 The induced complexity on above rules (modulo remaining rules) is 208.08/59.08 YES(?,O(n^1)) . These rules are moved into the corresponding weak 208.08/59.08 component(s). 208.08/59.08 208.08/59.08 Sub-proof: 208.08/59.08 ---------- 208.08/59.08 The following argument positions are usable: 208.08/59.08 Uargs(s) = {1}, Uargs(quot) = {1}, Uargs(log) = {1} 208.08/59.08 208.08/59.08 TcT has computed the following constructor-based matrix 208.08/59.08 interpretation satisfying not(EDA). 208.08/59.08 208.08/59.08 [min](x1, x2) = [1] x1 + [0] 208.08/59.08 208.08/59.08 [0] = [1] 208.08/59.08 208.08/59.08 [s](x1) = [1] x1 + [1] 208.08/59.08 208.08/59.08 [quot](x1, x2) = [1] x1 + [0] 208.08/59.08 208.08/59.08 [log](x1) = [4] x1 + [0] 208.08/59.08 208.08/59.08 The order satisfies the following ordering constraints: 208.08/59.08 208.08/59.08 [min(X, 0())] = [1] X + [0] 208.08/59.08 >= [1] X + [0] 208.08/59.08 = [X] 208.08/59.08 208.08/59.08 [min(s(X), s(Y))] = [1] X + [1] 208.08/59.08 > [1] X + [0] 208.08/59.08 = [min(X, Y)] 208.08/59.08 208.08/59.08 [quot(0(), s(Y))] = [1] 208.08/59.08 >= [1] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [quot(s(X), s(Y))] = [1] X + [1] 208.08/59.08 >= [1] X + [1] 208.08/59.08 = [s(quot(min(X, Y), s(Y)))] 208.08/59.08 208.08/59.08 [log(s(0()))] = [8] 208.08/59.08 > [1] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [log(s(s(X)))] = [4] X + [8] 208.08/59.08 > [4] X + [5] 208.08/59.08 = [s(log(s(quot(X, s(s(0()))))))] 208.08/59.08 208.08/59.08 208.08/59.08 We return to the main proof. 208.08/59.08 208.08/59.08 We are left with following problem, upon which TcT provides the 208.08/59.08 certificate YES(O(1),O(n^2)). 208.08/59.08 208.08/59.08 Strict Trs: { quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } 208.08/59.08 Weak Trs: 208.08/59.08 { min(X, 0()) -> X 208.08/59.08 , min(s(X), s(Y)) -> min(X, Y) 208.08/59.08 , quot(0(), s(Y)) -> 0() 208.08/59.08 , log(s(0())) -> 0() 208.08/59.08 , log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) } 208.08/59.08 Obligation: 208.08/59.08 innermost runtime complexity 208.08/59.08 Answer: 208.08/59.08 YES(O(1),O(n^2)) 208.08/59.08 208.08/59.08 We use the processor 'matrix interpretation of dimension 2' to 208.08/59.08 orient following rules strictly. 208.08/59.08 208.08/59.08 Trs: { quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) } 208.08/59.08 208.08/59.08 The induced complexity on above rules (modulo remaining rules) is 208.08/59.08 YES(?,O(n^2)) . These rules are moved into the corresponding weak 208.08/59.08 component(s). 208.08/59.08 208.08/59.08 Sub-proof: 208.08/59.08 ---------- 208.08/59.08 The following argument positions are usable: 208.08/59.08 Uargs(s) = {1}, Uargs(quot) = {1}, Uargs(log) = {1} 208.08/59.08 208.08/59.08 TcT has computed the following constructor-based matrix 208.08/59.08 interpretation satisfying not(EDA). 208.08/59.08 208.08/59.08 [min](x1, x2) = [1 0] x1 + [0] 208.08/59.08 [0 1] [0] 208.08/59.08 208.08/59.08 [0] = [0] 208.08/59.08 [0] 208.08/59.08 208.08/59.08 [s](x1) = [1 2] x1 + [0] 208.08/59.08 [0 1] [1] 208.08/59.08 208.08/59.08 [quot](x1, x2) = [1 1] x1 + [0] 208.08/59.08 [0 1] [0] 208.08/59.08 208.08/59.08 [log](x1) = [3 0] x1 + [4] 208.08/59.08 [0 1] [0] 208.08/59.08 208.08/59.08 The order satisfies the following ordering constraints: 208.08/59.08 208.08/59.08 [min(X, 0())] = [1 0] X + [0] 208.08/59.08 [0 1] [0] 208.08/59.08 >= [1 0] X + [0] 208.08/59.08 [0 1] [0] 208.08/59.08 = [X] 208.08/59.08 208.08/59.08 [min(s(X), s(Y))] = [1 2] X + [0] 208.08/59.08 [0 1] [1] 208.08/59.08 >= [1 0] X + [0] 208.08/59.08 [0 1] [0] 208.08/59.08 = [min(X, Y)] 208.08/59.08 208.08/59.08 [quot(0(), s(Y))] = [0] 208.08/59.08 [0] 208.08/59.08 >= [0] 208.08/59.08 [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [quot(s(X), s(Y))] = [1 3] X + [1] 208.08/59.08 [0 1] [1] 208.08/59.08 > [1 3] X + [0] 208.08/59.08 [0 1] [1] 208.08/59.08 = [s(quot(min(X, Y), s(Y)))] 208.08/59.08 208.08/59.08 [log(s(0()))] = [4] 208.08/59.08 [1] 208.08/59.08 > [0] 208.08/59.08 [0] 208.08/59.08 = [0()] 208.08/59.08 208.08/59.08 [log(s(s(X)))] = [3 12] X + [10] 208.08/59.08 [0 1] [2] 208.08/59.08 > [3 11] X + [6] 208.08/59.08 [0 1] [2] 208.08/59.08 = [s(log(s(quot(X, s(s(0()))))))] 208.08/59.08 208.08/59.08 208.08/59.08 We return to the main proof. 208.08/59.08 208.08/59.08 We are left with following problem, upon which TcT provides the 208.08/59.08 certificate YES(O(1),O(1)). 208.08/59.08 208.08/59.08 Weak Trs: 208.08/59.08 { min(X, 0()) -> X 208.08/59.08 , min(s(X), s(Y)) -> min(X, Y) 208.08/59.08 , quot(0(), s(Y)) -> 0() 208.08/59.08 , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) 208.08/59.08 , log(s(0())) -> 0() 208.08/59.08 , log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) } 208.08/59.08 Obligation: 208.08/59.08 innermost runtime complexity 208.08/59.08 Answer: 208.08/59.08 YES(O(1),O(1)) 208.08/59.08 208.08/59.08 Empty rules are trivially bounded 208.08/59.08 208.08/59.08 Hurray, we answered YES(O(1),O(n^2)) 208.49/59.28 EOF