MAYBE

Problem:
 *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
 *(X,1()) -> X
 *(X,0()) -> X
 *(X,0()) -> 0()

Proof:
 DP Processor:
  DPs:
   *#(X,+(Y,1())) -> *#(1(),0())
   *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
  TRS:
   *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
   *(X,1()) -> X
   *(X,0()) -> X
   *(X,0()) -> 0()
  Usable Rule Processor:
   DPs:
    *#(X,+(Y,1())) -> *#(1(),0())
    *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
   TRS:
    *(X,0()) -> X
    *(X,0()) -> 0()
   Restore Modifier:
    DPs:
     *#(X,+(Y,1())) -> *#(1(),0())
     *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
    TRS:
     *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
     *(X,1()) -> X
     *(X,0()) -> X
     *(X,0()) -> 0()
    SCC Processor:
     #sccs: 1
     #rules: 2
     #arcs: 4/4
     DPs:
      *#(X,+(Y,1())) -> *#(1(),0())
      *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
     TRS:
      *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
      *(X,1()) -> X
      *(X,0()) -> X
      *(X,0()) -> 0()
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [*#](x0, x1) = x1,
       
       [0] = 0,
       
       [*](x0, x1) = x0,
       
       [+](x0, x1) = x1,
       
       [1] = 1
      orientation:
       *#(X,+(Y,1())) = 1 >= 0 = *#(1(),0())
       
       *#(X,+(Y,1())) = 1 >= 1 = *#(X,+(Y,*(1(),0())))
       
       *(X,+(Y,1())) = X >= X = +(*(X,+(Y,*(1(),0()))),X)
       
       *(X,1()) = X >= X = X
       
       *(X,0()) = X >= X = X
       
       *(X,0()) = X >= 0 = 0()
      problem:
       DPs:
        *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
       TRS:
        *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
        *(X,1()) -> X
        *(X,0()) -> X
        *(X,0()) -> 0()
      Open