MAYBE

Problem:
 *(0(),x) -> 0()
 *(1(),x) -> x
 *(2(),2()) -> .(1(),0())
 *(3(),x) -> .(x,*(min(),x))
 *(min(),min()) -> 1()
 *(2(),min()) -> .(min(),2())
 *(.(x,y),z) -> .(*(x,z),*(y,z))
 *(+(y,z),x) -> +(*(x,y),*(x,z))
 +(0(),x) -> x
 +(x,x) -> *(2(),x)
 +(1(),2()) -> 3()
 +(1(),min()) -> 0()
 +(2(),min()) -> 1()
 +(3(),x) -> .(1(),+(min(),x))
 +(.(x,y),z) -> .(x,+(y,z))
 +(*(2(),x),x) -> *(3(),x)
 +(*(min(),x),x) -> 0()
 +(*(2(),v),*(min(),v)) -> v
 .(min(),3()) -> min()
 .(x,min()) -> .(+(min(),x),3())
 .(0(),x) -> x
 .(x,.(y,z)) -> .(+(x,y),z)

Proof:
 DP Processor:
  DPs:
   *#(2(),2()) -> .#(1(),0())
   *#(3(),x) -> *#(min(),x)
   *#(3(),x) -> .#(x,*(min(),x))
   *#(2(),min()) -> .#(min(),2())
   *#(.(x,y),z) -> *#(y,z)
   *#(.(x,y),z) -> *#(x,z)
   *#(.(x,y),z) -> .#(*(x,z),*(y,z))
   *#(+(y,z),x) -> *#(x,z)
   *#(+(y,z),x) -> *#(x,y)
   *#(+(y,z),x) -> +#(*(x,y),*(x,z))
   +#(x,x) -> *#(2(),x)
   +#(3(),x) -> +#(min(),x)
   +#(3(),x) -> .#(1(),+(min(),x))
   +#(.(x,y),z) -> +#(y,z)
   +#(.(x,y),z) -> .#(x,+(y,z))
   +#(*(2(),x),x) -> *#(3(),x)
   .#(x,min()) -> +#(min(),x)
   .#(x,min()) -> .#(+(min(),x),3())
   .#(x,.(y,z)) -> +#(x,y)
   .#(x,.(y,z)) -> .#(+(x,y),z)
  TRS:
   *(0(),x) -> 0()
   *(1(),x) -> x
   *(2(),2()) -> .(1(),0())
   *(3(),x) -> .(x,*(min(),x))
   *(min(),min()) -> 1()
   *(2(),min()) -> .(min(),2())
   *(.(x,y),z) -> .(*(x,z),*(y,z))
   *(+(y,z),x) -> +(*(x,y),*(x,z))
   +(0(),x) -> x
   +(x,x) -> *(2(),x)
   +(1(),2()) -> 3()
   +(1(),min()) -> 0()
   +(2(),min()) -> 1()
   +(3(),x) -> .(1(),+(min(),x))
   +(.(x,y),z) -> .(x,+(y,z))
   +(*(2(),x),x) -> *(3(),x)
   +(*(min(),x),x) -> 0()
   +(*(2(),v),*(min(),v)) -> v
   .(min(),3()) -> min()
   .(x,min()) -> .(+(min(),x),3())
   .(0(),x) -> x
   .(x,.(y,z)) -> .(+(x,y),z)
  Open