Time: 0.205196
TRS:
 {     g(x, cons(y, ys)) -> cons(plus_int(x, y), g(x, ys)),
  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(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)}
 SRS: We consider a TRS.
  Trs:
   {     g(x, cons(y, ys)) -> cons(plus_int(x, y), g(x, ys)),
    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(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)}
  APP: We consider a non-applicative system.
   Trs:
    {     g(x, cons(y, ys)) -> cons(plus_int(x, y), g(x, ys)),
     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(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)}
   REF:
    Strict:
     {     g(cons(ys, y), x) -> cons(g(ys, x), plus_int(y, x)),
      plus_int(pos y, pos x) -> pos plus_nat(y, x),
      plus_int(pos y, neg x) -> minus_nat(x, y),
      plus_int(neg y, pos x) -> minus_nat(y, x),
      plus_int(neg y, neg x) -> neg plus_nat(y, x),
         minus_nat(0(), 0()) -> pos 0(),
         minus_nat(0(), s x) -> pos s x,
         minus_nat(s y, 0()) -> neg s y,
         minus_nat(s y, s x) -> minus_nat(y, x),
            plus_nat(x, 0()) -> x,
            plus_nat(y, s x) -> s plus_nat(y, x)}
    Weak:
    {}
    LPO:
     Precedence:
      plus_nat > s, minus_nat > neg, minus_nat > pos, plus_int > plus_nat, plus_int > neg, plus_int > pos, plus_int > minus_nat, g > plus_int, g > cons
     Strict:
      {}
     Weak:
      {}
     Qed