MAYBE Time: 0.036342 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, if(true(), true(), x, y) -> id_inc div(minus(x, y), y), if(true(), false(), x, y) -> 0(), if(false(), b, x, y) -> div_by_zero(), div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)} DP: DP: { ge#(s x, s y) -> ge#(x, y), minus#(s x, s y) -> minus#(x, y), if#(true(), true(), x, y) -> minus#(x, y), if#(true(), true(), x, y) -> id_inc# div(minus(x, y), y), if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(x, y), div#(x, y) -> ge#(y, s 0()), div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y)} 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, if(true(), true(), x, y) -> id_inc div(minus(x, y), y), if(true(), false(), x, y) -> 0(), if(false(), b, x, y) -> div_by_zero(), div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)} EDG: {(if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y)) (if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s 0())) (if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(x, y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (div#(x, y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> minus#(x, y)) (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> id_inc# div(minus(x, y), y)) (div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y), if#(true(), true(), x, y) -> div#(minus(x, y), y)) (if#(true(), true(), x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (div#(x, y) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y))} STATUS: arrows: 0.828125 SCCS (3): Scc: {if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> if#(ge(y, s 0()), ge(x, y), x, y)} Scc: {minus#(s x, s y) -> minus#(x, y)} Scc: {ge#(s x, s y) -> ge#(x, y)} SCC (2): Strict: {if#(true(), true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> if#(ge(y, s 0()), ge(x, y), 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, if(true(), true(), x, y) -> id_inc div(minus(x, y), y), if(true(), false(), x, y) -> 0(), if(false(), b, x, y) -> div_by_zero(), div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)} 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, if(true(), true(), x, y) -> id_inc div(minus(x, y), y), if(true(), false(), x, y) -> 0(), if(false(), b, x, y) -> div_by_zero(), div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3) = x0 + 1, [ge](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + x1 + 1, [div](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [id_inc](x0) = x0, [true] = 1, [0] = 1, [false] = 1, [div_by_zero] = 0, [minus#](x0, x1) = x0 Strict: minus#(s x, s y) -> minus#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y) 1 + 1x + 0y >= 4 + 0x + 0y if(false(), b, x, y) -> div_by_zero() 2 + 0x + 0y + 0b >= 0 if(true(), false(), x, y) -> 0() 2 + 0x + 0y >= 1 if(true(), true(), x, y) -> id_inc div(minus(x, y), y) 2 + 0x + 0y >= 2 + 1x + 1y id_inc x -> s x 0 + 1x >= 1 + 1x id_inc x -> x 0 + 1x >= 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 >= 1 ge(x, 0()) -> true() 2 + 0x >= 1 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, if(true(), true(), x, y) -> id_inc div(minus(x, y), y), if(true(), false(), x, y) -> 0(), if(false(), b, x, y) -> div_by_zero(), div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3) = x0 + 1, [ge](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + x1 + 1, [div](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [id_inc](x0) = x0, [true] = 1, [0] = 1, [false] = 1, [div_by_zero] = 0, [ge#](x0, x1) = x0 Strict: ge#(s x, s y) -> ge#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: div(x, y) -> if(ge(y, s 0()), ge(x, y), x, y) 1 + 1x + 0y >= 4 + 0x + 0y if(false(), b, x, y) -> div_by_zero() 2 + 0x + 0y + 0b >= 0 if(true(), false(), x, y) -> 0() 2 + 0x + 0y >= 1 if(true(), true(), x, y) -> id_inc div(minus(x, y), y) 2 + 0x + 0y >= 2 + 1x + 1y id_inc x -> s x 0 + 1x >= 1 + 1x id_inc x -> x 0 + 1x >= 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 >= 1 ge(x, 0()) -> true() 2 + 0x >= 1 Qed