YES Time: 0.056548 TRS: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), log s 0() -> 0(), log s s x -> s log s quot(x, s s 0())} DP: DP: { le#(s x, s y) -> le#(x, y), minus#(s x, y) -> le#(s x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y), quot#(s x, s y) -> minus#(x, y), quot#(s x, s y) -> quot#(minus(x, y), s y), log# s s x -> quot#(x, s s 0()), log# s s x -> log# s quot(x, s s 0())} TRS: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), log s 0() -> 0(), log s s x -> s log s quot(x, s s 0())} UR: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), a(z, w) -> z, a(z, w) -> w} EDG: {(log# s s x -> log# s quot(x, s s 0()), log# s s x -> log# s quot(x, s s 0())) (log# s s x -> log# s quot(x, s s 0()), log# s s x -> quot#(x, s s 0())) (minus#(s x, y) -> le#(s x, y), le#(s x, s y) -> le#(x, y)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (quot#(s x, s y) -> minus#(x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, y)) (quot#(s x, s y) -> minus#(x, y), minus#(s x, y) -> le#(s x, y)) (if_minus#(false(), s x, y) -> minus#(x, y), minus#(s x, y) -> le#(s x, y)) (if_minus#(false(), s x, y) -> minus#(x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, y)) (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y)) (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y)) (minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y)) (log# s s x -> quot#(x, s s 0()), quot#(s x, s y) -> minus#(x, y)) (log# s s x -> quot#(x, s s 0()), quot#(s x, s y) -> quot#(minus(x, y), s y))} STATUS: arrows: 0.796875 SCCS (4): Scc: {log# s s x -> log# s quot(x, s s 0())} Scc: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Scc: { minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y)} Scc: {le#(s x, s y) -> le#(x, y)} SCC (1): Strict: {log# s s x -> log# s quot(x, s s 0())} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), log s 0() -> 0(), log s s x -> s log s quot(x, s s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_minus](x0, x1, x2) = x0, [le](x0, x1) = x0 + 1, [minus](x0, x1) = x0, [quot](x0, x1) = x0, [s](x0) = x0 + 1, [log](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [log#](x0) = x0 + 1 Strict: log# s s x -> log# s quot(x, s s 0()) 3 + 1x >= 2 + 1x Weak: log s s x -> s log s quot(x, s s 0()) 3 + 1x >= 3 + 1x log s 0() -> 0() 2 >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 1 + 0y + 1x >= 1 + 0y + 1x quot(0(), s y) -> 0() 0 + 0y >= 0 if_minus(false(), s x, y) -> s minus(x, y) 1 + 0y + 1x >= 1 + 0y + 1x if_minus(true(), s x, y) -> 0() 1 + 0y + 1x >= 0 minus(s x, y) -> if_minus(le(s x, y), s x, y) 1 + 0y + 1x >= 1 + 0y + 1x minus(0(), y) -> 0() 0 + 0y >= 0 le(s x, s y) -> le(x, y) 2 + 0y + 1x >= 1 + 0y + 1x le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 1 + 0y >= 0 Qed SCC (1): Strict: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), log s 0() -> 0(), log s s x -> s log s quot(x, s s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_minus](x0, x1, x2) = x0, [le](x0, x1) = x0 + 1, [minus](x0, x1) = x0, [quot](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [log](x0) = x0, [true] = 0, [0] = 1, [false] = 0, [quot#](x0, x1) = x0 + 1 Strict: quot#(s x, s y) -> quot#(minus(x, y), s y) 2 + 0y + 1x >= 1 + 0y + 1x Weak: log s s x -> s log s quot(x, s s 0()) 2 + 1x >= 6 + 0x log s 0() -> 0() 2 >= 1 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 1y + 0x >= 3 + 1y + 0x quot(0(), s y) -> 0() 2 + 1y >= 1 if_minus(false(), s x, y) -> s minus(x, y) 1 + 0y + 1x >= 1 + 0y + 1x if_minus(true(), s x, y) -> 0() 1 + 0y + 1x >= 1 minus(s x, y) -> if_minus(le(s x, y), s x, y) 1 + 0y + 1x >= 1 + 0y + 1x minus(0(), y) -> 0() 1 + 0y >= 1 le(s x, s y) -> le(x, y) 2 + 0y + 1x >= 1 + 0y + 1x le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 Qed SCC (2): Strict: { minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), log s 0() -> 0(), log s s x -> s log s quot(x, s s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_minus](x0, x1, x2) = x0, [le](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0, [s](x0) = x0 + 1, [log](x0) = 0, [true] = 0, [0] = 1, [false] = 0, [if_minus#](x0, x1, x2) = x0, [minus#](x0, x1) = x0 Strict: if_minus#(false(), s x, y) -> minus#(x, y) 1 + 0y + 1x >= 0 + 0y + 1x minus#(s x, y) -> if_minus#(le(s x, y), s x, y) 1 + 0y + 1x >= 1 + 0y + 1x Weak: log s s x -> s log s quot(x, s s 0()) 0 + 0x >= 1 + 0x log s 0() -> 0() 0 >= 1 quot(s x, s y) -> s quot(minus(x, y), s y) 1 + 1y + 0x >= 2 + 1y + 0x quot(0(), s y) -> 0() 1 + 1y >= 1 if_minus(false(), s x, y) -> s minus(x, y) 0 + 0y + 0x >= 2 + 0y + 1x if_minus(true(), s x, y) -> 0() 0 + 0y + 0x >= 1 minus(s x, y) -> if_minus(le(s x, y), s x, y) 2 + 0y + 1x >= 2 + 0y + 1x minus(0(), y) -> 0() 2 + 0y >= 1 le(s x, s y) -> le(x, y) 2 + 0y + 1x >= 1 + 0y + 1x le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 SCCS (0): SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), log s 0() -> 0(), log s s x -> s log s quot(x, s s 0())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_minus](x0, x1, x2) = x0, [le](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [log](x0) = x0, [true] = 0, [0] = 1, [false] = 0, [le#](x0, x1) = x0 + 1 Strict: le#(s x, s y) -> le#(x, y) 2 + 0y + 1x >= 1 + 0y + 1x Weak: log s s x -> s log s quot(x, s s 0()) 2 + 1x >= 6 + 0x log s 0() -> 0() 2 >= 1 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 1y + 0x >= 3 + 1y + 0x quot(0(), s y) -> 0() 2 + 1y >= 1 if_minus(false(), s x, y) -> s minus(x, y) 0 + 0y + 0x >= 2 + 0y + 1x if_minus(true(), s x, y) -> 0() 0 + 0y + 0x >= 1 minus(s x, y) -> if_minus(le(s x, y), s x, y) 2 + 0y + 1x >= 2 + 0y + 1x minus(0(), y) -> 0() 2 + 0y >= 1 le(s x, s y) -> le(x, y) 2 + 0y + 1x >= 1 + 0y + 1x le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 Qed