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