MAYBE

Problem:
 fac(s(x)) -> *(fac(p(s(x))),s(x))
 p(s(0())) -> 0()
 p(s(s(x))) -> s(p(s(x)))

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