YES

Proof:
This system is confluent.
By \cite{ALS94}, Theorem 4.1.
This system is of type 3 or smaller.
This system is strongly deterministic.
All 2 critical pairs are joinable.
pair(0, s(x)) = pair(s(y), $1) <= lt(x, $2) = false, div(m(x, $2), s($2)) = pair(y, $1), lt(x, $2) = true:
This critical pair is unfeasible.
pair(s(x), y) = pair(0, s($1)) <= lt($1, $2) = true, lt($1, $2) = false, div(m($1, $2), s($2)) = pair(x, y):
This critical pair is unfeasible.
This system is of type 3 or smaller.
This system is deterministic.
Call external tool:
ttt2 - trs 30
Input:
  lt(x, 0) -> false
  lt(0, s(x)) -> true
  lt(s(x), s(y)) -> lt(x, y)
  m(0, s(y)) -> 0
  m(x, 0) -> x
  m(s(x), s(y)) -> m(x, y)
  div(0, s(x)) -> pair(0, 0)
  div(s(x), s(y)) -> pair(0, s(x))
  div(s(x), s(y)) -> lt(x, y)
  div(s(x), s(y)) -> pair(s(div(m(x, y), s(y))), div(m(x, y), s(y)))
  div(s(x), s(y)) -> div(m(x, y), s(y))
  m(x, y) -> x
  m(x, y) -> y
  pair(x, y) -> x
  pair(x, y) -> y
  s(x) -> x
  div(x, y) -> x
  div(x, y) -> y
  lt(x, y) -> x
  lt(x, y) -> y

 Unfolding Processor:
  loop length: 2
  terms:
   div(s(x588),s(s(x588)))
   pair(s(div(m(x588,s(x588)),s(s(x588)))),div(m(x588,s(x588)),s(s(x588))))
  context: pair(s([]),div(m(x588,s(x588)),s(s(x588))))
  substitution:
   x588 -> x588
  Qed
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to optimized U(R).
Call external tool:
ttt2 - trs 30
Input:
  lt(x, 0) -> false
  lt(0, s(x)) -> true
  lt(s(x), s(y)) -> lt(x, y)
  m(0, s(y)) -> 0
  m(x, 0) -> x
  m(s(x), s(y)) -> m(x, y)
  div(0, s(x)) -> pair(0, 0)
  ?2(true, x, y) -> pair(0, s(x))
  div(s(x), s(y)) -> ?2(lt(x, y), x, y)
  ?1(pair(q, r), x, y) -> pair(s(q), r)
  ?2(false, x, y) -> ?1(div(m(x, y), s(y)), x, y)

 DP Processor:
  DPs:
   lt#(s(x),s(y)) -> lt#(x,y)
   m#(s(x),s(y)) -> m#(x,y)
   div#(s(x),s(y)) -> lt#(x,y)
   div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
   ?2#(false(),x,y) -> m#(x,y)
   ?2#(false(),x,y) -> div#(m(x,y),s(y))
   ?2#(false(),x,y) -> ?1#(div(m(x,y),s(y)),x,y)
  TRS:
   lt(x,0()) -> false()
   lt(0(),s(x)) -> true()
   lt(s(x),s(y)) -> lt(x,y)
   m(0(),s(y)) -> 0()
   m(x,0()) -> x
   m(s(x),s(y)) -> m(x,y)
   div(0(),s(x)) -> pair(0(),0())
   ?2(true(),x,y) -> pair(0(),s(x))
   div(s(x),s(y)) -> ?2(lt(x,y),x,y)
   ?1(pair(q,r),x,y) -> pair(s(q),r)
   ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
  TDG Processor:
   DPs:
    lt#(s(x),s(y)) -> lt#(x,y)
    m#(s(x),s(y)) -> m#(x,y)
    div#(s(x),s(y)) -> lt#(x,y)
    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
    ?2#(false(),x,y) -> m#(x,y)
    ?2#(false(),x,y) -> div#(m(x,y),s(y))
    ?2#(false(),x,y) -> ?1#(div(m(x,y),s(y)),x,y)
   TRS:
    lt(x,0()) -> false()
    lt(0(),s(x)) -> true()
    lt(s(x),s(y)) -> lt(x,y)
    m(0(),s(y)) -> 0()
    m(x,0()) -> x
    m(s(x),s(y)) -> m(x,y)
    div(0(),s(x)) -> pair(0(),0())
    ?2(true(),x,y) -> pair(0(),s(x))
    div(s(x),s(y)) -> ?2(lt(x,y),x,y)
    ?1(pair(q,r),x,y) -> pair(s(q),r)
    ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
   graph:
    ?2#(false(),x,y) -> div#(m(x,y),s(y)) ->
    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
    ?2#(false(),x,y) -> div#(m(x,y),s(y)) -> div#(s(x),s(y)) -> lt#(x,y)
    ?2#(false(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
    ?2#(false(),x,y) -> ?1#(div(m(x,y),s(y)),x,y)
    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
    ?2#(false(),x,y) -> div#(m(x,y),s(y))
    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> ?2#(false(),x,y) -> m#(x,y)
    div#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
    m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 9/49
    DPs:
     ?2#(false(),x,y) -> div#(m(x,y),s(y))
     div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
    TRS:
     lt(x,0()) -> false()
     lt(0(),s(x)) -> true()
     lt(s(x),s(y)) -> lt(x,y)
     m(0(),s(y)) -> 0()
     m(x,0()) -> x
     m(s(x),s(y)) -> m(x,y)
     div(0(),s(x)) -> pair(0(),0())
     ?2(true(),x,y) -> pair(0(),s(x))
     div(s(x),s(y)) -> ?2(lt(x,y),x,y)
     ?1(pair(q,r),x,y) -> pair(s(q),r)
     ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
    Usable Rule Processor:
     DPs:
      ?2#(false(),x,y) -> div#(m(x,y),s(y))
      div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
     TRS:
      m(0(),s(y)) -> 0()
      m(x,0()) -> x
      m(s(x),s(y)) -> m(x,y)
      lt(x,0()) -> false()
      lt(0(),s(x)) -> true()
      lt(s(x),s(y)) -> lt(x,y)
     Matrix Interpretation Processor: dim=2
      
      usable rules:
       m(0(),s(y)) -> 0()
       m(x,0()) -> x
       m(s(x),s(y)) -> m(x,y)
      interpretation:
                [0]
       [true] = [0],
       
                      [0]
       [lt](x0, x1) = [0],
       
                 [3 0]     [1]
       [s](x0) = [0 1]x0 + [0],
       
                     [1 0]  
       [m](x0, x1) = [1 2]x0,
       
             [0]
       [0] = [0],
       
       [div#](x0, x1) = [1 0]x0 + [0 2]x1 + [2],
       
       [?2#](x0, x1, x2) = [1 0]x1 + [0 2]x2 + [2],
       
                 [0]
       [false] = [0]
      orientation:
       ?2#(false(),x,y) = [1 0]x + [0 2]y + [2] >= [1 0]x + [0 2]y + [2] = div#(m(x,y),s(y))
       
       div#(s(x),s(y)) = [3 0]x + [0 2]y + [3] >= [1 0]x + [0 2]y + [2] = ?2#(lt(x,y),x,y)
       
                     [0]    [0]      
       m(0(),s(y)) = [0] >= [0] = 0()
       
                  [1 0]          
       m(x,0()) = [1 2]x >= x = x
       
                      [3 0]    [1]    [1 0]          
       m(s(x),s(y)) = [3 2]x + [1] >= [1 2]x = m(x,y)
       
                   [0]    [0]          
       lt(x,0()) = [0] >= [0] = false()
       
                      [0]    [0]         
       lt(0(),s(x)) = [0] >= [0] = true()
       
                       [0]    [0]          
       lt(s(x),s(y)) = [0] >= [0] = lt(x,y)
      problem:
       DPs:
        ?2#(false(),x,y) -> div#(m(x,y),s(y))
       TRS:
        m(0(),s(y)) -> 0()
        m(x,0()) -> x
        m(s(x),s(y)) -> m(x,y)
        lt(x,0()) -> false()
        lt(0(),s(x)) -> true()
        lt(s(x),s(y)) -> lt(x,y)
      Restore Modifier:
       DPs:
        ?2#(false(),x,y) -> div#(m(x,y),s(y))
       TRS:
        lt(x,0()) -> false()
        lt(0(),s(x)) -> true()
        lt(s(x),s(y)) -> lt(x,y)
        m(0(),s(y)) -> 0()
        m(x,0()) -> x
        m(s(x),s(y)) -> m(x,y)
        div(0(),s(x)) -> pair(0(),0())
        ?2(true(),x,y) -> pair(0(),s(x))
        div(s(x),s(y)) -> ?2(lt(x,y),x,y)
        ?1(pair(q,r),x,y) -> pair(s(q),r)
        ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
       EDG Processor:
        DPs:
         ?2#(false(),x,y) -> div#(m(x,y),s(y))
        TRS:
         lt(x,0()) -> false()
         lt(0(),s(x)) -> true()
         lt(s(x),s(y)) -> lt(x,y)
         m(0(),s(y)) -> 0()
         m(x,0()) -> x
         m(s(x),s(y)) -> m(x,y)
         div(0(),s(x)) -> pair(0(),0())
         ?2(true(),x,y) -> pair(0(),s(x))
         div(s(x),s(y)) -> ?2(lt(x,y),x,y)
         ?1(pair(q,r),x,y) -> pair(s(q),r)
         ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
        graph:
         
        Qed
    
    DPs:
     m#(s(x),s(y)) -> m#(x,y)
    TRS:
     lt(x,0()) -> false()
     lt(0(),s(x)) -> true()
     lt(s(x),s(y)) -> lt(x,y)
     m(0(),s(y)) -> 0()
     m(x,0()) -> x
     m(s(x),s(y)) -> m(x,y)
     div(0(),s(x)) -> pair(0(),0())
     ?2(true(),x,y) -> pair(0(),s(x))
     div(s(x),s(y)) -> ?2(lt(x,y),x,y)
     ?1(pair(q,r),x,y) -> pair(s(q),r)
     ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(m#) = 0
     problem:
      DPs:
       
      TRS:
       lt(x,0()) -> false()
       lt(0(),s(x)) -> true()
       lt(s(x),s(y)) -> lt(x,y)
       m(0(),s(y)) -> 0()
       m(x,0()) -> x
       m(s(x),s(y)) -> m(x,y)
       div(0(),s(x)) -> pair(0(),0())
       ?2(true(),x,y) -> pair(0(),s(x))
       div(s(x),s(y)) -> ?2(lt(x,y),x,y)
       ?1(pair(q,r),x,y) -> pair(s(q),r)
       ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
     Qed
    
    DPs:
     lt#(s(x),s(y)) -> lt#(x,y)
    TRS:
     lt(x,0()) -> false()
     lt(0(),s(x)) -> true()
     lt(s(x),s(y)) -> lt(x,y)
     m(0(),s(y)) -> 0()
     m(x,0()) -> x
     m(s(x),s(y)) -> m(x,y)
     div(0(),s(x)) -> pair(0(),0())
     ?2(true(),x,y) -> pair(0(),s(x))
     div(s(x),s(y)) -> ?2(lt(x,y),x,y)
     ?1(pair(q,r),x,y) -> pair(s(q),r)
     ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(lt#) = 0
     problem:
      DPs:
       
      TRS:
       lt(x,0()) -> false()
       lt(0(),s(x)) -> true()
       lt(s(x),s(y)) -> lt(x,y)
       m(0(),s(y)) -> 0()
       m(x,0()) -> x
       m(s(x),s(y)) -> m(x,y)
       div(0(),s(x)) -> pair(0(),0())
       ?2(true(),x,y) -> pair(0(),s(x))
       div(s(x),s(y)) -> ?2(lt(x,y),x,y)
       ?1(pair(q,r),x,y) -> pair(s(q),r)
       ?2(false(),x,y) -> ?1(div(m(x,y),s(y)),x,y)
     Qed