MAYBE

Problem:
 zeros() -> cons(0(),zeros())
 tail(cons(X,XS)) -> XS

Proof:
 DP Processor:
  DPs:
   zeros#() -> zeros#()
  TRS:
   zeros() -> cons(0(),zeros())
   tail(cons(X,XS)) -> XS
  Usable Rule Processor:
   DPs:
    zeros#() -> zeros#()
   TRS:
    
   Restore Modifier:
    DPs:
     zeros#() -> zeros#()
    TRS:
     zeros() -> cons(0(),zeros())
     tail(cons(X,XS)) -> XS
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 1/1
     DPs:
      zeros#() -> zeros#()
     TRS:
      zeros() -> cons(0(),zeros())
      tail(cons(X,XS)) -> XS
     Open