Time: 5.195948
TRS:
{ Cond_eval_7(true(), x, y1, y2, z) -> eval_9(x, y1, y2, z),
or(true(), true()) -> true(),
or(true(), false()) -> true(),
or(false(), true()) -> true(),
or(false(), false()) -> false(),
lesseq_int(pos x, neg s y) -> false(),
lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
lesseq_int(pos s x, pos 0()) -> false(),
lesseq_int(pos s x, neg y) -> false(),
lesseq_int(pos 0(), pos y) -> true(),
lesseq_int(pos 0(), neg 0()) -> true(),
lesseq_int(neg x, pos y) -> true(),
lesseq_int(neg x, neg 0()) -> true(),
lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
lesseq_int(neg 0(), neg s y) -> false(),
not true() -> false(),
not false() -> true(),
equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
equal_int(pos s x, pos 0()) -> false(),
equal_int(pos s x, neg s y) -> false(),
equal_int(pos s x, neg 0()) -> false(),
equal_int(pos 0(), pos s y) -> false(),
equal_int(pos 0(), pos 0()) -> true(),
equal_int(pos 0(), neg s y) -> false(),
equal_int(pos 0(), neg 0()) -> true(),
equal_int(neg s x, pos s y) -> false(),
equal_int(neg s x, pos 0()) -> false(),
equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
equal_int(neg s x, neg 0()) -> false(),
equal_int(neg 0(), pos s y) -> false(),
equal_int(neg 0(), pos 0()) -> true(),
equal_int(neg 0(), neg s y) -> false(),
equal_int(neg 0(), neg 0()) -> true(),
eval_7(x, y1, y2, z) -> Cond_eval_7(or(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), not equal_int(y2, pos s 0())), x, y1, y2, z),
eval_7(x, y1, y2, z) -> Cond_eval_71(and(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), equal_int(y2, pos s 0())), x, y1, y2, z),
eval_5(x, y1, y2, z) -> Cond_eval_5(greater_int(y2, pos s 0()), x, y1, y2, z),
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),
Cond_eval_71(true(), x, y1, y2, z) -> eval_5(x, y1, y2, minus_int(y1, pos s s s s s s s s s s 0())),
and(true(), true()) -> true(),
and(true(), false()) -> false(),
and(false(), true()) -> false(),
and(false(), false()) -> false(),
greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
greater_int(pos s x, pos 0()) -> true(),
greater_int(pos s x, neg s y) -> true(),
greater_int(pos s x, neg 0()) -> true(),
greater_int(pos 0(), pos s y) -> false(),
greater_int(pos 0(), pos 0()) -> false(),
greater_int(pos 0(), neg s y) -> true(),
greater_int(pos 0(), neg 0()) -> false(),
greater_int(neg s x, pos s y) -> false(),
greater_int(neg s x, pos 0()) -> false(),
greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
greater_int(neg s x, neg 0()) -> false(),
greater_int(neg 0(), pos s y) -> false(),
greater_int(neg 0(), pos 0()) -> false(),
greater_int(neg 0(), neg s y) -> true(),
greater_int(neg 0(), neg 0()) -> false(),
Cond_eval_31(true(), x, y1, y2, z) -> eval_5(x, y1, y2, z),
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_11(x, y1, y2, z) -> eval_5(x, plus_int(pos s s s s s s s s s s s 0(), y1), plus_int(pos s 0(), y2), z),
Cond_eval_11(true(), x, y1, y2, z) -> eval_3(x, y1, y2, z),
eval_1(x, y1, y2, z) -> Cond_eval_11(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_1(x, y1, y2, z) -> Cond_eval_1(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_3(x, y1, y2, z) -> Cond_eval_31(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_3(x, y1, y2, z) -> Cond_eval_3(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
Cond_eval_9(true(), x, y1, y2, z) -> eval_11(x, y1, y2, z),
Cond_eval_91(true(), x, y1, y2, z) -> eval_11(x, minus_int(y1, pos s s s s s s s s s s 0()), minus_int(y2, pos s 0()), z),
Cond_eval_1(true(), x, y1, y2, z) -> eval_2(x, y1, y2, minus_int(y1, pos s s s s s s s s s s 0())),
eval_9(x, y1, y2, z) -> Cond_eval_9(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_9(x, y1, y2, z) -> Cond_eval_91(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
Cond_eval_5(true(), x, y1, y2, z) -> eval_7(x, minus_int(y1, pos s s s s s s s s s s 0()), minus_int(y2, pos s 0()), z),
eval_0(x, y1, y2, z) -> eval_1(x, x, pos s 0(), z),
Cond_eval_3(true(), x, y1, y2, z) -> eval_3(x, plus_int(pos s s s s s s s s s s s 0(), y1), plus_int(pos s 0(), y2), z),
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_eval_7(true(), x, y1, y2, z) -> eval_9(x, y1, y2, z),
or(true(), true()) -> true(),
or(true(), false()) -> true(),
or(false(), true()) -> true(),
or(false(), false()) -> false(),
lesseq_int(pos x, neg s y) -> false(),
lesseq_int(pos s x, pos s y) -> lesseq_int(pos x, pos y),
lesseq_int(pos s x, pos 0()) -> false(),
lesseq_int(pos s x, neg y) -> false(),
lesseq_int(pos 0(), pos y) -> true(),
lesseq_int(pos 0(), neg 0()) -> true(),
lesseq_int(neg x, pos y) -> true(),
lesseq_int(neg x, neg 0()) -> true(),
lesseq_int(neg s x, neg s y) -> lesseq_int(neg x, neg y),
lesseq_int(neg 0(), neg s y) -> false(),
not true() -> false(),
not false() -> true(),
equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
equal_int(pos s x, pos 0()) -> false(),
equal_int(pos s x, neg s y) -> false(),
equal_int(pos s x, neg 0()) -> false(),
equal_int(pos 0(), pos s y) -> false(),
equal_int(pos 0(), pos 0()) -> true(),
equal_int(pos 0(), neg s y) -> false(),
equal_int(pos 0(), neg 0()) -> true(),
equal_int(neg s x, pos s y) -> false(),
equal_int(neg s x, pos 0()) -> false(),
equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
equal_int(neg s x, neg 0()) -> false(),
equal_int(neg 0(), pos s y) -> false(),
equal_int(neg 0(), pos 0()) -> true(),
equal_int(neg 0(), neg s y) -> false(),
equal_int(neg 0(), neg 0()) -> true(),
eval_7(x, y1, y2, z) -> Cond_eval_7(or(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), not equal_int(y2, pos s 0())), x, y1, y2, z),
eval_7(x, y1, y2, z) -> Cond_eval_71(and(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), equal_int(y2, pos s 0())), x, y1, y2, z),
eval_5(x, y1, y2, z) -> Cond_eval_5(greater_int(y2, pos s 0()), x, y1, y2, z),
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),
Cond_eval_71(true(), x, y1, y2, z) -> eval_5(x, y1, y2, minus_int(y1, pos s s s s s s s s s s 0())),
and(true(), true()) -> true(),
and(true(), false()) -> false(),
and(false(), true()) -> false(),
and(false(), false()) -> false(),
greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
greater_int(pos s x, pos 0()) -> true(),
greater_int(pos s x, neg s y) -> true(),
greater_int(pos s x, neg 0()) -> true(),
greater_int(pos 0(), pos s y) -> false(),
greater_int(pos 0(), pos 0()) -> false(),
greater_int(pos 0(), neg s y) -> true(),
greater_int(pos 0(), neg 0()) -> false(),
greater_int(neg s x, pos s y) -> false(),
greater_int(neg s x, pos 0()) -> false(),
greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
greater_int(neg s x, neg 0()) -> false(),
greater_int(neg 0(), pos s y) -> false(),
greater_int(neg 0(), pos 0()) -> false(),
greater_int(neg 0(), neg s y) -> true(),
greater_int(neg 0(), neg 0()) -> false(),
Cond_eval_31(true(), x, y1, y2, z) -> eval_5(x, y1, y2, z),
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_11(x, y1, y2, z) -> eval_5(x, plus_int(pos s s s s s s s s s s s 0(), y1), plus_int(pos s 0(), y2), z),
Cond_eval_11(true(), x, y1, y2, z) -> eval_3(x, y1, y2, z),
eval_1(x, y1, y2, z) -> Cond_eval_11(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_1(x, y1, y2, z) -> Cond_eval_1(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_3(x, y1, y2, z) -> Cond_eval_31(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_3(x, y1, y2, z) -> Cond_eval_3(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
Cond_eval_9(true(), x, y1, y2, z) -> eval_11(x, y1, y2, z),
Cond_eval_91(true(), x, y1, y2, z) -> eval_11(x, minus_int(y1, pos s s s s s s s s s s 0()), minus_int(y2, pos s 0()), z),
Cond_eval_1(true(), x, y1, y2, z) -> eval_2(x, y1, y2, minus_int(y1, pos s s s s s s s s s s 0())),
eval_9(x, y1, y2, z) -> Cond_eval_9(lesseq_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
eval_9(x, y1, y2, z) -> Cond_eval_91(greater_int(y1, pos s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0()), x, y1, y2, z),
Cond_eval_5(true(), x, y1, y2, z) -> eval_7(x, minus_int(y1, pos s s s s s s s s s s 0()), minus_int(y2, pos s 0()), z),
eval_0(x, y1, y2, z) -> eval_1(x, x, pos s 0(), z),
Cond_eval_3(true(), x, y1, y2, z) -> eval_3(x, plus_int(pos s s s s s s s s s s s 0(), y1), plus_int(pos s 0(), y2), z),
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