Time: 5.817989
TRS:
{
Cond_eval_511(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
greater_int(pos 0(), pos 0()) -> false(),
greater_int(pos 0(), pos s y) -> false(),
greater_int(pos 0(), neg 0()) -> false(),
greater_int(pos 0(), neg s y) -> true(),
greater_int(pos s x, pos 0()) -> true(),
greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
greater_int(pos s x, neg 0()) -> true(),
greater_int(pos s x, neg s y) -> true(),
greater_int(neg 0(), pos 0()) -> false(),
greater_int(neg 0(), pos s y) -> false(),
greater_int(neg 0(), neg 0()) -> false(),
greater_int(neg 0(), neg s y) -> true(),
greater_int(neg s x, pos 0()) -> false(),
greater_int(neg s x, pos s y) -> false(),
greater_int(neg s x, neg 0()) -> false(),
greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_511(greater_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_51(lesseq_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_52(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_53(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_51(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_52(n, i, j, k, l, t, h, m, p, q, r, up),
eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_5(not up, n, i, j, k, l, t, h, m, p, q, r, up),
eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_52(up, n, i, j, k, l, t, h, m, p, q, r, up),
eval_4(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_5(n, i, j, k, l, t, h, n, p, q, r, up),
Cond_eval_33(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, q, r, up),
lesseq_int(pos x, neg s y) -> false(),
lesseq_int(pos 0(), pos y) -> true(),
lesseq_int(pos 0(), neg 0()) -> true(),
lesseq_int(pos s x, pos 0()) -> false(),
lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
lesseq_int(pos s x, neg y) -> false(),
lesseq_int(neg x, pos y) -> true(),
lesseq_int(neg x, neg 0()) -> true(),
lesseq_int(neg 0(), neg s y) -> false(),
lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_33(lesseq_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_331(greater_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_381(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_39(n, i, j, k, l, t, h, m, p, q, r, up),
eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_381(greater_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_38(lesseq_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_32(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
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),
eval_31(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_32(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
Cond_eval_231(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_24(n, i, j, k, l, t, h, m, p, q, r, up),
and(true(), true()) -> true(),
and(true(), false()) -> false(),
and(false(), true()) -> false(),
and(false(), false()) -> false(),
eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_231(and(greater_int(q, pos 0()), greater_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_23(or(lesseq_int(q, pos 0()), lesseq_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_191(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_19(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_18(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_19(n, i, j, k, l, t, h, minus_int(m, q), p, q, r, up),
eval_13(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, mult_int(pos s s 0(), n), k, l, t, h, m, p, q, r, up),
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),
eval_12(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_13(n, plus_int(pos s 0(), n), j, k, l, t, h, m, p, q, r, up),
eval_50(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
Cond_eval_49(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_50(n, i, j, k, l, t, h, m, p, q, r, up),
eval_41(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_42(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
eval_40(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_41(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
Cond_eval_0(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_1(n, i, j, k, l, t, h, m, p, q, r, true()),
eval_0(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_0(greater_int(n, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_461(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, l, t, h, m, p, q, r, up),
eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_461(greater_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_46(lesseq_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_22(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, minus_int(m, r), p, q, r, up),
eval_21(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, m, up),
eval_14(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_15(n, i, j, k, l, t, h, m, p, q, r, up),
mult_int(pos x, pos y) -> pos mult_nat(x, y),
mult_int(pos x, neg y) -> neg mult_nat(x, y),
mult_int(neg x, pos y) -> neg mult_nat(x, y),
mult_int(neg x, neg y) -> pos mult_nat(x, y),
eval_10(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_11(n, i, j, pos s 0(), l, t, h, m, p, q, r, up),
Cond_eval_5(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_10(n, i, j, k, l, t, h, m, p, q, r, up),
eval_3(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_4(n, i, j, k, l, t, pos s 0(), m, p, q, r, up),
eval_2(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_3(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_191(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_21(n, i, j, k, l, t, h, m, p, q, r, up),
less_int(pos 0(), pos 0()) -> false(),
less_int(pos 0(), pos s y) -> true(),
less_int(pos 0(), neg 0()) -> false(),
less_int(pos 0(), neg s y) -> false(),
less_int(pos s x, pos 0()) -> false(),
less_int(pos s x, pos s y) -> less_int(pos x, pos y),
less_int(pos s x, neg 0()) -> false(),
less_int(pos s x, neg s y) -> false(),
less_int(neg 0(), pos 0()) -> false(),
less_int(neg 0(), pos s y) -> true(),
less_int(neg 0(), neg 0()) -> false(),
less_int(neg 0(), neg s y) -> false(),
less_int(neg s x, pos 0()) -> true(),
less_int(neg s x, pos s y) -> true(),
less_int(neg s x, neg 0()) -> true(),
less_int(neg s x, neg s y) -> less_int(neg x, neg y),
Cond_eval_151(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_17(n, i, j, k, l, t, h, m, p, q, r, up),
eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_151(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_15(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_47(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_48(n, i, j, k, l, t, h, m, p, q, r, not up),
Cond_eval_46(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_47(n, i, j, k, t, t, h, m, p, q, r, up),
eval_53(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
Cond_eval_491(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_481(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_49(n, i, j, k, l, t, h, m, mult_int(pos s s 0(), p), q, r, up),
greatereq_int(pos x, pos 0()) -> true(),
greatereq_int(pos x, neg y) -> true(),
greatereq_int(pos 0(), pos s y) -> false(),
greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
greatereq_int(neg x, pos s y) -> false(),
greatereq_int(neg 0(), pos 0()) -> true(),
greatereq_int(neg 0(), neg y) -> true(),
greatereq_int(neg s x, pos 0()) -> false(),
greatereq_int(neg s x, neg 0()) -> false(),
greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_481(greatereq_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_48(less_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_26(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_27(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
eval_25(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_26(n, i, j, k, l, t, h, m, p, q, r, up),
eval_37(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
not true() -> false(),
not false() -> true(),
eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_49(not up, n, i, j, k, l, t, h, m, p, q, r, up),
eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_491(up, n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_23(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, r, up),
or(true(), true()) -> true(),
or(true(), false()) -> true(),
or(false(), true()) -> true(),
or(false(), false()) -> false(),
eval_9(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, mult_int(pos s s 0(), n), t, h, n, p, q, r, up),
eval_30(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_31(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
eval_29(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_30(n, i, j, k, l, t, h, m, p, q, r, up),
eval_20(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, p, up),
Cond_eval_19(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_20(n, i, j, k, l, t, h, m, p, q, r, up),
eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_25(n, i, j, k, l, t, h, m, p, q, r, up),
eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_29(n, i, j, k, l, t, h, m, p, q, r, up),
eval_39(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_40(n, i, j, k, l, t, h, m, p, q, r, up),
eval_36(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_37(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
eval_35(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_36(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
eval_34(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_35(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_331(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_34(n, i, j, k, l, t, h, m, p, q, r, up),
eval_1(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, pos s 0(), q, r, up),
eval_28(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
eval_27(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_28(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
Cond_eval_48(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, p, q, r, up),
eval_8(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_9(n, i, j, plus_int(pos s 0(), n), l, t, h, n, p, q, r, up),
eval_43(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_44(n, i, j, k, l, t, neg_int h, m, p, q, r, up),
Cond_eval_38(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_43(n, i, j, k, l, t, h, m, p, q, r, up),
eval_42(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
eval_7(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_8(n, i, n, k, l, t, h, m, p, q, r, up),
eval_6(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_7(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
eval_16(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, p, r, up),
Cond_eval_15(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_16(n, i, j, k, l, t, h, m, p, q, r, up),
eval_44(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_45(n, i, j, k, l, k, h, m, p, q, r, up),
neg_int pos x -> neg x,
neg_int neg x -> pos x,
eval_11(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_12(n, i, j, k, n, t, h, m, p, q, r, up),
eval_45(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_46(n, i, j, l, l, t, h, m, p, q, r, up),
Cond_eval_52(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_6(n, i, j, k, l, t, h, m, p, q, r, up),
eval_17(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, m, r, up),
minus_nat(0(), 0()) -> pos 0(),
minus_nat(0(), s y) -> neg s y,
minus_nat(s x, 0()) -> pos s x,
minus_nat(s x, s y) -> minus_nat(x, y),
plus_nat(0(), x) -> x,
plus_nat(s x, y) -> s plus_nat(x, y),
mult_nat(0(), y) -> 0(),
mult_nat(s x, 0()) -> 0(),
mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y)
}
SRS: We consider a TRS.
Trs:
{
Cond_eval_511(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
greater_int(pos 0(), pos 0()) -> false(),
greater_int(pos 0(), pos s y) -> false(),
greater_int(pos 0(), neg 0()) -> false(),
greater_int(pos 0(), neg s y) -> true(),
greater_int(pos s x, pos 0()) -> true(),
greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
greater_int(pos s x, neg 0()) -> true(),
greater_int(pos s x, neg s y) -> true(),
greater_int(neg 0(), pos 0()) -> false(),
greater_int(neg 0(), pos s y) -> false(),
greater_int(neg 0(), neg 0()) -> false(),
greater_int(neg 0(), neg s y) -> true(),
greater_int(neg s x, pos 0()) -> false(),
greater_int(neg s x, pos s y) -> false(),
greater_int(neg s x, neg 0()) -> false(),
greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_511(greater_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_51(lesseq_int(i, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_52(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_53(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_51(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_52(n, i, j, k, l, t, h, m, p, q, r, up),
eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_5(not up, n, i, j, k, l, t, h, m, p, q, r, up),
eval_5(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_52(up, n, i, j, k, l, t, h, m, p, q, r, up),
eval_4(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_5(n, i, j, k, l, t, h, n, p, q, r, up),
Cond_eval_33(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, q, r, up),
lesseq_int(pos x, neg s y) -> false(),
lesseq_int(pos 0(), pos y) -> true(),
lesseq_int(pos 0(), neg 0()) -> true(),
lesseq_int(pos s x, pos 0()) -> false(),
lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
lesseq_int(pos s x, neg y) -> false(),
lesseq_int(neg x, pos y) -> true(),
lesseq_int(neg x, neg 0()) -> true(),
lesseq_int(neg 0(), neg s y) -> false(),
lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_33(lesseq_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_33(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_331(greater_int(r, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_381(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_39(n, i, j, k, l, t, h, m, p, q, r, up),
eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_381(greater_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_38(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_38(lesseq_int(q, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_32(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
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),
eval_31(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_32(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
Cond_eval_231(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_24(n, i, j, k, l, t, h, m, p, q, r, up),
and(true(), true()) -> true(),
and(true(), false()) -> false(),
and(false(), true()) -> false(),
and(false(), false()) -> false(),
eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_231(and(greater_int(q, pos 0()), greater_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
eval_23(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_23(or(lesseq_int(q, pos 0()), lesseq_int(r, pos 0())), n, i, j, k, l, t, h, m, p, q, r, up),
eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_191(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_19(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_19(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_18(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_19(n, i, j, k, l, t, h, minus_int(m, q), p, q, r, up),
eval_13(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, mult_int(pos s s 0(), n), k, l, t, h, m, p, q, r, up),
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),
eval_12(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_13(n, plus_int(pos s 0(), n), j, k, l, t, h, m, p, q, r, up),
eval_50(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
Cond_eval_49(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_50(n, i, j, k, l, t, h, m, p, q, r, up),
eval_41(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_42(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
eval_40(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_41(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
Cond_eval_0(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_1(n, i, j, k, l, t, h, m, p, q, r, true()),
eval_0(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_0(greater_int(n, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_461(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, l, t, h, m, p, q, r, up),
eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_461(greater_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_46(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_46(lesseq_int(m, pos 0()), n, i, j, k, l, t, h, m, p, q, r, up),
eval_22(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, minus_int(m, r), p, q, r, up),
eval_21(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, m, up),
eval_14(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_15(n, i, j, k, l, t, h, m, p, q, r, up),
mult_int(pos x, pos y) -> pos mult_nat(x, y),
mult_int(pos x, neg y) -> neg mult_nat(x, y),
mult_int(neg x, pos y) -> neg mult_nat(x, y),
mult_int(neg x, neg y) -> pos mult_nat(x, y),
eval_10(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_11(n, i, j, pos s 0(), l, t, h, m, p, q, r, up),
Cond_eval_5(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_10(n, i, j, k, l, t, h, m, p, q, r, up),
eval_3(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_4(n, i, j, k, l, t, pos s 0(), m, p, q, r, up),
eval_2(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_3(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_191(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_21(n, i, j, k, l, t, h, m, p, q, r, up),
less_int(pos 0(), pos 0()) -> false(),
less_int(pos 0(), pos s y) -> true(),
less_int(pos 0(), neg 0()) -> false(),
less_int(pos 0(), neg s y) -> false(),
less_int(pos s x, pos 0()) -> false(),
less_int(pos s x, pos s y) -> less_int(pos x, pos y),
less_int(pos s x, neg 0()) -> false(),
less_int(pos s x, neg s y) -> false(),
less_int(neg 0(), pos 0()) -> false(),
less_int(neg 0(), pos s y) -> true(),
less_int(neg 0(), neg 0()) -> false(),
less_int(neg 0(), neg s y) -> false(),
less_int(neg s x, pos 0()) -> true(),
less_int(neg s x, pos s y) -> true(),
less_int(neg s x, neg 0()) -> true(),
less_int(neg s x, neg s y) -> less_int(neg x, neg y),
Cond_eval_151(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_17(n, i, j, k, l, t, h, m, p, q, r, up),
eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_151(less_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_15(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_15(greatereq_int(m, p), n, i, j, k, l, t, h, m, p, q, r, up),
eval_47(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_48(n, i, j, k, l, t, h, m, p, q, r, not up),
Cond_eval_46(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_47(n, i, j, k, t, t, h, m, p, q, r, up),
eval_53(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_51(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
Cond_eval_491(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_481(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_49(n, i, j, k, l, t, h, m, mult_int(pos s s 0(), p), q, r, up),
greatereq_int(pos x, pos 0()) -> true(),
greatereq_int(pos x, neg y) -> true(),
greatereq_int(pos 0(), pos s y) -> false(),
greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
greatereq_int(neg x, pos s y) -> false(),
greatereq_int(neg 0(), pos 0()) -> true(),
greatereq_int(neg 0(), neg y) -> true(),
greatereq_int(neg s x, pos 0()) -> false(),
greatereq_int(neg s x, neg 0()) -> false(),
greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_481(greatereq_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_48(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_48(less_int(p, n), n, i, j, k, l, t, h, m, p, q, r, up),
eval_26(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_27(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
eval_25(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_26(n, i, j, k, l, t, h, m, p, q, r, up),
eval_37(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, minus_int(r, pos s 0()), up),
not true() -> false(),
not false() -> true(),
eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_49(not up, n, i, j, k, l, t, h, m, p, q, r, up),
eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> Cond_eval_491(up, n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_23(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_33(n, i, j, k, l, t, h, m, p, q, r, up),
or(true(), true()) -> true(),
or(true(), false()) -> true(),
or(false(), true()) -> true(),
or(false(), false()) -> false(),
eval_9(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_14(n, i, j, k, mult_int(pos s s 0(), n), t, h, n, p, q, r, up),
eval_30(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_31(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
eval_29(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_30(n, i, j, k, l, t, h, m, p, q, r, up),
eval_20(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_22(n, i, j, k, l, t, h, m, p, q, p, up),
Cond_eval_19(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_20(n, i, j, k, l, t, h, m, p, q, r, up),
eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_25(n, i, j, k, l, t, h, m, p, q, r, up),
eval_24(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_29(n, i, j, k, l, t, h, m, p, q, r, up),
eval_39(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_40(n, i, j, k, l, t, h, m, p, q, r, up),
eval_36(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_37(n, i, minus_int(j, pos s 0()), k, l, t, h, m, p, q, r, up),
eval_35(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_36(n, i, j, plus_int(k, h), l, t, h, m, p, q, r, up),
eval_34(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_35(n, i, j, k, l, t, h, m, p, q, r, up),
Cond_eval_331(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_34(n, i, j, k, l, t, h, m, p, q, r, up),
eval_1(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, pos s 0(), q, r, up),
eval_28(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_23(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
eval_27(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_28(n, plus_int(pos s 0(), i), j, k, l, t, h, m, p, q, r, up),
Cond_eval_48(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_2(n, i, j, k, l, t, h, m, p, q, r, up),
eval_8(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_9(n, i, j, plus_int(pos s 0(), n), l, t, h, n, p, q, r, up),
eval_43(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_44(n, i, j, k, l, t, neg_int h, m, p, q, r, up),
Cond_eval_38(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_43(n, i, j, k, l, t, h, m, p, q, r, up),
eval_42(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_38(n, i, j, k, l, t, h, m, p, minus_int(q, pos s 0()), r, up),
eval_7(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_8(n, i, n, k, l, t, h, m, p, q, r, up),
eval_6(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_7(n, pos s 0(), j, k, l, t, h, m, p, q, r, up),
eval_16(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, p, r, up),
Cond_eval_15(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_16(n, i, j, k, l, t, h, m, p, q, r, up),
eval_44(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_45(n, i, j, k, l, k, h, m, p, q, r, up),
neg_int pos x -> neg x,
neg_int neg x -> pos x,
eval_11(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_12(n, i, j, k, n, t, h, m, p, q, r, up),
eval_45(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_46(n, i, j, l, l, t, h, m, p, q, r, up),
Cond_eval_52(true(), n, i, j, k, l, t, h, m, p, q, r, up) -> eval_6(n, i, j, k, l, t, h, m, p, q, r, up),
eval_17(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_18(n, i, j, k, l, t, h, m, p, m, r, up),
minus_nat(0(), 0()) -> pos 0(),
minus_nat(0(), s y) -> neg s y,
minus_nat(s x, 0()) -> pos s x,
minus_nat(s x, s y) -> minus_nat(x, y),
plus_nat(0(), x) -> x,
plus_nat(s x, y) -> s plus_nat(x, y),
mult_nat(0(), y) -> 0(),
mult_nat(s x, 0()) -> 0(),
mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y)
}
Fail