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()
  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()
   Open