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