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