YES

Proof:
This system is quasi-decreasing.
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 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)
  gcd(x, x) -> x
  gcd(s(x), 0) -> s(x)
  gcd(0, s(y)) -> s(y)
  ?1(true, x, y) -> gcd(m(x, y), s(y))
  gcd(s(x), s(y)) -> ?1(lt(y, x), x, y)
  ?2(true, x, y) -> gcd(s(x), m(y, x))
  gcd(s(x), s(y)) -> ?2(lt(x, y), x, y)

 DP Processor:
  DPs:
   lt#(s(x),s(y)) -> lt#(x,y)
   m#(s(x),s(y)) -> m#(x,y)
   ?1#(true(),x,y) -> m#(x,y)
   ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
   gcd#(s(x),s(y)) -> lt#(y,x)
   gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
   ?2#(true(),x,y) -> m#(y,x)
   ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
   gcd#(s(x),s(y)) -> lt#(x,y)
   gcd#(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)
   gcd(x,x) -> x
   gcd(s(x),0()) -> s(x)
   gcd(0(),s(y)) -> s(y)
   ?1(true(),x,y) -> gcd(m(x,y),s(y))
   gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
   ?2(true(),x,y) -> gcd(s(x),m(y,x))
   gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
  TDG Processor:
   DPs:
    lt#(s(x),s(y)) -> lt#(x,y)
    m#(s(x),s(y)) -> m#(x,y)
    ?1#(true(),x,y) -> m#(x,y)
    ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
    gcd#(s(x),s(y)) -> lt#(y,x)
    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
    ?2#(true(),x,y) -> m#(y,x)
    ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
    gcd#(s(x),s(y)) -> lt#(x,y)
    gcd#(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)
    gcd(x,x) -> x
    gcd(s(x),0()) -> s(x)
    gcd(0(),s(y)) -> s(y)
    ?1(true(),x,y) -> gcd(m(x,y),s(y))
    gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
    ?2(true(),x,y) -> gcd(s(x),m(y,x))
    gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
   graph:
    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
    gcd#(s(x),s(y)) -> lt#(x,y)
    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) -> gcd#(s(x),s(y)) -> lt#(y,x)
    ?2#(true(),x,y) -> m#(y,x) -> m#(s(x),s(y)) -> m#(x,y)
    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
    gcd#(s(x),s(y)) -> lt#(x,y)
    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) -> gcd#(s(x),s(y)) -> lt#(y,x)
    ?1#(true(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
    ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
    ?2#(true(),x,y) -> m#(y,x)
    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y) ->
    ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y) -> ?1#(true(),x,y) -> m#(x,y)
    gcd#(s(x),s(y)) -> lt#(y,x) -> lt#(s(x),s(y)) -> lt#(x,y)
    gcd#(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: 6
    #arcs: 18/100
    DPs:
     ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
     gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
     ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
     gcd#(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)
     gcd(x,x) -> x
     gcd(s(x),0()) -> s(x)
     gcd(0(),s(y)) -> s(y)
     ?1(true(),x,y) -> gcd(m(x,y),s(y))
     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
     ?2(true(),x,y) -> gcd(s(x),m(y,x))
     gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
    Usable Rule Processor:
     DPs:
      ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
      gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
      ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
      gcd#(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 0]     [0 0]  
       [lt](x0, x1) = [0 1]x0 + [1 1]x1,
       
                 [1 0]     [0]
       [s](x0) = [1 1]x0 + [1],
       
                       
       [m](x0, x1) = x0,
       
             [2]
       [0] = [1],
       
       [?1#](x0, x1, x2) = [1 0]x1 + [2 2]x2 + [2],
       
       [gcd#](x0, x1) = [1 0]x0 + [0 2]x1,
       
       [?2#](x0, x1, x2) = [1 0]x1 + [2 2]x2,
       
                 [0]
       [false] = [0]
      orientation:
       ?2#(true(),x,y) = [1 0]x + [2 2]y >= [1 0]x + [0 2]y = gcd#(s(x),m(y,x))
       
       gcd#(s(x),s(y)) = [1 0]x + [2 2]y + [2] >= [1 0]x + [2 2]y + [2] = ?1#(lt(y,x),x,y)
       
       ?1#(true(),x,y) = [1 0]x + [2 2]y + [2] >= [1 0]x + [2 2]y + [2] = gcd#(m(x,y),s(y))
       
       gcd#(s(x),s(y)) = [1 0]x + [2 2]y + [2] >= [1 0]x + [2 2]y = ?2#(lt(x,y),x,y)
       
                     [2]    [2]      
       m(0(),s(y)) = [1] >= [1] = 0()
       
                            
       m(x,0()) = x >= x = x
       
                      [1 0]    [0]              
       m(s(x),s(y)) = [1 1]x + [1] >= x = m(x,y)
       
                   [0 0]    [0]    [0]          
       lt(x,0()) = [0 1]x + [3] >= [0] = false()
       
                      [0 0]    [0]    [0]         
       lt(0(),s(x)) = [2 1]x + [2] >= [0] = true()
       
                       [0 0]    [0 0]    [0]    [0 0]    [0 0]           
       lt(s(x),s(y)) = [1 1]x + [2 1]y + [2] >= [0 1]x + [1 1]y = lt(x,y)
      problem:
       DPs:
        ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
        gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
        ?1#(true(),x,y) -> gcd#(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#(true(),x,y) -> gcd#(s(x),m(y,x))
        gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
        ?1#(true(),x,y) -> gcd#(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)
        gcd(x,x) -> x
        gcd(s(x),0()) -> s(x)
        gcd(0(),s(y)) -> s(y)
        ?1(true(),x,y) -> gcd(m(x,y),s(y))
        gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
        ?2(true(),x,y) -> gcd(s(x),m(y,x))
        gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
       EDG Processor:
        DPs:
         ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
         gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
         ?1#(true(),x,y) -> gcd#(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)
         gcd(x,x) -> x
         gcd(s(x),0()) -> s(x)
         gcd(0(),s(y)) -> s(y)
         ?1(true(),x,y) -> gcd(m(x,y),s(y))
         gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
         ?2(true(),x,y) -> gcd(s(x),m(y,x))
         gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
        graph:
         ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
         gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
         ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
         gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
         gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y) -> ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
        SCC Processor:
         #sccs: 1
         #rules: 2
         #arcs: 3/9
         DPs:
          gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
          ?1#(true(),x,y) -> gcd#(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)
          gcd(x,x) -> x
          gcd(s(x),0()) -> s(x)
          gcd(0(),s(y)) -> s(y)
          ?1(true(),x,y) -> gcd(m(x,y),s(y))
          gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
          ?2(true(),x,y) -> gcd(s(x),m(y,x))
          gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
         Usable Rule Processor:
          DPs:
           gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
           ?1#(true(),x,y) -> gcd#(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)
          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],
            
                           [1 0]     [0 0]     [1]
            [lt](x0, x1) = [2 0]x0 + [0 2]x1 + [1],
            
                      [1 1]     [1]
            [s](x0) = [1 1]x0 + [0],
            
                          [1 0]     [0 0]     [0]
            [m](x0, x1) = [0 2]x0 + [1 0]x1 + [2],
            
                  [1]
            [0] = [0],
            
            [?1#](x0, x1, x2) = [3 0]x1 + [1 1]x2,
            
            [gcd#](x0, x1) = [3 0]x0 + [0 1]x1,
            
                      [0]
            [false] = [0]
           orientation:
            gcd#(s(x),s(y)) = [3 3]x + [1 1]y + [3] >= [3 0]x + [1 1]y = ?1#(lt(y,x),x,y)
            
            ?1#(true(),x,y) = [3 0]x + [1 1]y >= [3 0]x + [1 1]y = gcd#(m(x,y),s(y))
            
                        [1 0]    [1]    [0]          
            lt(x,0()) = [2 0]x + [1] >= [0] = false()
            
                           [0 0]    [2]    [0]         
            lt(0(),s(x)) = [2 2]x + [3] >= [0] = true()
            
                            [1 1]    [0 0]    [2]    [1 0]    [0 0]    [1]          
            lt(s(x),s(y)) = [2 2]x + [2 2]y + [3] >= [2 0]x + [0 2]y + [1] = lt(x,y)
            
                          [0 0]    [1]    [1]      
            m(0(),s(y)) = [1 1]y + [3] >= [0] = 0()
            
                       [1 0]    [0]         
            m(x,0()) = [0 2]x + [3] >= x = x
            
                           [1 1]    [0 0]    [1]    [1 0]    [0 0]    [0]         
            m(s(x),s(y)) = [2 2]x + [1 1]y + [3] >= [0 2]x + [1 0]y + [2] = m(x,y)
           problem:
            DPs:
             ?1#(true(),x,y) -> gcd#(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)
           Restore Modifier:
            DPs:
             ?1#(true(),x,y) -> gcd#(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)
             gcd(x,x) -> x
             gcd(s(x),0()) -> s(x)
             gcd(0(),s(y)) -> s(y)
             ?1(true(),x,y) -> gcd(m(x,y),s(y))
             gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
             ?2(true(),x,y) -> gcd(s(x),m(y,x))
             gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
            EDG Processor:
             DPs:
              ?1#(true(),x,y) -> gcd#(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)
              gcd(x,x) -> x
              gcd(s(x),0()) -> s(x)
              gcd(0(),s(y)) -> s(y)
              ?1(true(),x,y) -> gcd(m(x,y),s(y))
              gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
              ?2(true(),x,y) -> gcd(s(x),m(y,x))
              gcd(s(x),s(y)) -> ?2(lt(x,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)
     gcd(x,x) -> x
     gcd(s(x),0()) -> s(x)
     gcd(0(),s(y)) -> s(y)
     ?1(true(),x,y) -> gcd(m(x,y),s(y))
     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
     ?2(true(),x,y) -> gcd(s(x),m(y,x))
     gcd(s(x),s(y)) -> ?2(lt(x,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)
       gcd(x,x) -> x
       gcd(s(x),0()) -> s(x)
       gcd(0(),s(y)) -> s(y)
       ?1(true(),x,y) -> gcd(m(x,y),s(y))
       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
       ?2(true(),x,y) -> gcd(s(x),m(y,x))
       gcd(s(x),s(y)) -> ?2(lt(x,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)
     gcd(x,x) -> x
     gcd(s(x),0()) -> s(x)
     gcd(0(),s(y)) -> s(y)
     ?1(true(),x,y) -> gcd(m(x,y),s(y))
     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
     ?2(true(),x,y) -> gcd(s(x),m(y,x))
     gcd(s(x),s(y)) -> ?2(lt(x,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)
       gcd(x,x) -> x
       gcd(s(x),0()) -> s(x)
       gcd(0(),s(y)) -> s(y)
       ?1(true(),x,y) -> gcd(m(x,y),s(y))
       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
       ?2(true(),x,y) -> gcd(s(x),m(y,x))
       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
     Qed