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