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 + 1,
    
    [mod](x0, x1) = x0 + 2x1 + 1,
    
    [<](x0, x1) = x0 + 2x1 + 4,
    
    [0] = 4,
    
    [s](x0) = 2x0 + 4,
    
    [if](x0, x1, x2) = x0 + x1 + x2 + 7,
    
    [true] = 3
   orientation:
    <(0(),s(x617)) = 4x617 + 16 >= 3 = true()
    
    if(true(),0(),x621) = x621 + 14 >= 4 = 0()
    
    gcd(0(),x630) = 4x630 + 5 >= x630 = x630
    
    mod(x631,0()) = x631 + 9 >= x631 = x631
    
    mod(0(),x632) = 2x632 + 5 >= 4 = 0()
    
    gcd(x633,0()) = x633 + 17 >= x633 = x633
   problem:
    
   Qed