Time: 5.119950
TRS:
{Cond_b14(true(), sv14_14, sv23_37, sv24_38) -> b15(sv14_14, sv23_37, sv24_38),
and(true(), true()) -> true(),
and(true(), false()) -> false(),
and(false(), true()) -> false(),
and(false(), false()) -> false(),
greatereq_int(pos x, pos 0()) -> true(),
greatereq_int(pos x, neg y) -> true(),
greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
greatereq_int(pos 0(), pos s y) -> false(),
greatereq_int(neg x, pos s y) -> false(),
greatereq_int(neg s x, pos 0()) -> false(),
greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
greatereq_int(neg s x, neg 0()) -> false(),
greatereq_int(neg 0(), pos 0()) -> true(),
greatereq_int(neg 0(), neg y) -> true(),
less_int(pos s x, pos s y) -> less_int(pos x, pos y),
less_int(pos s x, pos 0()) -> false(),
less_int(pos s x, neg s y) -> false(),
less_int(pos s x, neg 0()) -> false(),
less_int(pos 0(), pos s y) -> true(),
less_int(pos 0(), pos 0()) -> false(),
less_int(pos 0(), neg s y) -> false(),
less_int(pos 0(), neg 0()) -> false(),
less_int(neg s x, pos s y) -> true(),
less_int(neg s x, pos 0()) -> true(),
less_int(neg s x, neg s y) -> less_int(neg x, neg y),
less_int(neg s x, neg 0()) -> true(),
less_int(neg 0(), pos s y) -> true(),
less_int(neg 0(), pos 0()) -> false(),
less_int(neg 0(), neg s y) -> false(),
less_int(neg 0(), neg 0()) -> false(),
b14(sv14_14, sv23_37, sv24_38) -> Cond_b14(and(greatereq_int(sv23_37, sv14_14), and(less_int(pos s 0(), sv14_14), and(true(), and(less_int(pos 0(), sv24_38), less_int(pos s 0(), sv23_37))))), sv14_14, sv23_37, sv24_38),
b15(sv14_14, sv23_37, sv24_38) -> b10(sv14_14, minus_int(sv23_37, sv14_14), plus_int(pos s 0(), sv24_38)),
b10(sv14_14, sv23_37, sv24_38) -> b14(sv14_14, sv23_37, sv24_38),
minus_int(pos x, pos y) -> minus_nat(x, y),
minus_int(pos x, neg y) -> pos plus_nat(x, y),
minus_int(neg x, pos y) -> neg plus_nat(x, y),
minus_int(neg x, neg y) -> minus_nat(y, x),
plus_int(pos x, pos y) -> pos plus_nat(x, y),
plus_int(pos x, neg y) -> minus_nat(x, y),
plus_int(neg x, pos y) -> minus_nat(y, x),
plus_int(neg x, neg y) -> neg plus_nat(x, y),
minus_nat(s x, s y) -> minus_nat(x, y),
minus_nat(s x, 0()) -> pos s x,
minus_nat(0(), s y) -> neg s y,
minus_nat(0(), 0()) -> pos 0(),
plus_nat(s x, y) -> s plus_nat(x, y),
plus_nat(0(), x) -> x}
SRS: We consider a TRS.
Trs:
{Cond_b14(true(), sv14_14, sv23_37, sv24_38) -> b15(sv14_14, sv23_37, sv24_38),
and(true(), true()) -> true(),
and(true(), false()) -> false(),
and(false(), true()) -> false(),
and(false(), false()) -> false(),
greatereq_int(pos x, pos 0()) -> true(),
greatereq_int(pos x, neg y) -> true(),
greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
greatereq_int(pos 0(), pos s y) -> false(),
greatereq_int(neg x, pos s y) -> false(),
greatereq_int(neg s x, pos 0()) -> false(),
greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
greatereq_int(neg s x, neg 0()) -> false(),
greatereq_int(neg 0(), pos 0()) -> true(),
greatereq_int(neg 0(), neg y) -> true(),
less_int(pos s x, pos s y) -> less_int(pos x, pos y),
less_int(pos s x, pos 0()) -> false(),
less_int(pos s x, neg s y) -> false(),
less_int(pos s x, neg 0()) -> false(),
less_int(pos 0(), pos s y) -> true(),
less_int(pos 0(), pos 0()) -> false(),
less_int(pos 0(), neg s y) -> false(),
less_int(pos 0(), neg 0()) -> false(),
less_int(neg s x, pos s y) -> true(),
less_int(neg s x, pos 0()) -> true(),
less_int(neg s x, neg s y) -> less_int(neg x, neg y),
less_int(neg s x, neg 0()) -> true(),
less_int(neg 0(), pos s y) -> true(),
less_int(neg 0(), pos 0()) -> false(),
less_int(neg 0(), neg s y) -> false(),
less_int(neg 0(), neg 0()) -> false(),
b14(sv14_14, sv23_37, sv24_38) -> Cond_b14(and(greatereq_int(sv23_37, sv14_14), and(less_int(pos s 0(), sv14_14), and(true(), and(less_int(pos 0(), sv24_38), less_int(pos s 0(), sv23_37))))), sv14_14, sv23_37, sv24_38),
b15(sv14_14, sv23_37, sv24_38) -> b10(sv14_14, minus_int(sv23_37, sv14_14), plus_int(pos s 0(), sv24_38)),
b10(sv14_14, sv23_37, sv24_38) -> b14(sv14_14, sv23_37, sv24_38),
minus_int(pos x, pos y) -> minus_nat(x, y),
minus_int(pos x, neg y) -> pos plus_nat(x, y),
minus_int(neg x, pos y) -> neg plus_nat(x, y),
minus_int(neg x, neg y) -> minus_nat(y, x),
plus_int(pos x, pos y) -> pos plus_nat(x, y),
plus_int(pos x, neg y) -> minus_nat(x, y),
plus_int(neg x, pos y) -> minus_nat(y, x),
plus_int(neg x, neg y) -> neg plus_nat(x, y),
minus_nat(s x, s y) -> minus_nat(x, y),
minus_nat(s x, 0()) -> pos s x,
minus_nat(0(), s y) -> neg s y,
minus_nat(0(), 0()) -> pos 0(),
plus_nat(s x, y) -> s plus_nat(x, y),
plus_nat(0(), x) -> x}
Fail