MAYBE

Problem:
 h(f(f(x))) -> h(f(g(f(x))))
 f(g(f(x))) -> f(f(x))

Proof:
 DP Processor:
  DPs:
   h#(f(f(x))) -> f#(g(f(x)))
   h#(f(f(x))) -> h#(f(g(f(x))))
   f#(g(f(x))) -> f#(f(x))
  TRS:
   h(f(f(x))) -> h(f(g(f(x))))
   f(g(f(x))) -> f(f(x))
  Usable Rule Processor:
   DPs:
    h#(f(f(x))) -> f#(g(f(x)))
    h#(f(f(x))) -> h#(f(g(f(x))))
    f#(g(f(x))) -> f#(f(x))
   TRS:
    f(g(f(x))) -> f(f(x))
   TDG Processor:
    DPs:
     h#(f(f(x))) -> f#(g(f(x)))
     h#(f(f(x))) -> h#(f(g(f(x))))
     f#(g(f(x))) -> f#(f(x))
    TRS:
     f(g(f(x))) -> f(f(x))
    graph:
     f#(g(f(x))) -> f#(f(x)) -> f#(g(f(x))) -> f#(f(x))
     h#(f(f(x))) -> f#(g(f(x))) -> f#(g(f(x))) -> f#(f(x))
     h#(f(f(x))) -> h#(f(g(f(x)))) -> h#(f(f(x))) -> h#(f(g(f(x))))
     h#(f(f(x))) -> h#(f(g(f(x)))) -> h#(f(f(x))) -> f#(g(f(x)))
    Restore Modifier:
     DPs:
      h#(f(f(x))) -> f#(g(f(x)))
      h#(f(f(x))) -> h#(f(g(f(x))))
      f#(g(f(x))) -> f#(f(x))
     TRS:
      h(f(f(x))) -> h(f(g(f(x))))
      f(g(f(x))) -> f(f(x))
     SCC Processor:
      #sccs: 2
      #rules: 2
      #arcs: 4/9
      DPs:
       h#(f(f(x))) -> h#(f(g(f(x))))
      TRS:
       h(f(f(x))) -> h(f(g(f(x))))
       f(g(f(x))) -> f(f(x))
      Open
      
      DPs:
       f#(g(f(x))) -> f#(f(x))
      TRS:
       h(f(f(x))) -> h(f(g(f(x))))
       f(g(f(x))) -> f(f(x))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0) = x0,
        
        [g](x0) = 1,
        
        [h](x0) = 0,
        
        [f](x0) = 0
       orientation:
        f#(g(f(x))) = 1 >= 0 = f#(f(x))
        
        h(f(f(x))) = 0 >= 0 = h(f(g(f(x))))
        
        f(g(f(x))) = 0 >= 0 = f(f(x))
       problem:
        DPs:
         
        TRS:
         h(f(f(x))) -> h(f(g(f(x))))
         f(g(f(x))) -> f(f(x))
       Qed