MAYBE 530.18/292.23 MAYBE 530.18/292.23 530.18/292.23 We are left with following problem, upon which TcT provides the 530.18/292.23 certificate MAYBE. 530.18/292.23 530.18/292.23 Strict Trs: 530.18/292.23 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.23 , minus(X, 0()) -> X 530.18/292.23 , pred(s(X)) -> X 530.18/292.23 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.23 , le(s(X), 0()) -> false() 530.18/292.23 , le(0(), Y) -> true() 530.18/292.23 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.23 , gcd(s(X), 0()) -> s(X) 530.18/292.23 , gcd(0(), Y) -> 0() 530.18/292.23 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.23 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.23 Obligation: 530.18/292.23 runtime complexity 530.18/292.23 Answer: 530.18/292.23 MAYBE 530.18/292.23 530.18/292.23 None of the processors succeeded. 530.18/292.23 530.18/292.23 Details of failed attempt(s): 530.18/292.23 ----------------------------- 530.18/292.23 1) 'Best' failed due to the following reason: 530.18/292.23 530.18/292.23 None of the processors succeeded. 530.18/292.23 530.18/292.23 Details of failed attempt(s): 530.18/292.23 ----------------------------- 530.18/292.23 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 530.18/292.23 seconds)' failed due to the following reason: 530.18/292.23 530.18/292.23 The weightgap principle applies (using the following nonconstant 530.18/292.23 growth matrix-interpretation) 530.18/292.23 530.18/292.23 The following argument positions are usable: 530.18/292.23 Uargs(pred) = {1}, Uargs(gcd) = {1}, Uargs(if) = {1} 530.18/292.23 530.18/292.23 TcT has computed the following matrix interpretation satisfying 530.18/292.23 not(EDA) and not(IDA(1)). 530.18/292.23 530.18/292.23 [minus](x1, x2) = [1] x1 + [7] 530.18/292.23 530.18/292.23 [s](x1) = [1] x1 + [7] 530.18/292.23 530.18/292.23 [pred](x1) = [1] x1 + [7] 530.18/292.23 530.18/292.23 [0] = [7] 530.18/292.23 530.18/292.23 [le](x1, x2) = [1] 530.18/292.23 530.18/292.23 [false] = [1] 530.18/292.23 530.18/292.23 [true] = [1] 530.18/292.23 530.18/292.23 [gcd](x1, x2) = [1] x1 + [1] x2 + [1] 530.18/292.23 530.18/292.23 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 530.18/292.23 530.18/292.23 The order satisfies the following ordering constraints: 530.18/292.23 530.18/292.23 [minus(X, s(Y))] = [1] X + [7] 530.18/292.23 ? [1] X + [14] 530.18/292.23 = [pred(minus(X, Y))] 530.18/292.23 530.18/292.23 [minus(X, 0())] = [1] X + [7] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [pred(s(X))] = [1] X + [14] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [le(s(X), s(Y))] = [1] 530.18/292.23 >= [1] 530.18/292.23 = [le(X, Y)] 530.18/292.23 530.18/292.23 [le(s(X), 0())] = [1] 530.18/292.23 >= [1] 530.18/292.23 = [false()] 530.18/292.23 530.18/292.23 [le(0(), Y)] = [1] 530.18/292.23 >= [1] 530.18/292.23 = [true()] 530.18/292.23 530.18/292.23 [gcd(s(X), s(Y))] = [1] X + [1] Y + [15] 530.18/292.23 >= [1] X + [1] Y + [15] 530.18/292.23 = [if(le(Y, X), s(X), s(Y))] 530.18/292.23 530.18/292.23 [gcd(s(X), 0())] = [1] X + [15] 530.18/292.23 > [1] X + [7] 530.18/292.23 = [s(X)] 530.18/292.23 530.18/292.23 [gcd(0(), Y)] = [1] Y + [8] 530.18/292.23 > [7] 530.18/292.23 = [0()] 530.18/292.23 530.18/292.23 [if(false(), s(X), s(Y))] = [1] X + [1] Y + [15] 530.18/292.23 >= [1] X + [1] Y + [15] 530.18/292.23 = [gcd(minus(Y, X), s(X))] 530.18/292.23 530.18/292.23 [if(true(), s(X), s(Y))] = [1] X + [1] Y + [15] 530.18/292.23 >= [1] X + [1] Y + [15] 530.18/292.23 = [gcd(minus(X, Y), s(Y))] 530.18/292.23 530.18/292.23 530.18/292.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 530.18/292.23 530.18/292.23 We are left with following problem, upon which TcT provides the 530.18/292.23 certificate MAYBE. 530.18/292.23 530.18/292.23 Strict Trs: 530.18/292.23 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.23 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.23 , le(s(X), 0()) -> false() 530.18/292.23 , le(0(), Y) -> true() 530.18/292.23 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.23 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.23 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.23 Weak Trs: 530.18/292.23 { minus(X, 0()) -> X 530.18/292.23 , pred(s(X)) -> X 530.18/292.23 , gcd(s(X), 0()) -> s(X) 530.18/292.23 , gcd(0(), Y) -> 0() } 530.18/292.23 Obligation: 530.18/292.23 runtime complexity 530.18/292.23 Answer: 530.18/292.23 MAYBE 530.18/292.23 530.18/292.23 The weightgap principle applies (using the following nonconstant 530.18/292.23 growth matrix-interpretation) 530.18/292.23 530.18/292.23 The following argument positions are usable: 530.18/292.23 Uargs(pred) = {1}, Uargs(gcd) = {1}, Uargs(if) = {1} 530.18/292.23 530.18/292.23 TcT has computed the following matrix interpretation satisfying 530.18/292.23 not(EDA) and not(IDA(1)). 530.18/292.23 530.18/292.23 [minus](x1, x2) = [1] x1 + [0] 530.18/292.23 530.18/292.23 [s](x1) = [1] x1 + [0] 530.18/292.23 530.18/292.23 [pred](x1) = [1] x1 + [7] 530.18/292.23 530.18/292.23 [0] = [7] 530.18/292.23 530.18/292.23 [le](x1, x2) = [1] 530.18/292.23 530.18/292.23 [false] = [0] 530.18/292.23 530.18/292.23 [true] = [0] 530.18/292.23 530.18/292.23 [gcd](x1, x2) = [1] x1 + [1] x2 + [0] 530.18/292.23 530.18/292.23 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 530.18/292.23 530.18/292.23 The order satisfies the following ordering constraints: 530.18/292.23 530.18/292.23 [minus(X, s(Y))] = [1] X + [0] 530.18/292.23 ? [1] X + [7] 530.18/292.23 = [pred(minus(X, Y))] 530.18/292.23 530.18/292.23 [minus(X, 0())] = [1] X + [0] 530.18/292.23 >= [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [pred(s(X))] = [1] X + [7] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [le(s(X), s(Y))] = [1] 530.18/292.23 >= [1] 530.18/292.23 = [le(X, Y)] 530.18/292.23 530.18/292.23 [le(s(X), 0())] = [1] 530.18/292.23 > [0] 530.18/292.23 = [false()] 530.18/292.23 530.18/292.23 [le(0(), Y)] = [1] 530.18/292.23 > [0] 530.18/292.23 = [true()] 530.18/292.23 530.18/292.23 [gcd(s(X), s(Y))] = [1] X + [1] Y + [0] 530.18/292.23 ? [1] X + [1] Y + [1] 530.18/292.23 = [if(le(Y, X), s(X), s(Y))] 530.18/292.23 530.18/292.23 [gcd(s(X), 0())] = [1] X + [7] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [s(X)] 530.18/292.23 530.18/292.23 [gcd(0(), Y)] = [1] Y + [7] 530.18/292.23 >= [7] 530.18/292.23 = [0()] 530.18/292.23 530.18/292.23 [if(false(), s(X), s(Y))] = [1] X + [1] Y + [0] 530.18/292.23 >= [1] X + [1] Y + [0] 530.18/292.23 = [gcd(minus(Y, X), s(X))] 530.18/292.23 530.18/292.23 [if(true(), s(X), s(Y))] = [1] X + [1] Y + [0] 530.18/292.23 >= [1] X + [1] Y + [0] 530.18/292.23 = [gcd(minus(X, Y), s(Y))] 530.18/292.23 530.18/292.23 530.18/292.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 530.18/292.23 530.18/292.23 We are left with following problem, upon which TcT provides the 530.18/292.23 certificate MAYBE. 530.18/292.23 530.18/292.23 Strict Trs: 530.18/292.23 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.23 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.23 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.23 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.23 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.23 Weak Trs: 530.18/292.23 { minus(X, 0()) -> X 530.18/292.23 , pred(s(X)) -> X 530.18/292.23 , le(s(X), 0()) -> false() 530.18/292.23 , le(0(), Y) -> true() 530.18/292.23 , gcd(s(X), 0()) -> s(X) 530.18/292.23 , gcd(0(), Y) -> 0() } 530.18/292.23 Obligation: 530.18/292.23 runtime complexity 530.18/292.23 Answer: 530.18/292.23 MAYBE 530.18/292.23 530.18/292.23 The weightgap principle applies (using the following nonconstant 530.18/292.23 growth matrix-interpretation) 530.18/292.23 530.18/292.23 The following argument positions are usable: 530.18/292.23 Uargs(pred) = {1}, Uargs(gcd) = {1}, Uargs(if) = {1} 530.18/292.23 530.18/292.23 TcT has computed the following matrix interpretation satisfying 530.18/292.23 not(EDA) and not(IDA(1)). 530.18/292.23 530.18/292.23 [minus](x1, x2) = [1] x1 + [0] 530.18/292.23 530.18/292.23 [s](x1) = [1] x1 + [0] 530.18/292.23 530.18/292.23 [pred](x1) = [1] x1 + [7] 530.18/292.23 530.18/292.23 [0] = [7] 530.18/292.23 530.18/292.23 [le](x1, x2) = [4] 530.18/292.23 530.18/292.23 [false] = [1] 530.18/292.23 530.18/292.23 [true] = [0] 530.18/292.23 530.18/292.23 [gcd](x1, x2) = [1] x1 + [1] x2 + [0] 530.18/292.23 530.18/292.23 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 530.18/292.23 530.18/292.23 The order satisfies the following ordering constraints: 530.18/292.23 530.18/292.23 [minus(X, s(Y))] = [1] X + [0] 530.18/292.23 ? [1] X + [7] 530.18/292.23 = [pred(minus(X, Y))] 530.18/292.23 530.18/292.23 [minus(X, 0())] = [1] X + [0] 530.18/292.23 >= [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [pred(s(X))] = [1] X + [7] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [le(s(X), s(Y))] = [4] 530.18/292.23 >= [4] 530.18/292.23 = [le(X, Y)] 530.18/292.23 530.18/292.23 [le(s(X), 0())] = [4] 530.18/292.23 > [1] 530.18/292.23 = [false()] 530.18/292.23 530.18/292.23 [le(0(), Y)] = [4] 530.18/292.23 > [0] 530.18/292.23 = [true()] 530.18/292.23 530.18/292.23 [gcd(s(X), s(Y))] = [1] X + [1] Y + [0] 530.18/292.23 ? [1] X + [1] Y + [4] 530.18/292.23 = [if(le(Y, X), s(X), s(Y))] 530.18/292.23 530.18/292.23 [gcd(s(X), 0())] = [1] X + [7] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [s(X)] 530.18/292.23 530.18/292.23 [gcd(0(), Y)] = [1] Y + [7] 530.18/292.23 >= [7] 530.18/292.23 = [0()] 530.18/292.23 530.18/292.23 [if(false(), s(X), s(Y))] = [1] X + [1] Y + [1] 530.18/292.23 > [1] X + [1] Y + [0] 530.18/292.23 = [gcd(minus(Y, X), s(X))] 530.18/292.23 530.18/292.23 [if(true(), s(X), s(Y))] = [1] X + [1] Y + [0] 530.18/292.23 >= [1] X + [1] Y + [0] 530.18/292.23 = [gcd(minus(X, Y), s(Y))] 530.18/292.23 530.18/292.23 530.18/292.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 530.18/292.23 530.18/292.23 We are left with following problem, upon which TcT provides the 530.18/292.23 certificate MAYBE. 530.18/292.23 530.18/292.23 Strict Trs: 530.18/292.23 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.23 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.23 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.23 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.23 Weak Trs: 530.18/292.23 { minus(X, 0()) -> X 530.18/292.23 , pred(s(X)) -> X 530.18/292.23 , le(s(X), 0()) -> false() 530.18/292.23 , le(0(), Y) -> true() 530.18/292.23 , gcd(s(X), 0()) -> s(X) 530.18/292.23 , gcd(0(), Y) -> 0() 530.18/292.23 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) } 530.18/292.23 Obligation: 530.18/292.23 runtime complexity 530.18/292.23 Answer: 530.18/292.23 MAYBE 530.18/292.23 530.18/292.23 The weightgap principle applies (using the following nonconstant 530.18/292.23 growth matrix-interpretation) 530.18/292.23 530.18/292.23 The following argument positions are usable: 530.18/292.23 Uargs(pred) = {1}, Uargs(gcd) = {1}, Uargs(if) = {1} 530.18/292.23 530.18/292.23 TcT has computed the following matrix interpretation satisfying 530.18/292.23 not(EDA) and not(IDA(1)). 530.18/292.23 530.18/292.23 [minus](x1, x2) = [1] x1 + [0] 530.18/292.23 530.18/292.23 [s](x1) = [1] x1 + [4] 530.18/292.23 530.18/292.23 [pred](x1) = [1] x1 + [7] 530.18/292.23 530.18/292.23 [0] = [7] 530.18/292.23 530.18/292.23 [le](x1, x2) = [0] 530.18/292.23 530.18/292.23 [false] = [0] 530.18/292.23 530.18/292.23 [true] = [0] 530.18/292.23 530.18/292.23 [gcd](x1, x2) = [1] x1 + [1] x2 + [0] 530.18/292.23 530.18/292.23 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 530.18/292.23 530.18/292.23 The order satisfies the following ordering constraints: 530.18/292.23 530.18/292.23 [minus(X, s(Y))] = [1] X + [0] 530.18/292.23 ? [1] X + [7] 530.18/292.23 = [pred(minus(X, Y))] 530.18/292.23 530.18/292.23 [minus(X, 0())] = [1] X + [0] 530.18/292.23 >= [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [pred(s(X))] = [1] X + [11] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [le(s(X), s(Y))] = [0] 530.18/292.23 >= [0] 530.18/292.23 = [le(X, Y)] 530.18/292.23 530.18/292.23 [le(s(X), 0())] = [0] 530.18/292.23 >= [0] 530.18/292.23 = [false()] 530.18/292.23 530.18/292.23 [le(0(), Y)] = [0] 530.18/292.23 >= [0] 530.18/292.23 = [true()] 530.18/292.23 530.18/292.23 [gcd(s(X), s(Y))] = [1] X + [1] Y + [8] 530.18/292.23 >= [1] X + [1] Y + [8] 530.18/292.23 = [if(le(Y, X), s(X), s(Y))] 530.18/292.23 530.18/292.23 [gcd(s(X), 0())] = [1] X + [11] 530.18/292.23 > [1] X + [4] 530.18/292.23 = [s(X)] 530.18/292.23 530.18/292.23 [gcd(0(), Y)] = [1] Y + [7] 530.18/292.23 >= [7] 530.18/292.23 = [0()] 530.18/292.23 530.18/292.23 [if(false(), s(X), s(Y))] = [1] X + [1] Y + [8] 530.18/292.23 > [1] X + [1] Y + [4] 530.18/292.23 = [gcd(minus(Y, X), s(X))] 530.18/292.23 530.18/292.23 [if(true(), s(X), s(Y))] = [1] X + [1] Y + [8] 530.18/292.23 > [1] X + [1] Y + [4] 530.18/292.23 = [gcd(minus(X, Y), s(Y))] 530.18/292.23 530.18/292.23 530.18/292.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 530.18/292.23 530.18/292.23 We are left with following problem, upon which TcT provides the 530.18/292.23 certificate MAYBE. 530.18/292.23 530.18/292.23 Strict Trs: 530.18/292.23 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.23 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.23 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) } 530.18/292.23 Weak Trs: 530.18/292.23 { minus(X, 0()) -> X 530.18/292.23 , pred(s(X)) -> X 530.18/292.23 , le(s(X), 0()) -> false() 530.18/292.23 , le(0(), Y) -> true() 530.18/292.23 , gcd(s(X), 0()) -> s(X) 530.18/292.23 , gcd(0(), Y) -> 0() 530.18/292.23 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.23 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.23 Obligation: 530.18/292.23 runtime complexity 530.18/292.23 Answer: 530.18/292.23 MAYBE 530.18/292.23 530.18/292.23 The weightgap principle applies (using the following nonconstant 530.18/292.23 growth matrix-interpretation) 530.18/292.23 530.18/292.23 The following argument positions are usable: 530.18/292.23 Uargs(pred) = {1}, Uargs(gcd) = {1}, Uargs(if) = {1} 530.18/292.23 530.18/292.23 TcT has computed the following matrix interpretation satisfying 530.18/292.23 not(EDA) and not(IDA(1)). 530.18/292.23 530.18/292.23 [minus](x1, x2) = [1] x1 + [0] 530.18/292.23 530.18/292.23 [s](x1) = [1] x1 + [4] 530.18/292.23 530.18/292.23 [pred](x1) = [1] x1 + [7] 530.18/292.23 530.18/292.23 [0] = [7] 530.18/292.23 530.18/292.23 [le](x1, x2) = [0] 530.18/292.23 530.18/292.23 [false] = [0] 530.18/292.23 530.18/292.23 [true] = [0] 530.18/292.23 530.18/292.23 [gcd](x1, x2) = [1] x1 + [1] x2 + [4] 530.18/292.23 530.18/292.23 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 530.18/292.23 530.18/292.23 The order satisfies the following ordering constraints: 530.18/292.23 530.18/292.23 [minus(X, s(Y))] = [1] X + [0] 530.18/292.23 ? [1] X + [7] 530.18/292.23 = [pred(minus(X, Y))] 530.18/292.23 530.18/292.23 [minus(X, 0())] = [1] X + [0] 530.18/292.23 >= [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [pred(s(X))] = [1] X + [11] 530.18/292.23 > [1] X + [0] 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [le(s(X), s(Y))] = [0] 530.18/292.23 >= [0] 530.18/292.23 = [le(X, Y)] 530.18/292.23 530.18/292.23 [le(s(X), 0())] = [0] 530.18/292.23 >= [0] 530.18/292.23 = [false()] 530.18/292.23 530.18/292.23 [le(0(), Y)] = [0] 530.18/292.23 >= [0] 530.18/292.23 = [true()] 530.18/292.23 530.18/292.23 [gcd(s(X), s(Y))] = [1] X + [1] Y + [12] 530.18/292.23 > [1] X + [1] Y + [8] 530.18/292.23 = [if(le(Y, X), s(X), s(Y))] 530.18/292.23 530.18/292.23 [gcd(s(X), 0())] = [1] X + [15] 530.18/292.23 > [1] X + [4] 530.18/292.23 = [s(X)] 530.18/292.23 530.18/292.23 [gcd(0(), Y)] = [1] Y + [11] 530.18/292.23 > [7] 530.18/292.23 = [0()] 530.18/292.23 530.18/292.23 [if(false(), s(X), s(Y))] = [1] X + [1] Y + [8] 530.18/292.23 >= [1] X + [1] Y + [8] 530.18/292.23 = [gcd(minus(Y, X), s(X))] 530.18/292.23 530.18/292.23 [if(true(), s(X), s(Y))] = [1] X + [1] Y + [8] 530.18/292.23 >= [1] X + [1] Y + [8] 530.18/292.23 = [gcd(minus(X, Y), s(Y))] 530.18/292.23 530.18/292.23 530.18/292.23 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 530.18/292.23 530.18/292.23 We are left with following problem, upon which TcT provides the 530.18/292.23 certificate MAYBE. 530.18/292.23 530.18/292.23 Strict Trs: 530.18/292.23 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.23 , le(s(X), s(Y)) -> le(X, Y) } 530.18/292.23 Weak Trs: 530.18/292.23 { minus(X, 0()) -> X 530.18/292.23 , pred(s(X)) -> X 530.18/292.23 , le(s(X), 0()) -> false() 530.18/292.23 , le(0(), Y) -> true() 530.18/292.23 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.23 , gcd(s(X), 0()) -> s(X) 530.18/292.23 , gcd(0(), Y) -> 0() 530.18/292.23 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.23 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.23 Obligation: 530.18/292.23 runtime complexity 530.18/292.23 Answer: 530.18/292.23 MAYBE 530.18/292.23 530.18/292.23 None of the processors succeeded. 530.18/292.23 530.18/292.23 Details of failed attempt(s): 530.18/292.23 ----------------------------- 530.18/292.23 1) 'empty' failed due to the following reason: 530.18/292.23 530.18/292.23 Empty strict component of the problem is NOT empty. 530.18/292.23 530.18/292.23 2) 'With Problem ...' failed due to the following reason: 530.18/292.23 530.18/292.23 None of the processors succeeded. 530.18/292.23 530.18/292.23 Details of failed attempt(s): 530.18/292.23 ----------------------------- 530.18/292.23 1) 'empty' failed due to the following reason: 530.18/292.23 530.18/292.23 Empty strict component of the problem is NOT empty. 530.18/292.23 530.18/292.23 2) 'Fastest' failed due to the following reason: 530.18/292.23 530.18/292.23 None of the processors succeeded. 530.18/292.23 530.18/292.23 Details of failed attempt(s): 530.18/292.23 ----------------------------- 530.18/292.23 1) 'With Problem ...' failed due to the following reason: 530.18/292.23 530.18/292.23 We use the processor 'polynomial interpretation' to orient 530.18/292.23 following rules strictly. 530.18/292.23 530.18/292.23 Trs: { le(s(X), s(Y)) -> le(X, Y) } 530.18/292.23 530.18/292.23 The induced complexity on above rules (modulo remaining rules) is 530.18/292.23 YES(?,O(n^2)) . These rules are moved into the corresponding weak 530.18/292.23 component(s). 530.18/292.23 530.18/292.23 Sub-proof: 530.18/292.23 ---------- 530.18/292.23 We consider the following typing: 530.18/292.23 530.18/292.23 minus :: (b,b) -> b 530.18/292.23 s :: b -> b 530.18/292.23 pred :: b -> b 530.18/292.23 0 :: b 530.18/292.23 le :: (b,b) -> a 530.18/292.23 false :: a 530.18/292.23 true :: a 530.18/292.23 gcd :: (b,b) -> b 530.18/292.23 if :: (a,b,b) -> b 530.18/292.23 530.18/292.23 The following argument positions are considered usable: 530.18/292.23 530.18/292.23 Uargs(pred) = {1}, Uargs(gcd) = {1}, Uargs(if) = {1} 530.18/292.23 530.18/292.23 TcT has computed the following constructor-restricted 530.18/292.23 typedpolynomial interpretation. 530.18/292.23 530.18/292.23 [minus](x1, x2) = x1 530.18/292.23 530.18/292.23 [s](x1) = 1 + x1 530.18/292.23 530.18/292.23 [pred](x1) = x1 530.18/292.23 530.18/292.23 [0]() = 0 530.18/292.23 530.18/292.23 [le](x1, x2) = x2 530.18/292.23 530.18/292.23 [false]() = 0 530.18/292.23 530.18/292.23 [true]() = 0 530.18/292.23 530.18/292.23 [gcd](x1, x2) = 3*x1 + x1^2 + 2*x2 + x2^2 530.18/292.23 530.18/292.23 [if](x1, x2, x3) = x1 + 2*x2 + x2^2 + 2*x3 + x3^2 530.18/292.23 530.18/292.23 530.18/292.23 This order satisfies the following ordering constraints. 530.18/292.23 530.18/292.23 [minus(X, s(Y))] = X 530.18/292.23 >= X 530.18/292.23 = [pred(minus(X, Y))] 530.18/292.23 530.18/292.23 [minus(X, 0())] = X 530.18/292.23 >= X 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [pred(s(X))] = 1 + X 530.18/292.23 > X 530.18/292.23 = [X] 530.18/292.23 530.18/292.23 [le(s(X), s(Y))] = 1 + Y 530.18/292.23 > Y 530.18/292.23 = [le(X, Y)] 530.18/292.23 530.18/292.23 [le(s(X), 0())] = 530.18/292.23 >= 530.18/292.23 = [false()] 530.18/292.23 530.18/292.23 [le(0(), Y)] = Y 530.18/292.23 >= 530.18/292.23 = [true()] 530.18/292.23 530.18/292.23 [gcd(s(X), s(Y))] = 7 + 5*X + X^2 + 4*Y + Y^2 530.18/292.23 > 5*X + 6 + X^2 + 4*Y + Y^2 530.18/292.23 = [if(le(Y, X), s(X), s(Y))] 530.18/292.23 530.18/292.23 [gcd(s(X), 0())] = 4 + 5*X + X^2 530.18/292.23 > 1 + X 530.18/292.23 = [s(X)] 530.18/292.23 530.18/292.23 [gcd(0(), Y)] = 2*Y + Y^2 530.18/292.23 >= 530.18/292.23 = [0()] 530.18/292.23 530.18/292.23 [if(false(), s(X), s(Y))] = 6 + 4*X + X^2 + 4*Y + Y^2 530.18/292.23 > 3*Y + Y^2 + 3 + 4*X + X^2 530.18/292.23 = [gcd(minus(Y, X), s(X))] 530.18/292.23 530.18/292.23 [if(true(), s(X), s(Y))] = 6 + 4*X + X^2 + 4*Y + Y^2 530.18/292.23 > 3*X + X^2 + 3 + 4*Y + Y^2 530.18/292.24 = [gcd(minus(X, Y), s(Y))] 530.18/292.24 530.18/292.24 530.18/292.24 We return to the main proof. 530.18/292.24 530.18/292.24 We are left with following problem, upon which TcT provides the 530.18/292.24 certificate MAYBE. 530.18/292.24 530.18/292.24 Strict Trs: { minus(X, s(Y)) -> pred(minus(X, Y)) } 530.18/292.24 Weak Trs: 530.18/292.24 { minus(X, 0()) -> X 530.18/292.24 , pred(s(X)) -> X 530.18/292.24 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.24 , le(s(X), 0()) -> false() 530.18/292.24 , le(0(), Y) -> true() 530.18/292.24 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.24 , gcd(s(X), 0()) -> s(X) 530.18/292.24 , gcd(0(), Y) -> 0() 530.18/292.24 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.24 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.24 Obligation: 530.18/292.24 runtime complexity 530.18/292.24 Answer: 530.18/292.24 MAYBE 530.18/292.24 530.18/292.24 None of the processors succeeded. 530.18/292.24 530.18/292.24 Details of failed attempt(s): 530.18/292.24 ----------------------------- 530.18/292.24 1) 'empty' failed due to the following reason: 530.18/292.24 530.18/292.24 Empty strict component of the problem is NOT empty. 530.18/292.24 530.18/292.24 2) 'With Problem ...' failed due to the following reason: 530.18/292.24 530.18/292.24 Empty strict component of the problem is NOT empty. 530.18/292.24 530.18/292.24 530.18/292.24 2) 'With Problem ...' failed due to the following reason: 530.18/292.24 530.18/292.24 None of the processors succeeded. 530.18/292.24 530.18/292.24 Details of failed attempt(s): 530.18/292.24 ----------------------------- 530.18/292.24 1) 'empty' failed due to the following reason: 530.18/292.24 530.18/292.24 Empty strict component of the problem is NOT empty. 530.18/292.24 530.18/292.24 2) 'With Problem ...' failed due to the following reason: 530.18/292.24 530.18/292.24 We use the processor 'matrix interpretation of dimension 2' to 530.18/292.24 orient following rules strictly. 530.18/292.24 530.18/292.24 Trs: { le(s(X), s(Y)) -> le(X, Y) } 530.18/292.24 530.18/292.24 The induced complexity on above rules (modulo remaining rules) is 530.18/292.24 YES(?,O(n^2)) . These rules are moved into the corresponding weak 530.18/292.24 component(s). 530.18/292.24 530.18/292.24 Sub-proof: 530.18/292.24 ---------- 530.18/292.24 The following argument positions are usable: 530.18/292.24 Uargs(pred) = {1}, Uargs(gcd) = {1}, Uargs(if) = {1} 530.18/292.24 530.18/292.24 TcT has computed the following constructor-based matrix 530.18/292.24 interpretation satisfying not(EDA). 530.18/292.24 530.18/292.24 [minus](x1, x2) = [1 0] x1 + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 530.18/292.24 [s](x1) = [1 1] x1 + [0] 530.18/292.24 [0 1] [2] 530.18/292.24 530.18/292.24 [pred](x1) = [1 0] x1 + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 530.18/292.24 [0] = [0] 530.18/292.24 [4] 530.18/292.24 530.18/292.24 [le](x1, x2) = [0 1] x2 + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 530.18/292.24 [false] = [0] 530.18/292.24 [0] 530.18/292.24 530.18/292.24 [true] = [0] 530.18/292.24 [0] 530.18/292.24 530.18/292.24 [gcd](x1, x2) = [2 3] x1 + [2 1] x2 + [0] 530.18/292.24 [1 0] [1 0] [4] 530.18/292.24 530.18/292.24 [if](x1, x2, x3) = [1 1] x1 + [2 1] x2 + [2 1] x3 + [0] 530.18/292.24 [0 0] [1 0] [1 0] [4] 530.18/292.24 530.18/292.24 The order satisfies the following ordering constraints: 530.18/292.24 530.18/292.24 [minus(X, s(Y))] = [1 0] X + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 >= [1 0] X + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 = [pred(minus(X, Y))] 530.18/292.24 530.18/292.24 [minus(X, 0())] = [1 0] X + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 >= [1 0] X + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 = [X] 530.18/292.24 530.18/292.24 [pred(s(X))] = [1 1] X + [0] 530.18/292.24 [0 1] [2] 530.18/292.24 >= [1 0] X + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 = [X] 530.18/292.24 530.18/292.24 [le(s(X), s(Y))] = [0 1] Y + [2] 530.18/292.24 [0 1] [2] 530.18/292.24 > [0 1] Y + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 = [le(X, Y)] 530.18/292.24 530.18/292.24 [le(s(X), 0())] = [4] 530.18/292.24 [4] 530.18/292.24 > [0] 530.18/292.24 [0] 530.18/292.24 = [false()] 530.18/292.24 530.18/292.24 [le(0(), Y)] = [0 1] Y + [0] 530.18/292.24 [0 1] [0] 530.18/292.24 >= [0] 530.18/292.24 [0] 530.18/292.24 = [true()] 530.18/292.24 530.18/292.24 [gcd(s(X), s(Y))] = [2 5] X + [2 3] Y + [8] 530.18/292.24 [1 1] [1 1] [4] 530.18/292.24 > [2 5] X + [2 3] Y + [4] 530.18/292.24 [1 1] [1 1] [4] 530.18/292.24 = [if(le(Y, X), s(X), s(Y))] 530.18/292.24 530.18/292.24 [gcd(s(X), 0())] = [2 5] X + [10] 530.18/292.24 [1 1] [4] 530.18/292.24 > [1 1] X + [0] 530.18/292.24 [0 1] [2] 530.18/292.24 = [s(X)] 530.18/292.24 530.18/292.24 [gcd(0(), Y)] = [2 1] Y + [12] 530.18/292.24 [1 0] [4] 530.18/292.24 > [0] 530.18/292.24 [4] 530.18/292.24 = [0()] 530.18/292.24 530.18/292.24 [if(false(), s(X), s(Y))] = [2 3] X + [2 3] Y + [4] 530.18/292.24 [1 1] [1 1] [4] 530.18/292.24 > [2 3] X + [2 3] Y + [2] 530.18/292.24 [1 1] [1 0] [4] 530.18/292.24 = [gcd(minus(Y, X), s(X))] 530.18/292.24 530.18/292.24 [if(true(), s(X), s(Y))] = [2 3] X + [2 3] Y + [4] 530.18/292.24 [1 1] [1 1] [4] 530.18/292.24 > [2 3] X + [2 3] Y + [2] 530.18/292.24 [1 0] [1 1] [4] 530.18/292.24 = [gcd(minus(X, Y), s(Y))] 530.18/292.24 530.18/292.24 530.18/292.24 We return to the main proof. 530.18/292.24 530.18/292.24 We are left with following problem, upon which TcT provides the 530.18/292.24 certificate MAYBE. 530.18/292.24 530.18/292.24 Strict Trs: { minus(X, s(Y)) -> pred(minus(X, Y)) } 530.18/292.24 Weak Trs: 530.18/292.24 { minus(X, 0()) -> X 530.18/292.24 , pred(s(X)) -> X 530.18/292.24 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.24 , le(s(X), 0()) -> false() 530.18/292.24 , le(0(), Y) -> true() 530.18/292.24 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.24 , gcd(s(X), 0()) -> s(X) 530.18/292.24 , gcd(0(), Y) -> 0() 530.18/292.24 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.24 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.24 Obligation: 530.18/292.24 runtime complexity 530.18/292.24 Answer: 530.18/292.24 MAYBE 530.18/292.24 530.18/292.24 None of the processors succeeded. 530.18/292.24 530.18/292.24 Details of failed attempt(s): 530.18/292.24 ----------------------------- 530.18/292.24 1) 'empty' failed due to the following reason: 530.18/292.24 530.18/292.24 Empty strict component of the problem is NOT empty. 530.18/292.24 530.18/292.24 2) 'With Problem ...' failed due to the following reason: 530.18/292.24 530.18/292.24 None of the processors succeeded. 530.18/292.24 530.18/292.24 Details of failed attempt(s): 530.18/292.24 ----------------------------- 530.18/292.24 1) 'empty' failed due to the following reason: 530.18/292.24 530.18/292.24 Empty strict component of the problem is NOT empty. 530.18/292.24 530.18/292.24 2) 'With Problem ...' failed due to the following reason: 530.18/292.24 530.18/292.24 Empty strict component of the problem is NOT empty. 530.18/292.24 530.18/292.24 530.18/292.24 530.18/292.24 530.18/292.24 530.18/292.24 530.18/292.24 530.18/292.24 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 530.18/292.24 failed due to the following reason: 530.18/292.24 530.18/292.24 None of the processors succeeded. 530.18/292.24 530.18/292.24 Details of failed attempt(s): 530.18/292.24 ----------------------------- 530.18/292.24 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 530.18/292.24 failed due to the following reason: 530.18/292.24 530.18/292.24 match-boundness of the problem could not be verified. 530.18/292.24 530.18/292.24 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 530.18/292.24 failed due to the following reason: 530.18/292.24 530.18/292.24 match-boundness of the problem could not be verified. 530.18/292.24 530.18/292.24 530.18/292.24 3) 'Best' failed due to the following reason: 530.18/292.24 530.18/292.24 None of the processors succeeded. 530.18/292.24 530.18/292.24 Details of failed attempt(s): 530.18/292.24 ----------------------------- 530.18/292.24 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 530.18/292.24 following reason: 530.18/292.24 530.18/292.24 The processor is inapplicable, reason: 530.18/292.24 Processor only applicable for innermost runtime complexity analysis 530.18/292.24 530.18/292.24 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 530.18/292.24 to the following reason: 530.18/292.24 530.18/292.24 The processor is inapplicable, reason: 530.18/292.24 Processor only applicable for innermost runtime complexity analysis 530.18/292.24 530.18/292.24 530.18/292.24 530.18/292.24 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 530.18/292.24 the following reason: 530.18/292.24 530.18/292.24 We add the following weak dependency pairs: 530.18/292.24 530.18/292.24 Strict DPs: 530.18/292.24 { minus^#(X, s(Y)) -> c_1(pred^#(minus(X, Y))) 530.18/292.24 , minus^#(X, 0()) -> c_2(X) 530.18/292.24 , pred^#(s(X)) -> c_3(X) 530.18/292.24 , le^#(s(X), s(Y)) -> c_4(le^#(X, Y)) 530.18/292.24 , le^#(s(X), 0()) -> c_5() 530.18/292.24 , le^#(0(), Y) -> c_6() 530.18/292.24 , gcd^#(s(X), s(Y)) -> c_7(if^#(le(Y, X), s(X), s(Y))) 530.18/292.24 , gcd^#(s(X), 0()) -> c_8(X) 530.18/292.24 , gcd^#(0(), Y) -> c_9() 530.18/292.24 , if^#(false(), s(X), s(Y)) -> c_10(gcd^#(minus(Y, X), s(X))) 530.18/292.24 , if^#(true(), s(X), s(Y)) -> c_11(gcd^#(minus(X, Y), s(Y))) } 530.18/292.24 530.18/292.24 and mark the set of starting terms. 530.18/292.24 530.18/292.24 We are left with following problem, upon which TcT provides the 530.18/292.24 certificate MAYBE. 530.18/292.24 530.18/292.24 Strict DPs: 530.18/292.24 { minus^#(X, s(Y)) -> c_1(pred^#(minus(X, Y))) 530.18/292.24 , minus^#(X, 0()) -> c_2(X) 530.18/292.24 , pred^#(s(X)) -> c_3(X) 530.18/292.24 , le^#(s(X), s(Y)) -> c_4(le^#(X, Y)) 530.18/292.24 , le^#(s(X), 0()) -> c_5() 530.18/292.24 , le^#(0(), Y) -> c_6() 530.18/292.24 , gcd^#(s(X), s(Y)) -> c_7(if^#(le(Y, X), s(X), s(Y))) 530.18/292.24 , gcd^#(s(X), 0()) -> c_8(X) 530.18/292.24 , gcd^#(0(), Y) -> c_9() 530.18/292.24 , if^#(false(), s(X), s(Y)) -> c_10(gcd^#(minus(Y, X), s(X))) 530.18/292.24 , if^#(true(), s(X), s(Y)) -> c_11(gcd^#(minus(X, Y), s(Y))) } 530.18/292.24 Strict Trs: 530.18/292.24 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.24 , minus(X, 0()) -> X 530.18/292.24 , pred(s(X)) -> X 530.18/292.24 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.24 , le(s(X), 0()) -> false() 530.18/292.24 , le(0(), Y) -> true() 530.18/292.24 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.24 , gcd(s(X), 0()) -> s(X) 530.18/292.24 , gcd(0(), Y) -> 0() 530.18/292.24 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.24 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.24 Obligation: 530.18/292.24 runtime complexity 530.18/292.24 Answer: 530.18/292.24 MAYBE 530.18/292.24 530.18/292.24 We estimate the number of application of {5,6,9} by applications of 530.18/292.24 Pre({5,6,9}) = {2,3,4,8,10,11}. Here rules are labeled as follows: 530.18/292.24 530.18/292.24 DPs: 530.18/292.24 { 1: minus^#(X, s(Y)) -> c_1(pred^#(minus(X, Y))) 530.18/292.24 , 2: minus^#(X, 0()) -> c_2(X) 530.18/292.24 , 3: pred^#(s(X)) -> c_3(X) 530.18/292.24 , 4: le^#(s(X), s(Y)) -> c_4(le^#(X, Y)) 530.18/292.24 , 5: le^#(s(X), 0()) -> c_5() 530.18/292.24 , 6: le^#(0(), Y) -> c_6() 530.18/292.24 , 7: gcd^#(s(X), s(Y)) -> c_7(if^#(le(Y, X), s(X), s(Y))) 530.18/292.24 , 8: gcd^#(s(X), 0()) -> c_8(X) 530.18/292.24 , 9: gcd^#(0(), Y) -> c_9() 530.18/292.24 , 10: if^#(false(), s(X), s(Y)) -> c_10(gcd^#(minus(Y, X), s(X))) 530.18/292.24 , 11: if^#(true(), s(X), s(Y)) -> c_11(gcd^#(minus(X, Y), s(Y))) } 530.18/292.24 530.18/292.24 We are left with following problem, upon which TcT provides the 530.18/292.24 certificate MAYBE. 530.18/292.24 530.18/292.24 Strict DPs: 530.18/292.24 { minus^#(X, s(Y)) -> c_1(pred^#(minus(X, Y))) 530.18/292.24 , minus^#(X, 0()) -> c_2(X) 530.18/292.24 , pred^#(s(X)) -> c_3(X) 530.18/292.24 , le^#(s(X), s(Y)) -> c_4(le^#(X, Y)) 530.18/292.24 , gcd^#(s(X), s(Y)) -> c_7(if^#(le(Y, X), s(X), s(Y))) 530.18/292.24 , gcd^#(s(X), 0()) -> c_8(X) 530.18/292.24 , if^#(false(), s(X), s(Y)) -> c_10(gcd^#(minus(Y, X), s(X))) 530.18/292.24 , if^#(true(), s(X), s(Y)) -> c_11(gcd^#(minus(X, Y), s(Y))) } 530.18/292.24 Strict Trs: 530.18/292.24 { minus(X, s(Y)) -> pred(minus(X, Y)) 530.18/292.24 , minus(X, 0()) -> X 530.18/292.24 , pred(s(X)) -> X 530.18/292.24 , le(s(X), s(Y)) -> le(X, Y) 530.18/292.24 , le(s(X), 0()) -> false() 530.18/292.24 , le(0(), Y) -> true() 530.18/292.24 , gcd(s(X), s(Y)) -> if(le(Y, X), s(X), s(Y)) 530.18/292.24 , gcd(s(X), 0()) -> s(X) 530.18/292.24 , gcd(0(), Y) -> 0() 530.18/292.24 , if(false(), s(X), s(Y)) -> gcd(minus(Y, X), s(X)) 530.18/292.24 , if(true(), s(X), s(Y)) -> gcd(minus(X, Y), s(Y)) } 530.18/292.24 Weak DPs: 530.18/292.24 { le^#(s(X), 0()) -> c_5() 530.18/292.24 , le^#(0(), Y) -> c_6() 530.18/292.24 , gcd^#(0(), Y) -> c_9() } 530.18/292.24 Obligation: 530.18/292.24 runtime complexity 530.18/292.24 Answer: 530.18/292.24 MAYBE 530.18/292.24 530.18/292.24 Empty strict component of the problem is NOT empty. 530.18/292.24 530.18/292.24 530.18/292.24 Arrrr.. 530.53/292.55 EOF