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 (critical pair closing system, Thm 2.11):
  <(0(),s(x617)) -> true()
  if(true(),0(),x621) -> 0()
  gcd(0(),x630) -> x630
  mod(x631,0()) -> x631
  mod(0(),x632) -> 0()
  gcd(x633,0()) -> x633
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [gcd](x0, x1) = x0 + 4x1 + 3,
    
    [if](x0, x1, x2) = x0 + x1 + 2x2,
    
    [s](x0) = 2x0 + 1,
    
    [0] = 0,
    
    [true] = 4,
    
    [mod](x0, x1) = 2x0 + 2x1,
    
    [<](x0, x1) = x0 + 6x1 + 2
   orientation:
    <(0(),s(x617)) = 12x617 + 8 >= 4 = true()
    
    if(true(),0(),x621) = 2x621 + 4 >= 0 = 0()
    
    gcd(0(),x630) = 4x630 + 3 >= x630 = x630
    
    mod(x631,0()) = 2x631 >= x631 = x631
    
    mod(0(),x632) = 2x632 >= 0 = 0()
    
    gcd(x633,0()) = x633 + 3 >= x633 = x633
   problem:
    mod(x631,0()) -> x631
    mod(0(),x632) -> 0()
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [0] = 2,
     
     [mod](x0, x1) = x0 + 4x1
    orientation:
     mod(x631,0()) = x631 + 8 >= x631 = x631
     
     mod(0(),x632) = 4x632 + 2 >= 2 = 0()
    problem:
     mod(0(),x632) -> 0()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [0] = 0,
      
      [mod](x0, x1) = x0 + 4x1 + 1
     orientation:
      mod(0(),x632) = 4x632 + 1 >= 0 = 0()
     problem:
      
     Qed