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:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            gcd#_A(x1,x2) = max{0, x1 - 27, x2 - 42}
            s_A(x1) = max{25, x1 + 16}
            minus_A(x1,x2) = max{1, x1}
            max_A(x1,x2) = max{x1 + 1, x2 + 1}
            min_A(x1,x2) = max{x1 + 10, x2 - 9}
            transform_A(x1) = x1 + 18
            |0|_A = 10
            gcd#!_A(x1,x2) = max{2, x1 - 2, x2 - 13}
            s!_A(x1) = 1
            minus!_A(x1,x2) = 24
            max!_A(x1,x2) = max{24, x1 - 34, x2 - 26}
            min!_A(x1,x2) = max{0, x1 - 26, x2 - 26}
            transform!_A(x1) = 0
            |0|!_A = 0
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            gcd#_A(x1,x2) = 0
            s_A(x1) = 6
            minus_A(x1,x2) = max{7, x1}
            max_A(x1,x2) = max{x1, x2}
            min_A(x1,x2) = x1
            transform_A(x1) = 3
            |0|_A = 0
            gcd#!_A(x1,x2) = max{2, x2 - 8}
            s!_A(x1) = 4
            minus!_A(x1,x2) = max{6, x1 - 7}
            max!_A(x1,x2) = 6
            min!_A(x1,x2) = 1
            transform!_A(x1) = max{3, x1 - 8}
            |0|!_A = 1
        
  
    partial status:
  
      pi(gcd#) = []
      pi(s) = []
      pi(minus) = [1]
      pi(max) = [1, 2]
      pi(min) = [2]
      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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            min#_A(x1,x2) = 0
            s_A(x1) = max{1, x1 - 36}
            min#!_A(x1,x2) = 0
            s!_A(x1) = max{2, x1 - 68}
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            min#_A(x1,x2) = 0
            s_A(x1) = max{17, x1 - 13}
            min#!_A(x1,x2) = max{31, x1 + 14}
            s!_A(x1) = max{37, x1 + 32}
        
  
    partial status:
  
      pi(min#) = [1]
      pi(s) = [1]

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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            max#_A(x1,x2) = 0
            s_A(x1) = x1 + 8
            max#!_A(x1,x2) = max{1, x2 - 2}
            s!_A(x1) = max{89, x1 + 51}
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            max#_A(x1,x2) = 0
            s_A(x1) = max{21, x1 - 53}
            max#!_A(x1,x2) = max{75, x2 + 54}
            s!_A(x1) = max{76, x1 + 58}
        
  
    partial status:
  
      pi(max#) = []
      pi(s) = []

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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            minus#_A(x1,x2) = 0
            s_A(x1) = max{30, x1 + 8}
            minus#!_A(x1,x2) = max{0, x2 - 7}
            s!_A(x1) = max{1, x1 - 6}
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            minus#_A(x1,x2) = 0
            s_A(x1) = max{14, x1 - 11}
            minus#!_A(x1,x2) = 0
            s!_A(x1) = max{5, x1 + 2}
        
  
    partial status:
  
      pi(minus#) = []
      pi(s) = []

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:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            transform#_A(x1) = max{0, x1 - 22}
            cons_A(x1,x2) = max{21, x1 + 10, x2 + 5}
            cons#_A(x1,x2) = max{0, x1 - 22, x2 - 25}
            s_A(x1) = max{24, x1}
            min_A(x1,x2) = max{49, x1 - 28, x2 - 28}
            |0|_A = 27
            transform_A(x1) = max{30, x1 + 10}
            transform#!_A(x1) = 0
            cons!_A(x1,x2) = max{31, x1 + 28, x2 + 27}
            cons#!_A(x1,x2) = 0
            s!_A(x1) = 30
            min!_A(x1,x2) = max{31, x1 - 39, x2 - 107}
            |0|!_A = 0
            transform!_A(x1) = max{50, x1 + 29}
        
        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 + 8, x2 + 8}
            cons#_A(x1,x2) = max{0, x1 - 14, x2 - 16}
            s_A(x1) = max{15, x1}
            min_A(x1,x2) = max{77, x1 - 29, x2 - 45}
            |0|_A = 15
            transform_A(x1) = x1 + 16
            transform#!_A(x1) = max{1, x1 - 10}
            cons!_A(x1,x2) = max{26, x2 + 3}
            cons#!_A(x1,x2) = max{2, x1 - 14, x2 - 16}
            s!_A(x1) = x1 + 13
            min!_A(x1,x2) = max{27, x1 - 16, x2 - 78}
            |0|!_A = 27
            transform!_A(x1) = max{27, x1 - 14}
        
  
    partial status:
  
      pi(transform#) = []
      pi(cons) = [1, 2]
      pi(cons#) = []
      pi(s) = []
      pi(min) = [1, 2]
      pi(|0|) = []
      pi(transform) = [1]

The following rules are removed:

  p1, p2, p4, p5



-- 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:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            transform#_A(x1) = 0
            s_A(x1) = max{3, x1 - 43}
            min_A(x1,x2) = max{37, x1 - 4, x2 - 8}
            |0|_A = 0
            transform#!_A(x1) = 1
            s!_A(x1) = max{3, x1 - 67}
            min!_A(x1,x2) = max{1, x1 - 101, x2 - 67}
            |0|!_A = 0
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            transform#_A(x1) = x1
            s_A(x1) = max{38, x1 + 20}
            min_A(x1,x2) = max{148, x1 - 39, x2 - 39}
            |0|_A = 0
            transform#!_A(x1) = max{1, x1 - 18}
            s!_A(x1) = max{0, x1 - 218}
            min!_A(x1,x2) = max{1, x1 - 118, x2 - 107}
            |0|!_A = 2
        
  
    partial status:
  
      pi(transform#) = []
      pi(s) = []
      pi(min) = []
      pi(|0|) = []

The following rules are removed:

  p1

Then no dependency pair remains.