MAYBE

Problem:
 f(tt(),x) -> f(isList(x),x)
 isList(Cons(x,xs())) -> isList(xs())
 isList(nil()) -> tt()

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