MAYBE

Problem:
 f(tt(),x) -> f(isDouble(x),s(s(x)))
 isDouble(s(s(x))) -> isDouble(x)
 isDouble(0()) -> tt()

Proof:
 DP Processor:
  DPs:
   f#(tt(),x) -> isDouble#(x)
   f#(tt(),x) -> f#(isDouble(x),s(s(x)))
   isDouble#(s(s(x))) -> isDouble#(x)
  TRS:
   f(tt(),x) -> f(isDouble(x),s(s(x)))
   isDouble(s(s(x))) -> isDouble(x)
   isDouble(0()) -> tt()
  TDG Processor:
   DPs:
    f#(tt(),x) -> isDouble#(x)
    f#(tt(),x) -> f#(isDouble(x),s(s(x)))
    isDouble#(s(s(x))) -> isDouble#(x)
   TRS:
    f(tt(),x) -> f(isDouble(x),s(s(x)))
    isDouble(s(s(x))) -> isDouble(x)
    isDouble(0()) -> tt()
   graph:
    isDouble#(s(s(x))) -> isDouble#(x) ->
    isDouble#(s(s(x))) -> isDouble#(x)
    f#(tt(),x) -> isDouble#(x) ->
    isDouble#(s(s(x))) -> isDouble#(x)
    f#(tt(),x) -> f#(isDouble(x),s(s(x))) ->
    f#(tt(),x) -> f#(isDouble(x),s(s(x)))
    f#(tt(),x) -> f#(isDouble(x),s(s(x))) -> f#(tt(),x) -> isDouble#(x)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/9
    DPs:
     f#(tt(),x) -> f#(isDouble(x),s(s(x)))
    TRS:
     f(tt(),x) -> f(isDouble(x),s(s(x)))
     isDouble(s(s(x))) -> isDouble(x)
     isDouble(0()) -> tt()
    Open
    
    DPs:
     isDouble#(s(s(x))) -> isDouble#(x)
    TRS:
     f(tt(),x) -> f(isDouble(x),s(s(x)))
     isDouble(s(s(x))) -> isDouble(x)
     isDouble(0()) -> tt()
    KBO Processor:
     argument filtering:
      pi(tt) = []
      pi(f) = []
      pi(isDouble) = 0
      pi(s) = [0]
      pi(0) = []
      pi(isDouble#) = [0]
     weight function:
      w0 = 1
      w(isDouble#) = w(0) = w(f) = w(tt) = 1
      w(s) = w(isDouble) = 0
     precedence:
      s ~ f > 0 > isDouble# ~ isDouble ~ tt
     problem:
      DPs:
       
      TRS:
       f(tt(),x) -> f(isDouble(x),s(s(x)))
       isDouble(s(s(x))) -> isDouble(x)
       isDouble(0()) -> tt()
     Qed