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, r9, r12

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        gcd#_A(x1,x2) = max{21, x1 + 10, x2 - 35}
        s_A(x1) = x1 + 87
        minus_A(x1,x2) = max{x1 + 10, x2 - 88}
        max_A(x1,x2) = max{x1 + 68, x2 + 31}
        min_A(x1,x2) = x1 + 6
        transform_A(x1) = max{169, x1 + 3}
        |0|_A = 5
        gcd_A(x1,x2) = max{169, x1 - 78, x2 - 84}
        cons_A(x1,x2) = max{x1 + 170, x2 - 2}
  
    base order 2:
  
      precedence:
      
        max > gcd# > minus > gcd > min > s = transform = |0| = cons
      
  
    partial status:
  
      pi(gcd#) = [1]
      pi(s) = [1]
      pi(minus) = [1]
      pi(max) = [2]
      pi(min) = [1]
      pi(transform) = [1]
      pi(|0|) = []
      pi(gcd) = []
      pi(cons) = [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: 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, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        min#_A(x1,x2) = max{1, x1 - 1, x2 - 1}
        s_A(x1) = x1 + 6
        min_A(x1,x2) = max{7, x1 - 21, x2 - 7}
        |0|_A = 0
  
    base order 2:
  
      precedence:
      
        min# = min > s = |0|
      
  
    partial status:
  
      pi(min#) = []
      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: 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, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        max#_A(x1,x2) = max{x1 - 1, x2 + 5}
        s_A(x1) = x1 + 6
        min_A(x1,x2) = max{7, x1 - 21, x2 - 7}
        |0|_A = 0
  
    base order 2:
  
      precedence:
      
        max# = min > s = |0|
      
  
    partial status:
  
      pi(max#) = [2]
      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, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        minus#_A(x1,x2) = max{x1 - 1, x2 + 5}
        s_A(x1) = x1 + 6
        min_A(x1,x2) = max{7, x1 - 21, x2 - 7}
        |0|_A = 0
  
    base order 2:
  
      precedence:
      
        minus# = min > s = |0|
      
  
    partial status:
  
      pi(minus#) = [2]
      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: 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, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        transform#_A(x1) = max{22, x1 + 18}
        cons_A(x1,x2) = max{x1 + 23, x2 + 13}
        cons#_A(x1,x2) = max{x1 + 8, x2 - 7}
        s_A(x1) = max{4, x1}
        min_A(x1,x2) = max{1, x1 - 12, x2 - 38}
        |0|_A = 0
        transform_A(x1) = max{37, x1 + 24}
  
    base order 2:
  
      precedence:
      
        transform# = cons# > cons > transform > min > s = |0|
      
  
    partial status:
  
      pi(transform#) = [1]
      pi(cons) = [1, 2]
      pi(cons#) = [1]
      pi(s) = [1]
      pi(min) = []
      pi(|0|) = []
      pi(transform) = [1]

The following rules are removed:

  p1



-- SCC decomposition.

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

p1: cons#(cons(x,z),s(y)) -> transform#(x)
p2: transform#(s(x)) -> transform#(x)
p3: transform#(cons(x,y)) -> cons#(x,x)
p4: 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 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: cons#(cons(x,z),s(y)) -> transform#(x)
p2: transform#(cons(x,y)) -> cons#(x,x)
p3: cons#(x,cons(y,s(z))) -> cons#(y,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

  r1, r2

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        cons#_A(x1,x2) = max{x1 + 16, x2 + 9}
        cons_A(x1,x2) = max{x1 + 17, x2 - 11}
        s_A(x1) = x1 + 13
        transform#_A(x1) = x1 + 12
        min_A(x1,x2) = max{14, x1 - 4}
        |0|_A = 1
  
    base order 2:
  
      precedence:
      
        cons > s = min > cons# = |0| > transform#
      
  
    partial status:
  
      pi(cons#) = [1]
      pi(cons) = [1]
      pi(s) = [1]
      pi(transform#) = [1]
      pi(min) = []
      pi(|0|) = []

The following rules are removed:

  p4



-- SCC decomposition.

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

p1: cons#(cons(x,z),s(y)) -> transform#(x)
p2: transform#(cons(x,y)) -> cons#(x,x)
p3: 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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: cons#(cons(x,z),s(y)) -> transform#(x)
p2: transform#(cons(x,y)) -> cons#(x,x)
p3: 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

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        cons#_A(x1,x2) = max{1, x1 - 5, x2 - 6}
        cons_A(x1,x2) = max{19, x1 + 4, x2 - 20}
        s_A(x1) = max{59, x1 + 28}
        transform#_A(x1) = max{3, x1 - 2}
        min_A(x1,x2) = max{0, x1 - 61, x2 - 119}
        |0|_A = 0
  
    base order 2:
  
      precedence:
      
        cons > min > s = |0| > cons# > transform#
      
  
    partial status:
  
      pi(cons#) = []
      pi(cons) = [1]
      pi(s) = []
      pi(transform#) = []
      pi(min) = []
      pi(|0|) = []

The following rules are removed:

  p3



-- SCC decomposition.

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

p1: cons#(cons(x,z),s(y)) -> transform#(x)
p2: 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}


-- Reduction pair.

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

p1: cons#(cons(x,z),s(y)) -> transform#(x)
p2: 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 set of usable rules consists of

  r1, r2, r10

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        cons#_A(x1,x2) = max{x1 + 30, x2 + 36}
        cons_A(x1,x2) = max{13, x1 + 4, x2 - 14}
        s_A(x1) = max{2, x1 - 21}
        transform#_A(x1) = x1 + 33
        min_A(x1,x2) = max{27, x1 - 10, x2 - 25}
        |0|_A = 0
        transform_A(x1) = max{17, x1 - 3}
  
    base order 2:
  
      precedence:
      
        cons > transform > cons# > transform# = min > s = |0|
      
  
    partial status:
  
      pi(cons#) = [1]
      pi(cons) = [1]
      pi(s) = []
      pi(transform#) = [1]
      pi(min) = []
      pi(|0|) = []
      pi(transform) = []

The following rules are removed:

  p2



-- SCC decomposition.

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

p1: 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:

  (no SCCs)