MAYBE

Problem:
 from(X) -> cons(X,from(s(X)))
 2ndspos(0(),Z) -> rnil()
 2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
 2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
 2ndsneg(0(),Z) -> rnil()
 2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
 2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
 pi(X) -> 2ndspos(X,from(0()))
 plus(0(),Y) -> Y
 plus(s(X),Y) -> s(plus(X,Y))
 times(0(),Y) -> 0()
 times(s(X),Y) -> plus(Y,times(X,Y))
 square(X) -> times(X,X)

Proof:
 DP Processor:
  DPs:
   from#(X) -> from#(s(X))
   2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z))
   2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z)
   2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,Z))
   2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z)
   pi#(X) -> from#(0())
   pi#(X) -> 2ndspos#(X,from(0()))
   plus#(s(X),Y) -> plus#(X,Y)
   times#(s(X),Y) -> times#(X,Y)
   times#(s(X),Y) -> plus#(Y,times(X,Y))
   square#(X) -> times#(X,X)
  TRS:
   from(X) -> cons(X,from(s(X)))
   2ndspos(0(),Z) -> rnil()
   2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
   2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
   2ndsneg(0(),Z) -> rnil()
   2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
   2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
   pi(X) -> 2ndspos(X,from(0()))
   plus(0(),Y) -> Y
   plus(s(X),Y) -> s(plus(X,Y))
   times(0(),Y) -> 0()
   times(s(X),Y) -> plus(Y,times(X,Y))
   square(X) -> times(X,X)
  Usable Rule Processor:
   DPs:
    from#(X) -> from#(s(X))
    2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z))
    2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z)
    2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,Z))
    2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z)
    pi#(X) -> from#(0())
    pi#(X) -> 2ndspos#(X,from(0()))
    plus#(s(X),Y) -> plus#(X,Y)
    times#(s(X),Y) -> times#(X,Y)
    times#(s(X),Y) -> plus#(Y,times(X,Y))
    square#(X) -> times#(X,X)
   TRS:
    f22(x,y) -> x
    f22(x,y) -> y
    from(X) -> cons(X,from(s(X)))
    times(0(),Y) -> 0()
    times(s(X),Y) -> plus(Y,times(X,Y))
    plus(0(),Y) -> Y
    plus(s(X),Y) -> s(plus(X,Y))
   ADG Processor:
    DPs:
     from#(X) -> from#(s(X))
     2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z))
     2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z)
     2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,Z))
     2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z)
     pi#(X) -> from#(0())
     pi#(X) -> 2ndspos#(X,from(0()))
     plus#(s(X),Y) -> plus#(X,Y)
     times#(s(X),Y) -> times#(X,Y)
     times#(s(X),Y) -> plus#(Y,times(X,Y))
     square#(X) -> times#(X,X)
    TRS:
     f22(x,y) -> x
     f22(x,y) -> y
     from(X) -> cons(X,from(s(X)))
     times(0(),Y) -> 0()
     times(s(X),Y) -> plus(Y,times(X,Y))
     plus(0(),Y) -> Y
     plus(s(X),Y) -> s(plus(X,Y))
    graph:
     square#(X) -> times#(X,X) -> times#(s(X),Y) -> times#(X,Y)
     square#(X) -> times#(X,X) ->
     times#(s(X),Y) -> plus#(Y,times(X,Y))
     times#(s(X),Y) -> times#(X,Y) -> times#(s(X),Y) -> times#(X,Y)
     times#(s(X),Y) -> times#(X,Y) ->
     times#(s(X),Y) -> plus#(Y,times(X,Y))
     times#(s(X),Y) -> plus#(Y,times(X,Y)) ->
     plus#(s(X),Y) -> plus#(X,Y)
     plus#(s(X),Y) -> plus#(X,Y) -> plus#(s(X),Y) -> plus#(X,Y)
     pi#(X) -> 2ndspos#(X,from(0())) ->
     2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z))
     pi#(X) -> from#(0()) ->
     from#(X) -> from#(s(X))
     2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z) ->
     2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z))
     2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z) ->
     2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z)
     2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,Z)) ->
     2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z)
     2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z) ->
     2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,Z))
     2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z) ->
     2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z)
     2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z)) ->
     2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z)
     from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X))
    Restore Modifier:
     DPs:
      from#(X) -> from#(s(X))
      2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z))
      2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z)
      2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,Z))
      2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z)
      pi#(X) -> from#(0())
      pi#(X) -> 2ndspos#(X,from(0()))
      plus#(s(X),Y) -> plus#(X,Y)
      times#(s(X),Y) -> times#(X,Y)
      times#(s(X),Y) -> plus#(Y,times(X,Y))
      square#(X) -> times#(X,X)
     TRS:
      from(X) -> cons(X,from(s(X)))
      2ndspos(0(),Z) -> rnil()
      2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
      2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
      2ndsneg(0(),Z) -> rnil()
      2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
      2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
      pi(X) -> 2ndspos(X,from(0()))
      plus(0(),Y) -> Y
      plus(s(X),Y) -> s(plus(X,Y))
      times(0(),Y) -> 0()
      times(s(X),Y) -> plus(Y,times(X,Y))
      square(X) -> times(X,X)
     SCC Processor:
      #sccs: 4
      #rules: 7
      #arcs: 15/121
      DPs:
       from#(X) -> from#(s(X))
      TRS:
       from(X) -> cons(X,from(s(X)))
       2ndspos(0(),Z) -> rnil()
       2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
       2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
       2ndsneg(0(),Z) -> rnil()
       2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
       2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
       pi(X) -> 2ndspos(X,from(0()))
       plus(0(),Y) -> Y
       plus(s(X),Y) -> s(plus(X,Y))
       times(0(),Y) -> 0()
       times(s(X),Y) -> plus(Y,times(X,Y))
       square(X) -> times(X,X)
      Open
      
      DPs:
       2ndspos#(s(N),cons(X,Z)) -> 2ndspos#(s(N),cons2(X,Z))
       2ndspos#(s(N),cons2(X,cons(Y,Z))) -> 2ndsneg#(N,Z)
       2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> 2ndspos#(N,Z)
       2ndsneg#(s(N),cons(X,Z)) -> 2ndsneg#(s(N),cons2(X,Z))
      TRS:
       from(X) -> cons(X,from(s(X)))
       2ndspos(0(),Z) -> rnil()
       2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
       2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
       2ndsneg(0(),Z) -> rnil()
       2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
       2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
       pi(X) -> 2ndspos(X,from(0()))
       plus(0(),Y) -> Y
       plus(s(X),Y) -> s(plus(X,Y))
       times(0(),Y) -> 0()
       times(s(X),Y) -> plus(Y,times(X,Y))
       square(X) -> times(X,X)
      Open
      
      DPs:
       times#(s(X),Y) -> times#(X,Y)
      TRS:
       from(X) -> cons(X,from(s(X)))
       2ndspos(0(),Z) -> rnil()
       2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
       2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
       2ndsneg(0(),Z) -> rnil()
       2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
       2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
       pi(X) -> 2ndspos(X,from(0()))
       plus(0(),Y) -> Y
       plus(s(X),Y) -> s(plus(X,Y))
       times(0(),Y) -> 0()
       times(s(X),Y) -> plus(Y,times(X,Y))
       square(X) -> times(X,X)
      Open
      
      DPs:
       plus#(s(X),Y) -> plus#(X,Y)
      TRS:
       from(X) -> cons(X,from(s(X)))
       2ndspos(0(),Z) -> rnil()
       2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
       2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
       2ndsneg(0(),Z) -> rnil()
       2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
       2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
       pi(X) -> 2ndspos(X,from(0()))
       plus(0(),Y) -> Y
       plus(s(X),Y) -> s(plus(X,Y))
       times(0(),Y) -> 0()
       times(s(X),Y) -> plus(Y,times(X,Y))
       square(X) -> times(X,X)
      Open