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()
   CDG Processor:
    DPs:
     *#(X,+(Y,1())) -> *#(1(),0())
     *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
    TRS:
     *(X,0()) -> X
     *(X,0()) -> 0()
    graph:
     *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0()))) ->
     *#(X,+(Y,1())) -> *#(1(),0())
     *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0()))) -> *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),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: 1
      #arcs: 2/4
      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