YES
We show the termination of the TRS R:

  min(x,|0|()) -> |0|()
  min(|0|(),y) -> |0|()
  min(s(x),s(y)) -> s(min(x,y))
  max(x,|0|()) -> x
  max(|0|(),y) -> y
  max(s(x),s(y)) -> s(max(x,y))
  minus(x,|0|()) -> x
  minus(s(x),s(y)) -> s(minus(x,y))
  gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
  transform(x) -> s(s(x))
  transform(cons(x,y)) -> cons(cons(x,x),x)
  transform(cons(x,y)) -> y
  transform(s(x)) -> s(s(transform(x)))
  cons(x,y) -> y
  cons(x,cons(y,s(z))) -> cons(y,x)
  cons(cons(x,z),s(y)) -> transform(x)


-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: min#(s(x),s(y)) -> min#(x,y)
p2: max#(s(x),s(y)) -> max#(x,y)
p3: minus#(s(x),s(y)) -> minus#(x,y)
p4: gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
p5: gcd#(s(x),s(y)) -> minus#(max(x,y),min(x,transform(y)))
p6: gcd#(s(x),s(y)) -> max#(x,y)
p7: gcd#(s(x),s(y)) -> min#(x,transform(y))
p8: gcd#(s(x),s(y)) -> transform#(y)
p9: gcd#(s(x),s(y)) -> min#(x,y)
p10: transform#(cons(x,y)) -> cons#(cons(x,x),x)
p11: transform#(cons(x,y)) -> cons#(x,x)
p12: transform#(s(x)) -> transform#(x)
p13: cons#(x,cons(y,s(z))) -> cons#(y,x)
p14: cons#(cons(x,z),s(y)) -> transform#(x)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The estimated dependency graph contains the following SCCs:

  {p4}
  {p1}
  {p2}
  {p3}
  {p10, p11, p12, p13, p14}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        gcd#_A(x1,x2) = max{x1 + 16, x2 - 3}
        s_A(x1) = max{41, x1 + 24}
        minus_A(x1,x2) = max{7, x1 + 4}
        max_A(x1,x2) = max{2, x1, x2}
        min_A(x1,x2) = max{32, x1 + 15}
        transform_A(x1) = 0
        |0|_A = 16
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          gcd#_A(x1,x2) = max{0, x1 - 77, x2 - 87}
          s_A(x1) = max{120, x1 + 76}
          minus_A(x1,x2) = max{22, x1 + 21}
          max_A(x1,x2) = max{46, x1 + 1, x2 + 34}
          min_A(x1,x2) = max{12, x1 + 10, x2 - 202}
          transform_A(x1) = 196
          |0|_A = 0
          gcd#!_A(x1,x2) = max{x1 + 332, x2 + 125}
          s!_A(x1) = x1 + 5
          minus!_A(x1,x2) = max{28, x1 - 47}
          max!_A(x1,x2) = max{30, x1 + 26, x2 - 24}
          min!_A(x1,x2) = max{x1, x2 + 4}
          transform!_A(x1) = max{278, x1 + 202}
          |0|!_A = 3
  
    partial status:
  
      pi(gcd#) = []
      pi(s) = []
      pi(minus) = [1]
      pi(max) = [1, 2]
      pi(min) = [1]
      pi(transform) = []
      pi(|0|) = []

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: min#(s(x),s(y)) -> min#(x,y)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The set of usable rules consists of

  r1, r2

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        min#_A(x1,x2) = max{1, x2 - 1}
        s_A(x1) = x1 + 5
        min_A(x1,x2) = max{17, x1 - 20, x2 - 10}
        |0|_A = 0
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          min#_A(x1,x2) = 0
          s_A(x1) = max{3, x1 - 30}
          min_A(x1,x2) = max{29, x1 - 5, x2 - 6}
          |0|_A = 0
          min#!_A(x1,x2) = x2 + 33
          s!_A(x1) = max{1, x1 - 98}
          min!_A(x1,x2) = max{2, x1 - 104, x2 - 34}
          |0|!_A = 0
  
    partial status:
  
      pi(min#) = []
      pi(s) = []
      pi(min) = []
      pi(|0|) = []

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: max#(s(x),s(y)) -> max#(x,y)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The set of usable rules consists of

  r1, r2

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        max#_A(x1,x2) = max{1, x1 - 1, x2 - 5}
        s_A(x1) = max{10, x1 + 7}
        min_A(x1,x2) = max{23, x1 - 19, x2 - 28}
        |0|_A = 0
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          max#_A(x1,x2) = 0
          s_A(x1) = max{4, x1 - 22}
          min_A(x1,x2) = max{21, x1 - 6, x2 - 10}
          |0|_A = 0
          max#!_A(x1,x2) = max{2, x1 - 1}
          s!_A(x1) = max{1, x1 - 71}
          min!_A(x1,x2) = max{2, x2 - 112}
          |0|!_A = 1
  
    partial status:
  
      pi(max#) = []
      pi(s) = [1]
      pi(min) = []
      pi(|0|) = []

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: minus#(s(x),s(y)) -> minus#(x,y)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The set of usable rules consists of

  r1, r2

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        minus#_A(x1,x2) = max{1, x1 - 1, x2 - 1}
        s_A(x1) = x1 + 6
        min_A(x1,x2) = max{17, x1 - 9, x2 - 7}
        |0|_A = 0
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          minus#_A(x1,x2) = 0
          s_A(x1) = max{3, x1 - 17}
          min_A(x1,x2) = max{16, x1 - 5, x2 - 5}
          |0|_A = 4
          minus#!_A(x1,x2) = x2 + 22
          s!_A(x1) = max{3, x1 - 114}
          min!_A(x1,x2) = max{1, x1 - 103, x2 - 117}
          |0|!_A = 0
  
    partial status:
  
      pi(minus#) = []
      pi(s) = []
      pi(min) = []
      pi(|0|) = []

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: transform#(cons(x,y)) -> cons#(cons(x,x),x)
p2: cons#(cons(x,z),s(y)) -> transform#(x)
p3: transform#(s(x)) -> transform#(x)
p4: transform#(cons(x,y)) -> cons#(x,x)
p5: cons#(x,cons(y,s(z))) -> cons#(y,x)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The set of usable rules consists of

  r1, r2, r10, r11, r12, r13, r14, r15, r16

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        transform#_A(x1) = 20
        cons_A(x1,x2) = max{60, x1 + 21, x2 + 19}
        cons#_A(x1,x2) = 20
        s_A(x1) = max{23, x1 - 131}
        min_A(x1,x2) = max{78, x1 - 26, x2 - 133}
        |0|_A = 0
        transform_A(x1) = max{80, x1 + 22}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          transform#_A(x1) = max{0, x1 - 14}
          cons_A(x1,x2) = max{13, x1 + 6, x2 + 6}
          cons#_A(x1,x2) = max{0, x1 - 14, x2 - 14}
          s_A(x1) = max{11, x1}
          min_A(x1,x2) = max{39, x2 - 20}
          |0|_A = 18
          transform_A(x1) = max{18, x1 + 6}
          transform#!_A(x1) = max{1, x1 - 14}
          cons!_A(x1,x2) = max{41, x1 - 53}
          cons#!_A(x1,x2) = max{1, x1 - 14, x2 - 15}
          s!_A(x1) = max{37, x1 - 48}
          min!_A(x1,x2) = max{40, x1 - 49, x2 - 19}
          |0|!_A = 0
          transform!_A(x1) = max{40, x1 - 48}
  
    partial status:
  
      pi(transform#) = []
      pi(cons) = [1, 2]
      pi(cons#) = []
      pi(s) = []
      pi(min) = []
      pi(|0|) = []
      pi(transform) = []

The following rules are removed:

  p5



-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: transform#(cons(x,y)) -> cons#(cons(x,x),x)
p2: cons#(cons(x,z),s(y)) -> transform#(x)
p3: transform#(s(x)) -> transform#(x)
p4: transform#(cons(x,y)) -> cons#(x,x)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: transform#(cons(x,y)) -> cons#(cons(x,x),x)
p2: cons#(cons(x,z),s(y)) -> transform#(x)
p3: transform#(cons(x,y)) -> cons#(x,x)
p4: transform#(s(x)) -> transform#(x)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The set of usable rules consists of

  r10, r11, r12, r13, r14, r15, r16

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        transform#_A(x1) = 1
        cons_A(x1,x2) = max{8, x1 + 7, x2 + 2}
        cons#_A(x1,x2) = 1
        s_A(x1) = max{11, x1 - 23}
        transform_A(x1) = x1 + 12
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          transform#_A(x1) = max{0, x1 - 14}
          cons_A(x1,x2) = max{13, x1 + 6, x2 + 6}
          cons#_A(x1,x2) = max{0, x1 - 14, x2 - 11}
          s_A(x1) = max{10, x1}
          transform_A(x1) = max{18, x1 + 6}
          transform#!_A(x1) = max{0, x1 - 11}
          cons!_A(x1,x2) = max{0, x1 - 14, x2 - 15}
          cons#!_A(x1,x2) = max{1, x1 - 14, x2 - 11}
          s!_A(x1) = max{0, x1 - 38}
          transform!_A(x1) = 0
  
    partial status:
  
      pi(transform#) = []
      pi(cons) = [2]
      pi(cons#) = []
      pi(s) = []
      pi(transform) = []

The following rules are removed:

  p1, p2, p3



-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: transform#(s(x)) -> transform#(x)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: transform#(s(x)) -> transform#(x)

and R consists of:

r1: min(x,|0|()) -> |0|()
r2: min(|0|(),y) -> |0|()
r3: min(s(x),s(y)) -> s(min(x,y))
r4: max(x,|0|()) -> x
r5: max(|0|(),y) -> y
r6: max(s(x),s(y)) -> s(max(x,y))
r7: minus(x,|0|()) -> x
r8: minus(s(x),s(y)) -> s(minus(x,y))
r9: gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
r10: transform(x) -> s(s(x))
r11: transform(cons(x,y)) -> cons(cons(x,x),x)
r12: transform(cons(x,y)) -> y
r13: transform(s(x)) -> s(s(transform(x)))
r14: cons(x,y) -> y
r15: cons(x,cons(y,s(z))) -> cons(y,x)
r16: cons(cons(x,z),s(y)) -> transform(x)

The set of usable rules consists of

  r1, r2

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        transform#_A(x1) = max{4, x1 + 2}
        s_A(x1) = max{8, x1 + 3}
        min_A(x1,x2) = max{4, x1 - 23, x2 - 22}
        |0|_A = 0
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          transform#_A(x1) = 0
          s_A(x1) = max{1, x1 - 22}
          min_A(x1,x2) = max{21, x1 - 3, x2 - 3}
          |0|_A = 0
          transform#!_A(x1) = max{4, x1 - 36}
          s!_A(x1) = max{3, x1 - 35}
          min!_A(x1,x2) = max{4, x1 - 69, x2 - 17}
          |0|!_A = 0
  
    partial status:
  
      pi(transform#) = [1]
      pi(s) = [1]
      pi(min) = []
      pi(|0|) = []

The following rules are removed:

  p1

Then no dependency pair remains.