YES
TRS:
 {                               app(app(lt(), y), 0()) -> false(),
               app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y),
                       app(app(lt(), 0()), app(s(), y)) -> true(),
                                   app(app(eq(), x), x) -> true(),
                       app(app(eq(), app(s(), x)), 0()) -> false(),
                       app(app(eq(), 0()), app(s(), x)) -> false(),
  app(app(member(), w), app(app(app(fork(), x), y), z)) -> app(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))),
                          app(app(member(), w), null()) -> false()}
 DP:
  Strict:
   {             app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y),
                 app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(lt(), x),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z)),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(lt(), w), y),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(eq(), w), y),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(if(), app(app(eq(), w), y)), true()),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(lt(), w),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(eq(), w),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(if(), app(app(lt(), w), y)),
    app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(if(), app(app(eq(), w), y))}
  Weak:
  {                               app(app(lt(), y), 0()) -> false(),
                app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y),
                        app(app(lt(), 0()), app(s(), y)) -> true(),
                                    app(app(eq(), x), x) -> true(),
                        app(app(eq(), app(s(), x)), 0()) -> false(),
                        app(app(eq(), 0()), app(s(), x)) -> false(),
   app(app(member(), w), app(app(app(fork(), x), y), z)) -> app(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))),
                           app(app(member(), w), null()) -> false()}
  EDG:
   {(app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(if(), app(app(eq(), w), y)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(if(), app(app(lt(), w), y)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(eq(), w))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(lt(), w))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(if(), app(app(eq(), w), y)), true()))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(eq(), w), y))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(lt(), w), y))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))))
    (app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(lt(), x))
    (app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(if(), app(app(eq(), w), y)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(if(), app(app(lt(), w), y)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(eq(), w))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(lt(), w))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(if(), app(app(eq(), w), y)), true()))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(eq(), w), y))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(lt(), w), y))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z)))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(lt(), w), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y))
    (app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(lt(), w), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(lt(), x))}
   SCCS:
    Scc:
     {app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x),
      app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z)}
    Scc:
     {app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y)}
    SCC:
     Strict:
      {app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), x),
       app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z)}
     Weak:
     {                               app(app(lt(), y), 0()) -> false(),
                   app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y),
                           app(app(lt(), 0()), app(s(), y)) -> true(),
                                       app(app(eq(), x), x) -> true(),
                           app(app(eq(), app(s(), x)), 0()) -> false(),
                           app(app(eq(), 0()), app(s(), x)) -> false(),
      app(app(member(), w), app(app(app(fork(), x), y), z)) -> app(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))),
                              app(app(member(), w), null()) -> false()}
     SPSC:
      Simple Projection:
       pi(app#) = 1
      Strict:
       {app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z)}
      EDG:
       {(app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z), app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z))}
       SCCS:
        Scc:
         {app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z)}
        SCC:
         Strict:
          {app#(app(member(), w), app(app(app(fork(), x), y), z)) -> app#(app(member(), w), z)}
         Weak:
         {                               app(app(lt(), y), 0()) -> false(),
                       app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y),
                               app(app(lt(), 0()), app(s(), y)) -> true(),
                                           app(app(eq(), x), x) -> true(),
                               app(app(eq(), app(s(), x)), 0()) -> false(),
                               app(app(eq(), 0()), app(s(), x)) -> false(),
          app(app(member(), w), app(app(app(fork(), x), y), z)) -> app(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))),
                                  app(app(member(), w), null()) -> false()}
         SPSC:
          Simple Projection:
           pi(app#) = 1
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y)}
     Weak:
     {                               app(app(lt(), y), 0()) -> false(),
                   app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y),
                           app(app(lt(), 0()), app(s(), y)) -> true(),
                                       app(app(eq(), x), x) -> true(),
                           app(app(eq(), app(s(), x)), 0()) -> false(),
                           app(app(eq(), 0()), app(s(), x)) -> false(),
      app(app(member(), w), app(app(app(fork(), x), y), z)) -> app(app(app(if(), app(app(lt(), w), y)), app(app(member(), w), x)), app(app(app(if(), app(app(eq(), w), y)), true()), app(app(member(), w), z))),
                              app(app(member(), w), null()) -> false()}
     SPSC:
      Simple Projection:
       pi(app#) = 1
      Strict:
       {}
      Qed