YES

Problem:
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 -(s(x),s(y)) -> -(x,y)
 -(x,0()) -> x
 -(0(),x) -> 0()
 <(s(x),s(y)) -> <(x,y)
 <(0(),s(x)) -> true()
 <(x,0()) -> false()
 mod(0(),y) -> 0()
 mod(x,s(y)) -> if(<(x,s(y)),x,mod(-(x,s(y)),s(y)))
 mod(x,0()) -> x
 gcd(x,y) -> gcd(y,mod(x,y))
 gcd(x,0()) -> x
 gcd(0(),x) -> x

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 12
   0() <-3|[]- -(0(),0()) -4|[]-> 0()
   0() <-4|[]- -(0(),0()) -3|[]-> 0()
   0() <-8|[]- mod(0(),s(y)) -9|[]-> if(<(0(),s(y)),0(),mod(-(0(),s(y)),s(y)))
   0() <-8|[]- mod(0(),0()) -10|[]-> 0()
   if(<(0(),s(x607)),0(),mod(-(0(),s(x607)),s(x607))) <-9|[]- mod(0(),s(x607)) -8|[]-> 0()
   0() <-10|[]- mod(0(),0()) -8|[]-> 0()
   gcd(0(),mod(x,0())) <-11|[]- gcd(x,0()) -12|[]-> x
   gcd(x,mod(0(),x)) <-11|[]- gcd(0(),x) -13|[]-> x
   x <-12|[]- gcd(x,0()) -11|[]-> gcd(0(),mod(x,0()))
   0() <-12|[]- gcd(0(),0()) -13|[]-> 0()
   y <-13|[]- gcd(0(),y) -11|[]-> gcd(y,mod(0(),y))
   0() <-13|[]- gcd(0(),0()) -12|[]-> 0()
  Shift Processor lab=left (dd) (force):
   strict:
    -(0(),0()) -> 0()
    -(0(),0()) -> 0()
    -(0(),0()) -> 0()
    -(0(),0()) -> 0()
    mod(0(),s(y)) -> 0()
    mod(0(),s(y)) -> if(<(0(),s(y)),0(),mod(-(0(),s(y)),s(y)))
    if(<(0(),s(y)),0(),mod(-(0(),s(y)),s(y))) -> if(true(),0(),mod(-(0(),s(y)),s(y)))
    if(true(),0(),mod(-(0(),s(y)),s(y))) -> 0()
    mod(0(),0()) -> 0()
    mod(0(),0()) -> 0()
    mod(0(),s(x607)) -> if(<(0(),s(x607)),0(),mod(-(0(),s(x607)),s(x607)))
    mod(0(),s(x607)) -> 0()
    if(<(0(),s(x607)),0(),mod(-(0(),s(x607)),s(x607))) ->
    if(true(),0(),mod(-(0(),s(x607)),s(x607)))
    if(true(),0(),mod(-(0(),s(x607)),s(x607))) -> 0()
    mod(0(),0()) -> 0()
    mod(0(),0()) -> 0()
    gcd(x,0()) -> gcd(0(),mod(x,0()))
    gcd(x,0()) -> x
    gcd(0(),mod(x,0())) -> gcd(0(),x)
    gcd(0(),x) -> x
    gcd(0(),mod(x,0())) -> mod(x,0())
    mod(x,0()) -> x
    gcd(0(),x) -> gcd(x,mod(0(),x))
    gcd(0(),x) -> x
    gcd(x,mod(0(),x)) -> gcd(x,0())
    gcd(x,0()) -> x
    gcd(x,0()) -> x
    gcd(x,0()) -> gcd(0(),mod(x,0()))
    gcd(0(),mod(x,0())) -> gcd(0(),x)
    gcd(0(),x) -> x
    gcd(0(),mod(x,0())) -> mod(x,0())
    mod(x,0()) -> x
    gcd(0(),0()) -> 0()
    gcd(0(),0()) -> 0()
    gcd(0(),y) -> y
    gcd(0(),y) -> gcd(y,mod(0(),y))
    gcd(y,mod(0(),y)) -> gcd(y,0())
    gcd(y,0()) -> y
    gcd(0(),0()) -> 0()
    gcd(0(),0()) -> 0()
   weak:
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    -(s(x),s(y)) -> -(x,y)
    -(x,0()) -> x
    -(0(),x) -> 0()
    <(s(x),s(y)) -> <(x,y)
    <(0(),s(x)) -> true()
    <(x,0()) -> false()
    mod(0(),y) -> 0()
    mod(x,s(y)) -> if(<(x,s(y)),x,mod(-(x,s(y)),s(y)))
    mod(x,0()) -> x
    gcd(x,y) -> gcd(y,mod(x,y))
    gcd(x,0()) -> x
    gcd(0(),x) -> x
   Shift Processor (ldh) lab=left (force):
    strict:
     
    weak:
     
    Rule Labeling Processor:
     strict:
      
     weak:
      
     rule labeling (right):
      if(true(),x,y) -> x: 0
      if(false(),x,y) -> y: 0
      -(s(x),s(y)) -> -(x,y): 0
      -(x,0()) -> x: 0
      -(0(),x) -> 0(): 0
      <(s(x),s(y)) -> <(x,y): 0
      <(0(),s(x)) -> true(): 0
      <(x,0()) -> false(): 0
      mod(0(),y) -> 0(): 0
      mod(x,s(y)) -> if(<(x,s(y)),x,mod(-(x,s(y)),s(y))): 2
      mod(x,0()) -> x: 0
      gcd(x,y) -> gcd(y,mod(x,y)): 9
      gcd(x,0()) -> x: 8
      gcd(0(),x) -> x: 0
     Shift Processor lab=left (par):
      strict:
       
      weak:
       
      Decreasing Processor (par):
       The following diagrams are decreasing:
       peak:
        0() <-13|[==1,=>0]- gcd(0(),0()) -12|[==1,?=8]-> 0()
       joins (1):
        
        
       peak:
        y <-13|[==1,=>0]- gcd(0(),y) -11|[==1,?=9]-> gcd(y,mod(0(),y))
       joins (1):
        
        gcd(y,mod(0(),y)) -8|1[==1,=>0]-> gcd(y,0()) -12|[==1,?>8]-> y
       peak:
        0() <-12|[==1,=?8]- gcd(0(),0()) -13|[==1,>=0]-> 0()
       joins (1):
        
        
       peak:
        x <-12|[==1,=>8]- gcd(x,0()) -11|[==1,?=9]-> gcd(0(),mod(x,0()))
       joins (1):
        
        gcd(0(),mod(x,0())) -10|1[==1,>>0]-> gcd(0(),x) -13|[==1,>>0]-> x
       peak:
        gcd(x,mod(0(),x)) <-11|[==1,=?9]- gcd(0(),x) -13|[==1,>=0]-> x
       joins (1):
        gcd(x,mod(0(),x)) -8|1[==1,>=0]-> gcd(x,0()) -12|[==1,>?8]-> x
        
       peak:
        gcd(0(),mod(x,0())) <-11|[==1,=?9]- gcd(x,0()) -12|[==1,>=8]-> x
       joins (1):
        gcd(0(),mod(x,0())) -10|1[==1,>>0]-> gcd(0(),x) -13|[==1,>>0]-> x
        
       peak:
        0() <-10|[==1,==0]- mod(0(),0()) -8|[==1,==0]-> 0()
       joins (1):
        
        
       peak:
        if(<(0(),s(x607)),0(),mod(-(0(),s(x607)),s(x607))) <-9|[==1,=?2]- 
        mod(0(),s(x607)) -8|[==1,>=0]-> 0()
       joins (1):
        if(<(0(),s(x607)),0(),mod(-(0(),s(x607)),s(x607))) -6|0[==1,>=0]-> 
         if(true(),0(),mod(-(0(),s(x607)),s(x607))) -0|[==1,>=0]-> 0()
        
       peak:
        0() <-8|[==1,==0]- mod(0(),0()) -10|[==1,==0]-> 0()
       joins (1):
        
        
       peak:
        0() <-8|[==1,=>0]- mod(0(),s(y)) -9|[==1,?=2]-> if(<(0(),s(y)),0(),mod(-(0(),s(y)),s(y)))
       joins (1):
        
        if(<(0(),s(y)),0(),mod(-(0(),s(y)),s(y))) -6|0[==1,=>0]-> if(
                                                                    true(),
                                                                    0(),
                                                                    mod(-(0(),s(y)),s(y))) -0|
                                                                  [==1,=>0]-> 
                                                                  0()
       peak:
        0() <-4|[==1,==0]- -(0(),0()) -3|[==1,==0]-> 0()
       joins (1):
        
        
       peak:
        0() <-3|[==1,==0]- -(0(),0()) -4|[==1,==0]-> 0()
       joins (1):
        
        
       Qed