MAYBE
MAYBE
TRS:
 {
                  *(0(), x) -> 0(),
                  *(1(), x) -> x,
              *(.(x, y), z) -> .(*(x, z), *(y, z)),
                *(2(), 2()) -> .(1(), 0()),
              *(2(), min()) -> .(min(), 2()),
            *(min(), min()) -> 1(),
                  *(3(), x) -> .(x, *(min(), x)),
              *(+(y, z), x) -> +(*(x, y), *(x, z)),
              .(x, .(y, z)) -> .(+(x, y), z),
                .(x, min()) -> .(+(min(), x), 3()),
                  .(0(), x) -> x,
              .(min(), 3()) -> min(),
                    +(x, x) -> *(2(), x),
                  +(0(), x) -> x,
            +(*(2(), x), x) -> *(3(), x),
  +(*(2(), v), *(min(), v)) -> v,
          +(*(min(), x), x) -> 0(),
                +(1(), 2()) -> 3(),
              +(1(), min()) -> 0(),
              +(.(x, y), z) -> .(x, +(y, z)),
              +(2(), min()) -> 1(),
                  +(3(), x) -> .(1(), +(min(), x))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                    *(0(), x) -> 0(),
                    *(1(), x) -> x,
                *(.(x, y), z) -> .(*(x, z), *(y, z)),
                  *(2(), 2()) -> .(1(), 0()),
                *(2(), min()) -> .(min(), 2()),
              *(min(), min()) -> 1(),
                    *(3(), x) -> .(x, *(min(), x)),
                *(+(y, z), x) -> +(*(x, y), *(x, z)),
                .(x, .(y, z)) -> .(+(x, y), z),
                  .(x, min()) -> .(+(min(), x), 3()),
                    .(0(), x) -> x,
                .(min(), 3()) -> min(),
                      +(x, x) -> *(2(), x),
                    +(0(), x) -> x,
              +(*(2(), x), x) -> *(3(), x),
    +(*(2(), v), *(min(), v)) -> v,
            +(*(min(), x), x) -> 0(),
                  +(1(), 2()) -> 3(),
                +(1(), min()) -> 0(),
                +(.(x, y), z) -> .(x, +(y, z)),
                +(2(), min()) -> 1(),
                    +(3(), x) -> .(1(), +(min(), x))
   }
  Fail