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