MAYBE

Problem:
 and(tt(),tt()) -> tt()
 is_nat(0()) -> tt()
 is_nat(s(x)) -> is_nat(x)
 is_natlist(nil()) -> tt()
 is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
 from(x) -> fromCond(is_natlist(x),x)
 fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))

Proof:
 DP Processor:
  DPs:
   is_nat#(s(x)) -> is_nat#(x)
   is_natlist#(cons(x,xs)) -> is_natlist#(xs)
   is_natlist#(cons(x,xs)) -> is_nat#(x)
   is_natlist#(cons(x,xs)) -> and#(is_nat(x),is_natlist(xs))
   from#(x) -> is_natlist#(x)
   from#(x) -> fromCond#(is_natlist(x),x)
   fromCond#(tt(),cons(x,xs)) -> from#(cons(s(x),cons(x,xs)))
  TRS:
   and(tt(),tt()) -> tt()
   is_nat(0()) -> tt()
   is_nat(s(x)) -> is_nat(x)
   is_natlist(nil()) -> tt()
   is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
   from(x) -> fromCond(is_natlist(x),x)
   fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))
  TDG Processor:
   DPs:
    is_nat#(s(x)) -> is_nat#(x)
    is_natlist#(cons(x,xs)) -> is_natlist#(xs)
    is_natlist#(cons(x,xs)) -> is_nat#(x)
    is_natlist#(cons(x,xs)) -> and#(is_nat(x),is_natlist(xs))
    from#(x) -> is_natlist#(x)
    from#(x) -> fromCond#(is_natlist(x),x)
    fromCond#(tt(),cons(x,xs)) -> from#(cons(s(x),cons(x,xs)))
   TRS:
    and(tt(),tt()) -> tt()
    is_nat(0()) -> tt()
    is_nat(s(x)) -> is_nat(x)
    is_natlist(nil()) -> tt()
    is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
    from(x) -> fromCond(is_natlist(x),x)
    fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))
   graph:
    fromCond#(tt(),cons(x,xs)) -> from#(cons(s(x),cons(x,xs))) ->
    from#(x) -> fromCond#(is_natlist(x),x)
    fromCond#(tt(),cons(x,xs)) -> from#(cons(s(x),cons(x,xs))) ->
    from#(x) -> is_natlist#(x)
    from#(x) -> fromCond#(is_natlist(x),x) ->
    fromCond#(tt(),cons(x,xs)) -> from#(cons(s(x),cons(x,xs)))
    from#(x) -> is_natlist#(x) ->
    is_natlist#(cons(x,xs)) -> and#(is_nat(x),is_natlist(xs))
    from#(x) -> is_natlist#(x) -> is_natlist#(cons(x,xs)) -> is_nat#(x)
    from#(x) -> is_natlist#(x) ->
    is_natlist#(cons(x,xs)) -> is_natlist#(xs)
    is_natlist#(cons(x,xs)) -> is_natlist#(xs) ->
    is_natlist#(cons(x,xs)) -> and#(is_nat(x),is_natlist(xs))
    is_natlist#(cons(x,xs)) -> is_natlist#(xs) ->
    is_natlist#(cons(x,xs)) -> is_nat#(x)
    is_natlist#(cons(x,xs)) -> is_natlist#(xs) ->
    is_natlist#(cons(x,xs)) -> is_natlist#(xs)
    is_natlist#(cons(x,xs)) -> is_nat#(x) -> is_nat#(s(x)) -> is_nat#(x)
    is_nat#(s(x)) -> is_nat#(x) -> is_nat#(s(x)) -> is_nat#(x)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 11/49
    DPs:
     fromCond#(tt(),cons(x,xs)) -> from#(cons(s(x),cons(x,xs)))
     from#(x) -> fromCond#(is_natlist(x),x)
    TRS:
     and(tt(),tt()) -> tt()
     is_nat(0()) -> tt()
     is_nat(s(x)) -> is_nat(x)
     is_natlist(nil()) -> tt()
     is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
     from(x) -> fromCond(is_natlist(x),x)
     fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))
    Open
    
    DPs:
     is_natlist#(cons(x,xs)) -> is_natlist#(xs)
    TRS:
     and(tt(),tt()) -> tt()
     is_nat(0()) -> tt()
     is_nat(s(x)) -> is_nat(x)
     is_natlist(nil()) -> tt()
     is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
     from(x) -> fromCond(is_natlist(x),x)
     fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))
    Subterm Criterion Processor:
     simple projection:
      pi(is_natlist#) = 0
     problem:
      DPs:
       
      TRS:
       and(tt(),tt()) -> tt()
       is_nat(0()) -> tt()
       is_nat(s(x)) -> is_nat(x)
       is_natlist(nil()) -> tt()
       is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
       from(x) -> fromCond(is_natlist(x),x)
       fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))
     Qed
    
    DPs:
     is_nat#(s(x)) -> is_nat#(x)
    TRS:
     and(tt(),tt()) -> tt()
     is_nat(0()) -> tt()
     is_nat(s(x)) -> is_nat(x)
     is_natlist(nil()) -> tt()
     is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
     from(x) -> fromCond(is_natlist(x),x)
     fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))
    Subterm Criterion Processor:
     simple projection:
      pi(is_nat#) = 0
     problem:
      DPs:
       
      TRS:
       and(tt(),tt()) -> tt()
       is_nat(0()) -> tt()
       is_nat(s(x)) -> is_nat(x)
       is_natlist(nil()) -> tt()
       is_natlist(cons(x,xs)) -> and(is_nat(x),is_natlist(xs))
       from(x) -> fromCond(is_natlist(x),x)
       fromCond(tt(),cons(x,xs)) -> from(cons(s(x),cons(x,xs)))
     Qed