MAYBE
Time: 0.008892
TRS:
 {                 from X -> cons(X, from s X),
  after(s N, cons(X, XS)) -> after(N, XS),
           after(0(), XS) -> XS}
 DP:
  DP:
   {                 from# X -> from# s X,
    after#(s N, cons(X, XS)) -> after#(N, XS)}
  TRS:
  {                 from X -> cons(X, from s X),
   after(s N, cons(X, XS)) -> after(N, XS),
            after(0(), XS) -> XS}
  UR:
   {}
   EDG:
    {(after#(s N, cons(X, XS)) -> after#(N, XS), after#(s N, cons(X, XS)) -> after#(N, XS))
     (from# X -> from# s X, from# X -> from# s X)}
    STATUS:
     arrows: 0.500000
     SCCS (2):
      Scc:
       {after#(s N, cons(X, XS)) -> after#(N, XS)}
      Scc:
       {from# X -> from# s X}
      
      SCC (1):
       Strict:
        {after#(s N, cons(X, XS)) -> after#(N, XS)}
       Weak:
       {                 from X -> cons(X, from s X),
        after(s N, cons(X, XS)) -> after(N, XS),
                 after(0(), XS) -> XS}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = 1,
         
         [after](x0, x1) = x0 + 1,
         
         [from](x0) = 0,
         
         [s](x0) = x0 + 1,
         
         [0] = 0,
         
         [after#](x0, x1) = x0 + 1
        Strict:
         after#(s N, cons(X, XS)) -> after#(N, XS)
         2 + 0X + 0XS + 1N >= 1 + 0XS + 1N
        Weak:
         after(0(), XS) -> XS
         1 + 1XS >= 1XS
         after(s N, cons(X, XS)) -> after(N, XS)
         2 + 0X + 0XS + 0N >= 1 + 1XS + 0N
         from X -> cons(X, from s X)
         0 + 0X >= 1 + 0X
       Qed
     SCC (1):
      Strict:
       {from# X -> from# s X}
      Weak:
      {                 from X -> cons(X, from s X),
       after(s N, cons(X, XS)) -> after(N, XS),
                after(0(), XS) -> XS}
      Fail