MAYBE Time: 32.187725 TRS: { ge(x, 0()) -> true(), ge(0(), s y) -> false(), ge(s x, s y) -> ge(x, y), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), id_inc x -> x, id_inc x -> s x, div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z), quot(x, y) -> div(x, y, 0()), if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z), if(true(), false(), x, y, z) -> z, if(false(), b, x, y, z) -> div_by_zero()} DP: DP: { ge#(s x, s y) -> ge#(x, y), minus#(s x, s y) -> minus#(x, y), div#(x, y, z) -> ge#(x, y), div#(x, y, z) -> ge#(y, s 0()), div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), quot#(x, y) -> div#(x, y, 0()), if#(true(), true(), x, y, z) -> minus#(x, y), if#(true(), true(), x, y, z) -> id_inc# z, if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z)} TRS: { ge(x, 0()) -> true(), ge(0(), s y) -> false(), ge(s x, s y) -> ge(x, y), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), id_inc x -> x, id_inc x -> s x, div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z), quot(x, y) -> div(x, y, 0()), if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z), if(true(), false(), x, y, z) -> z, if(false(), b, x, y, z) -> div_by_zero()} EDG: {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (if#(true(), true(), x, y, z) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z)) (div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> id_inc# z) (div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> minus#(x, y)) (if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z), div#(x, y, z) -> ge#(x, y)) (if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z), div#(x, y, z) -> ge#(y, s 0())) (if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z), div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z)) (div#(x, y, z) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y)) (div#(x, y, z) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (quot#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> ge#(x, y)) (quot#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> ge#(y, s 0())) (quot#(x, y) -> div#(x, y, 0()), div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z))} STATUS: arrows: 0.827160 SCCS (3): Scc: { div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z)} Scc: {minus#(s x, s y) -> minus#(x, y)} Scc: {ge#(s x, s y) -> ge#(x, y)} SCC (2): Strict: { div#(x, y, z) -> if#(ge(y, s 0()), ge(x, y), x, y, z), if#(true(), true(), x, y, z) -> div#(minus(x, y), y, id_inc z)} Weak: { ge(x, 0()) -> true(), ge(0(), s y) -> false(), ge(s x, s y) -> ge(x, y), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), id_inc x -> x, id_inc x -> s x, div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z), quot(x, y) -> div(x, y, 0()), if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z), if(true(), false(), x, y, z) -> z, if(false(), b, x, y, z) -> div_by_zero()} Fail SCC (1): Strict: {minus#(s x, s y) -> minus#(x, y)} Weak: { ge(x, 0()) -> true(), ge(0(), s y) -> false(), ge(s x, s y) -> ge(x, y), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), id_inc x -> x, id_inc x -> s x, div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z), quot(x, y) -> div(x, y, 0()), if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z), if(true(), false(), x, y, z) -> z, if(false(), b, x, y, z) -> div_by_zero()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3, x4) = 0, [div](x0, x1, x2) = x0 + 1, [ge](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + x1 + 1, [quot](x0, x1) = 0, [s](x0) = x0 + 1, [id_inc](x0) = 0, [true] = 0, [0] = 1, [false] = 0, [div_by_zero] = 0, [minus#](x0, x1) = x0 Strict: minus#(s x, s y) -> minus#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: if(false(), b, x, y, z) -> div_by_zero() 0 + 0x + 0y + 0z + 0b >= 0 if(true(), false(), x, y, z) -> z 0 + 0x + 0y + 0z >= 1z if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z quot(x, y) -> div(x, y, 0()) 0 + 0x + 0y >= 2 + 0x + 0y div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z) 1 + 0x + 0y + 1z >= 0 + 0x + 0y + 0z id_inc x -> s x 0 + 0x >= 1 + 1x id_inc x -> x 0 + 0x >= 1x minus(s x, s y) -> minus(x, y) 3 + 1x + 1y >= 1 + 1x + 1y minus(0(), y) -> 0() 2 + 1y >= 1 minus(x, 0()) -> x 2 + 1x >= 1x ge(s x, s y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0(), s y) -> false() 2 + 1y >= 0 ge(x, 0()) -> true() 2 + 0x >= 0 Qed SCC (1): Strict: {ge#(s x, s y) -> ge#(x, y)} Weak: { ge(x, 0()) -> true(), ge(0(), s y) -> false(), ge(s x, s y) -> ge(x, y), minus(x, 0()) -> x, minus(0(), y) -> 0(), minus(s x, s y) -> minus(x, y), id_inc x -> x, id_inc x -> s x, div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z), quot(x, y) -> div(x, y, 0()), if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z), if(true(), false(), x, y, z) -> z, if(false(), b, x, y, z) -> div_by_zero()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3, x4) = 0, [div](x0, x1, x2) = x0 + 1, [ge](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + x1 + 1, [quot](x0, x1) = 0, [s](x0) = x0 + 1, [id_inc](x0) = 0, [true] = 0, [0] = 1, [false] = 0, [div_by_zero] = 0, [ge#](x0, x1) = x0 Strict: ge#(s x, s y) -> ge#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: if(false(), b, x, y, z) -> div_by_zero() 0 + 0x + 0y + 0z + 0b >= 0 if(true(), false(), x, y, z) -> z 0 + 0x + 0y + 0z >= 1z if(true(), true(), x, y, z) -> div(minus(x, y), y, id_inc z) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z quot(x, y) -> div(x, y, 0()) 0 + 0x + 0y >= 2 + 0x + 0y div(x, y, z) -> if(ge(y, s 0()), ge(x, y), x, y, z) 1 + 0x + 0y + 1z >= 0 + 0x + 0y + 0z id_inc x -> s x 0 + 0x >= 1 + 1x id_inc x -> x 0 + 0x >= 1x minus(s x, s y) -> minus(x, y) 3 + 1x + 1y >= 1 + 1x + 1y minus(0(), y) -> 0() 2 + 1y >= 1 minus(x, 0()) -> x 2 + 1x >= 1x ge(s x, s y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0(), s y) -> false() 2 + 1y >= 0 ge(x, 0()) -> true() 2 + 0x >= 0 Qed