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)
   EDG 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:
     f#(tt(),x) -> isList#(x) ->
     isList#(Cons(x,xs())) -> isList#(xs())
     f#(tt(),x) -> f#(isList(x),x) -> f#(tt(),x) -> isList#(x)
     f#(tt(),x) -> f#(isList(x),x) -> f#(tt(),x) -> f#(isList(x),x)
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 3/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