MAYBE
MAYBE
TRS:
 {
                           app'(app'(app'(app'(filter2(), true()), f), x), xs
                           )
  -> app'(app'(add(), x), app'(app'(filter(), f), xs)),
                          app'(app'(app'(app'(filter2(), false()), f), x), xs
                          )
  -> app'(app'(filter(), f), xs),
                 app'(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)
                 )
  -> app'(app'(rm(), n), x),
                app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)
                )
  -> app'(app'(add(), m), app'(app'(rm(), n), x)),
            app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y
            )
  ->
  app'(
      app'(add(), n),
      app'(
          app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)),
          nil()
      )
  ),
           app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y
           )
  -> app'(app'(minsort(), x), app'(app'(add(), n), y)),
                                  app'(app'(eq(), app'(s(), x)), app'(s(), y)
                                  )
  -> app'(app'(eq(), x), y),
                                           app'(app'(eq(), app'(s(), x)), 0()
                                           )
  -> false(),
                                           app'(app'(eq(), 0()), app'(s(), x)
                                           )
  -> false(),
                                                    app'(app'(eq(), 0()), 0()
                                                    )
  -> true(),
                                  app'(app'(le(), app'(s(), x)), app'(s(), y)
                                  )
  -> app'(app'(le(), x), y),
                                           app'(app'(le(), app'(s(), x)), 0()
                                           )
  -> false(),
                                                      app'(app'(le(), 0()), y
                                                      )
  -> true(),
                                 app'(app'(app(), app'(app'(add(), n), x)), y
                                 )
  -> app'(app'(add(), n), app'(app'(app(), x), y)),
                                                   app'(app'(app(), nil()), y
                                                   )
  -> y,
   app'(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))
   )
  -> app'(min(), app'(app'(add(), n), x)),
  app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))
  ) -> app'(min(), app'(app'(add(), m), x)),
                                  app'(app'(rm(), n), app'(app'(add(), m), x)
                                  )
  ->
  app'(
      app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)
  ),
                                                    app'(app'(rm(), n), nil()
                                                    )
  -> nil(),
                             app'(app'(minsort(), app'(app'(add(), n), x)), y
                             )
  ->
  app'(
      app'(
          app'(
              if_minsort(),
              app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))
          ), app'(app'(add(), n), x)
      ), y
  ),
                                           app'(app'(minsort(), nil()), nil()
                                           )
  -> nil(),
                                app'(app'(map(), f), app'(app'(add(), x), xs)
                                )
  -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)),
                                                   app'(app'(map(), f), nil()
                                                   )
  -> nil(),
                             app'(app'(filter(), f), app'(app'(add(), x), xs)
                             )
  -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs),
                                                app'(app'(filter(), f), nil()
                                                )
  -> nil(),
                    app'(min(), app'(app'(add(), n), app'(app'(add(), m), x))
                    )
  ->
  app'(
      app'(if_min(), app'(app'(le(), n), m)),
      app'(app'(add(), n), app'(app'(add(), m), x))
  ),
                                      app'(min(), app'(app'(add(), n), nil())
                                      )
  -> n
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                             app'(
                                 app'(app'(app'(filter2(), true()), f), x),
                                 xs
                             )
    -> app'(app'(add(), x), app'(app'(filter(), f), xs)),
                            app'(
                                app'(app'(app'(filter2(), false()), f), x),
                                xs
                            )
    -> app'(app'(filter(), f), xs),
                   app'(
                       app'(app'(if_rm(), true()), n),
                       app'(app'(add(), m), x)
                   )
    -> app'(app'(rm(), n), x),
                  app'(
                      app'(app'(if_rm(), false()), n),
                      app'(app'(add(), m), x)
                  )
    -> app'(app'(add(), m), app'(app'(rm(), n), x)),
              app'(
                  app'(app'(if_minsort(), true()), app'(app'(add(), n), x)),
                  y
              )
    ->
    app'(
        app'(add(), n),
        app'(
            app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)),
            nil()
        )
    ),
             app'(
                 app'(app'(if_minsort(), false()), app'(app'(add(), n), x)),
                 y
             )
    -> app'(app'(minsort(), x), app'(app'(add(), n), y)),
                                    app'(
                                        app'(eq(), app'(s(), x)),
                                        app'(s(), y)
                                    )
    -> app'(app'(eq(), x), y),
                                             app'(
                                                 app'(eq(), app'(s(), x)),
                                                 0()
                                             )
    -> false(),
                                             app'(
                                                 app'(eq(), 0()),
                                                 app'(s(), x)
                                             )
    -> false(),
                                                      app'(
                                                          app'(eq(), 0()),
                                                          0()
                                                      )
    -> true(),
                                    app'(
                                        app'(le(), app'(s(), x)),
                                        app'(s(), y)
                                    )
    -> app'(app'(le(), x), y),
                                             app'(
                                                 app'(le(), app'(s(), x)),
                                                 0()
                                             )
    -> false(),
                                                        app'(
                                                            app'(le(), 0()),
                                                            y
                                                        )
    -> true(),
                                   app'(
                                       app'(app(), app'(app'(add(), n), x)),
                                       y
                                   )
    -> app'(app'(add(), n), app'(app'(app(), x), y)),
                                                     app'(
                                                         app'(app(), nil()),
                                                         y
                                                     )
    -> y,
     app'(
         app'(if_min(), true()),
         app'(app'(add(), n), app'(app'(add(), m), x))
     )
    -> app'(min(), app'(app'(add(), n), x)),
    app'(
        app'(if_min(), false()),
        app'(app'(add(), n), app'(app'(add(), m), x))
    ) -> app'(min(), app'(app'(add(), m), x)),
                                    app'(
                                        app'(rm(), n),
                                        app'(app'(add(), m), x)
                                    )
    ->
    app'(
        app'(app'(if_rm(), app'(app'(eq(), n), m)), n),
        app'(app'(add(), m), x)
    ),
                                                      app'(
                                                          app'(rm(), n),
                                                          nil()
                                                      )
    -> nil(),
                               app'(
                                   app'(minsort(), app'(app'(add(), n), x)),
                                   y
                               )
    ->
    app'(
        app'(
            app'(
                if_minsort(),
                app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))
            ), app'(app'(add(), n), x)
        ), y
    ),
                                             app'(
                                                 app'(minsort(), nil()),
                                                 nil()
                                             )
    -> nil(),
                                  app'(
                                      app'(map(), f),
                                      app'(app'(add(), x), xs)
                                  )
    -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)),
                                                     app'(
                                                         app'(map(), f),
                                                         nil()
                                                     )
    -> nil(),
                               app'(
                                   app'(filter(), f),
                                   app'(app'(add(), x), xs)
                               )
    -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs),
                                                  app'(
                                                      app'(filter(), f),
                                                      nil()
                                                  )
    -> nil(),
                      app'(
                          min(),
                          app'(app'(add(), n), app'(app'(add(), m), x))
                      )
    ->
    app'(
        app'(if_min(), app'(app'(le(), n), m)),
        app'(app'(add(), n), app'(app'(add(), m), x))
    ),
                                        app'(
                                            min(),
                                            app'(app'(add(), n), nil())
                                        )
    -> n
   }
  Fail