YES Time: 0.276473 TRS: { -(x, 0()) -> x, -(0(), s y) -> 0(), -(s x, s y) -> -(x, y), lt(x, 0()) -> false(), lt(0(), s y) -> true(), lt(s x, s y) -> lt(x, y), if(false(), x, y) -> y, if(true(), x, y) -> x, div(x, 0()) -> 0(), div(0(), y) -> 0(), div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))} DP: DP: { -#(s x, s y) -> -#(x, y), lt#(s x, s y) -> lt#(x, y), div#(s x, s y) -> -#(x, y), div#(s x, s y) -> lt#(x, y), div#(s x, s y) -> if#(lt(x, y), 0(), s div(-(x, y), s y)), div#(s x, s y) -> div#(-(x, y), s y)} TRS: { -(x, 0()) -> x, -(0(), s y) -> 0(), -(s x, s y) -> -(x, y), lt(x, 0()) -> false(), lt(0(), s y) -> true(), lt(s x, s y) -> lt(x, y), if(false(), x, y) -> y, if(true(), x, y) -> x, div(x, 0()) -> 0(), div(0(), y) -> 0(), div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))} UR: { -(x, 0()) -> x, -(0(), s y) -> 0(), -(s x, s y) -> -(x, y), lt(x, 0()) -> false(), lt(0(), s y) -> true(), lt(s x, s y) -> lt(x, y), if(false(), x, y) -> y, if(true(), x, y) -> x, div(0(), y) -> 0(), div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y)), a(z, w) -> z, a(z, w) -> w} EDG: {(lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y)) (div#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y)) (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> -#(x, y)) (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> lt#(x, y)) (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> if#(lt(x, y), 0(), s div(-(x, y), s y))) (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> div#(-(x, y), s y)) (div#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))} STATUS: arrows: 0.777778 SCCS (3): Scc: {div#(s x, s y) -> div#(-(x, y), s y)} Scc: {lt#(s x, s y) -> lt#(x, y)} Scc: {-#(s x, s y) -> -#(x, y)} SCC (1): Strict: {div#(s x, s y) -> div#(-(x, y), s y)} Weak: { -(x, 0()) -> x, -(0(), s y) -> 0(), -(s x, s y) -> -(x, y), lt(x, 0()) -> false(), lt(0(), s y) -> true(), lt(s x, s y) -> lt(x, y), if(false(), x, y) -> y, if(true(), x, y) -> x, div(x, 0()) -> 0(), div(0(), y) -> 0(), div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [-](x0, x1) = x0, [lt](x0, x1) = 0, [div](x0, x1) = 0, [s](x0) = x0 + 1, [0] = 0, [false] = 1, [true] = 1, [div#](x0, x1) = x0 + 1 Strict: div#(s x, s y) -> div#(-(x, y), s y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y)) 0 + 0x + 0y >= 1 + 0x + 0y div(0(), y) -> 0() 0 + 0y >= 0 div(x, 0()) -> 0() 0 + 0x >= 0 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y lt(s x, s y) -> lt(x, y) 0 + 0x + 0y >= 0 + 0x + 0y lt(0(), s y) -> true() 0 + 0y >= 1 lt(x, 0()) -> false() 0 + 0x >= 1 -(s x, s y) -> -(x, y) 1 + 1x + 0y >= 0 + 1x + 0y -(0(), s y) -> 0() 0 + 0y >= 0 -(x, 0()) -> x 0 + 1x >= 1x Qed SCC (1): Strict: {lt#(s x, s y) -> lt#(x, y)} Weak: { -(x, 0()) -> x, -(0(), s y) -> 0(), -(s x, s y) -> -(x, y), lt(x, 0()) -> false(), lt(0(), s y) -> true(), lt(s x, s y) -> lt(x, y), if(false(), x, y) -> y, if(true(), x, y) -> x, div(x, 0()) -> 0(), div(0(), y) -> 0(), div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [-](x0, x1) = x0 + 1, [lt](x0, x1) = x0 + 1, [div](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [false] = 1, [true] = 1, [lt#](x0, x1) = x0 Strict: lt#(s x, s y) -> lt#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y)) 2 + 0x + 1y >= 2 + 0x + 1y div(0(), y) -> 0() 1 + 1y >= 1 div(x, 0()) -> 0() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y lt(s x, s y) -> lt(x, y) 2 + 0x + 1y >= 1 + 0x + 1y lt(0(), s y) -> true() 2 + 1y >= 1 lt(x, 0()) -> false() 2 + 0x >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(0(), s y) -> 0() 2 + 1y >= 1 -(x, 0()) -> x 2 + 0x >= 1x Qed SCC (1): Strict: {-#(s x, s y) -> -#(x, y)} Weak: { -(x, 0()) -> x, -(0(), s y) -> 0(), -(s x, s y) -> -(x, y), lt(x, 0()) -> false(), lt(0(), s y) -> true(), lt(s x, s y) -> lt(x, y), if(false(), x, y) -> y, if(true(), x, y) -> x, div(x, 0()) -> 0(), div(0(), y) -> 0(), div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [-](x0, x1) = x0 + 1, [lt](x0, x1) = x0 + 1, [div](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [false] = 1, [true] = 1, [-#](x0, x1) = x0 Strict: -#(s x, s y) -> -#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y)) 2 + 0x + 1y >= 2 + 0x + 1y div(0(), y) -> 0() 1 + 1y >= 1 div(x, 0()) -> 0() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y lt(s x, s y) -> lt(x, y) 2 + 0x + 1y >= 1 + 0x + 1y lt(0(), s y) -> true() 2 + 1y >= 1 lt(x, 0()) -> false() 2 + 0x >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(0(), s y) -> 0() 2 + 1y >= 1 -(x, 0()) -> x 2 + 0x >= 1x Qed