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()
    Subterm Criterion Processor:
     simple projection:
      pi(isDouble#) = 0
     problem:
      DPs:
       
      TRS:
       f(tt(),x) -> f(isDouble(x),s(s(x)))
       isDouble(s(s(x))) -> isDouble(x)
       isDouble(0()) -> tt()
     Qed