MAYBE

Problem:
 isList(nil()) -> tt()
 isList(Cons(x,xs)) -> isList(xs)
 downfrom(0()) -> nil()
 downfrom(s(x)) -> Cons(s(x),downfrom(x))
 f(x) -> cond(isList(downfrom(x)),s(x))
 cond(tt(),x) -> f(x)

Proof:
 DP Processor:
  DPs:
   isList#(Cons(x,xs)) -> isList#(xs)
   downfrom#(s(x)) -> downfrom#(x)
   f#(x) -> downfrom#(x)
   f#(x) -> isList#(downfrom(x))
   f#(x) -> cond#(isList(downfrom(x)),s(x))
   cond#(tt(),x) -> f#(x)
  TRS:
   isList(nil()) -> tt()
   isList(Cons(x,xs)) -> isList(xs)
   downfrom(0()) -> nil()
   downfrom(s(x)) -> Cons(s(x),downfrom(x))
   f(x) -> cond(isList(downfrom(x)),s(x))
   cond(tt(),x) -> f(x)
  TDG Processor:
   DPs:
    isList#(Cons(x,xs)) -> isList#(xs)
    downfrom#(s(x)) -> downfrom#(x)
    f#(x) -> downfrom#(x)
    f#(x) -> isList#(downfrom(x))
    f#(x) -> cond#(isList(downfrom(x)),s(x))
    cond#(tt(),x) -> f#(x)
   TRS:
    isList(nil()) -> tt()
    isList(Cons(x,xs)) -> isList(xs)
    downfrom(0()) -> nil()
    downfrom(s(x)) -> Cons(s(x),downfrom(x))
    f(x) -> cond(isList(downfrom(x)),s(x))
    cond(tt(),x) -> f(x)
   graph:
    cond#(tt(),x) -> f#(x) -> f#(x) -> cond#(isList(downfrom(x)),s(x))
    cond#(tt(),x) -> f#(x) -> f#(x) -> isList#(downfrom(x))
    cond#(tt(),x) -> f#(x) -> f#(x) -> downfrom#(x)
    f#(x) -> cond#(isList(downfrom(x)),s(x)) -> cond#(tt(),x) -> f#(x)
    f#(x) -> downfrom#(x) -> downfrom#(s(x)) -> downfrom#(x)
    f#(x) -> isList#(downfrom(x)) ->
    isList#(Cons(x,xs)) -> isList#(xs)
    downfrom#(s(x)) -> downfrom#(x) ->
    downfrom#(s(x)) -> downfrom#(x)
    isList#(Cons(x,xs)) -> isList#(xs) -> isList#(Cons(x,xs)) -> isList#(xs)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 8/36
    DPs:
     cond#(tt(),x) -> f#(x)
     f#(x) -> cond#(isList(downfrom(x)),s(x))
    TRS:
     isList(nil()) -> tt()
     isList(Cons(x,xs)) -> isList(xs)
     downfrom(0()) -> nil()
     downfrom(s(x)) -> Cons(s(x),downfrom(x))
     f(x) -> cond(isList(downfrom(x)),s(x))
     cond(tt(),x) -> f(x)
    Open
    
    DPs:
     isList#(Cons(x,xs)) -> isList#(xs)
    TRS:
     isList(nil()) -> tt()
     isList(Cons(x,xs)) -> isList(xs)
     downfrom(0()) -> nil()
     downfrom(s(x)) -> Cons(s(x),downfrom(x))
     f(x) -> cond(isList(downfrom(x)),s(x))
     cond(tt(),x) -> f(x)
    Subterm Criterion Processor:
     simple projection:
      pi(isList#) = 0
     problem:
      DPs:
       
      TRS:
       isList(nil()) -> tt()
       isList(Cons(x,xs)) -> isList(xs)
       downfrom(0()) -> nil()
       downfrom(s(x)) -> Cons(s(x),downfrom(x))
       f(x) -> cond(isList(downfrom(x)),s(x))
       cond(tt(),x) -> f(x)
     Qed
    
    DPs:
     downfrom#(s(x)) -> downfrom#(x)
    TRS:
     isList(nil()) -> tt()
     isList(Cons(x,xs)) -> isList(xs)
     downfrom(0()) -> nil()
     downfrom(s(x)) -> Cons(s(x),downfrom(x))
     f(x) -> cond(isList(downfrom(x)),s(x))
     cond(tt(),x) -> f(x)
    Subterm Criterion Processor:
     simple projection:
      pi(downfrom#) = 0
     problem:
      DPs:
       
      TRS:
       isList(nil()) -> tt()
       isList(Cons(x,xs)) -> isList(xs)
       downfrom(0()) -> nil()
       downfrom(s(x)) -> Cons(s(x),downfrom(x))
       f(x) -> cond(isList(downfrom(x)),s(x))
       cond(tt(),x) -> f(x)
     Qed