MAYBE

Problem:
 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)

Proof:
 DP Processor:
  DPs:
   min#(s(x),s(y)) -> min#(x,y)
   max#(s(x),s(y)) -> max#(x,y)
   minus#(s(x),s(y)) -> minus#(x,y)
   gcd#(s(x),s(y)) -> min#(x,y)
   gcd#(s(x),s(y)) -> transform#(y)
   gcd#(s(x),s(y)) -> min#(x,transform(y))
   gcd#(s(x),s(y)) -> max#(x,y)
   gcd#(s(x),s(y)) -> minus#(max(x,y),min(x,transform(y)))
   gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
   transform#(cons(x,y)) -> cons#(x,x)
   transform#(cons(x,y)) -> cons#(cons(x,x),x)
   transform#(s(x)) -> transform#(x)
   cons#(x,cons(y,s(z))) -> cons#(y,x)
   cons#(cons(x,z),s(y)) -> transform#(x)
  TRS:
   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)
  Usable Rule Processor:
   DPs:
    min#(s(x),s(y)) -> min#(x,y)
    max#(s(x),s(y)) -> max#(x,y)
    minus#(s(x),s(y)) -> minus#(x,y)
    gcd#(s(x),s(y)) -> min#(x,y)
    gcd#(s(x),s(y)) -> transform#(y)
    gcd#(s(x),s(y)) -> min#(x,transform(y))
    gcd#(s(x),s(y)) -> max#(x,y)
    gcd#(s(x),s(y)) -> minus#(max(x,y),min(x,transform(y)))
    gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
    transform#(cons(x,y)) -> cons#(x,x)
    transform#(cons(x,y)) -> cons#(cons(x,x),x)
    transform#(s(x)) -> transform#(x)
    cons#(x,cons(y,s(z))) -> cons#(y,x)
    cons#(cons(x,z),s(y)) -> transform#(x)
   TRS:
    f14(x,y) -> x
    f14(x,y) -> 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)
    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))
   EDG Processor:
    DPs:
     min#(s(x),s(y)) -> min#(x,y)
     max#(s(x),s(y)) -> max#(x,y)
     minus#(s(x),s(y)) -> minus#(x,y)
     gcd#(s(x),s(y)) -> min#(x,y)
     gcd#(s(x),s(y)) -> transform#(y)
     gcd#(s(x),s(y)) -> min#(x,transform(y))
     gcd#(s(x),s(y)) -> max#(x,y)
     gcd#(s(x),s(y)) -> minus#(max(x,y),min(x,transform(y)))
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
     transform#(cons(x,y)) -> cons#(x,x)
     transform#(cons(x,y)) -> cons#(cons(x,x),x)
     transform#(s(x)) -> transform#(x)
     cons#(x,cons(y,s(z))) -> cons#(y,x)
     cons#(cons(x,z),s(y)) -> transform#(x)
    TRS:
     f14(x,y) -> x
     f14(x,y) -> 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)
     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))
    graph:
     cons#(cons(x,z),s(y)) -> transform#(x) ->
     transform#(cons(x,y)) -> cons#(x,x)
     cons#(cons(x,z),s(y)) -> transform#(x) ->
     transform#(cons(x,y)) -> cons#(cons(x,x),x)
     cons#(cons(x,z),s(y)) -> transform#(x) ->
     transform#(s(x)) -> transform#(x)
     cons#(x,cons(y,s(z))) -> cons#(y,x) ->
     cons#(x,cons(y,s(z))) -> cons#(y,x)
     cons#(x,cons(y,s(z))) -> cons#(y,x) ->
     cons#(cons(x,z),s(y)) -> transform#(x)
     transform#(cons(x,y)) -> cons#(cons(x,x),x) ->
     cons#(x,cons(y,s(z))) -> cons#(y,x)
     transform#(cons(x,y)) -> cons#(cons(x,x),x) ->
     cons#(cons(x,z),s(y)) -> transform#(x)
     transform#(cons(x,y)) -> cons#(x,x) ->
     cons#(x,cons(y,s(z))) -> cons#(y,x)
     transform#(cons(x,y)) -> cons#(x,x) ->
     cons#(cons(x,z),s(y)) -> transform#(x)
     transform#(s(x)) -> transform#(x) ->
     transform#(cons(x,y)) -> cons#(x,x)
     transform#(s(x)) -> transform#(x) ->
     transform#(cons(x,y)) -> cons#(cons(x,x),x)
     transform#(s(x)) -> transform#(x) ->
     transform#(s(x)) -> transform#(x)
     gcd#(s(x),s(y)) -> transform#(y) ->
     transform#(cons(x,y)) -> cons#(x,x)
     gcd#(s(x),s(y)) -> transform#(y) ->
     transform#(cons(x,y)) -> cons#(cons(x,x),x)
     gcd#(s(x),s(y)) -> transform#(y) ->
     transform#(s(x)) -> transform#(x)
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ->
     gcd#(s(x),s(y)) -> min#(x,y)
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ->
     gcd#(s(x),s(y)) -> transform#(y)
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ->
     gcd#(s(x),s(y)) -> min#(x,transform(y))
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ->
     gcd#(s(x),s(y)) -> max#(x,y)
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ->
     gcd#(s(x),s(y)) -> minus#(max(x,y),min(x,transform(y)))
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ->
     gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
     gcd#(s(x),s(y)) -> minus#(max(x,y),min(x,transform(y))) ->
     minus#(s(x),s(y)) -> minus#(x,y)
     gcd#(s(x),s(y)) -> max#(x,y) ->
     max#(s(x),s(y)) -> max#(x,y)
     gcd#(s(x),s(y)) -> min#(x,transform(y)) ->
     min#(s(x),s(y)) -> min#(x,y)
     gcd#(s(x),s(y)) -> min#(x,y) -> min#(s(x),s(y)) -> min#(x,y)
     minus#(s(x),s(y)) -> minus#(x,y) ->
     minus#(s(x),s(y)) -> minus#(x,y)
     max#(s(x),s(y)) -> max#(x,y) -> max#(s(x),s(y)) -> max#(x,y)
     min#(s(x),s(y)) -> min#(x,y) -> min#(s(x),s(y)) -> min#(x,y)
    Restore Modifier:
     DPs:
      min#(s(x),s(y)) -> min#(x,y)
      max#(s(x),s(y)) -> max#(x,y)
      minus#(s(x),s(y)) -> minus#(x,y)
      gcd#(s(x),s(y)) -> min#(x,y)
      gcd#(s(x),s(y)) -> transform#(y)
      gcd#(s(x),s(y)) -> min#(x,transform(y))
      gcd#(s(x),s(y)) -> max#(x,y)
      gcd#(s(x),s(y)) -> minus#(max(x,y),min(x,transform(y)))
      gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
      transform#(cons(x,y)) -> cons#(x,x)
      transform#(cons(x,y)) -> cons#(cons(x,x),x)
      transform#(s(x)) -> transform#(x)
      cons#(x,cons(y,s(z))) -> cons#(y,x)
      cons#(cons(x,z),s(y)) -> transform#(x)
     TRS:
      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 Processor:
      #sccs: 5
      #rules: 9
      #arcs: 28/196
      DPs:
       gcd#(s(x),s(y)) -> gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y)))
      TRS:
       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)
      Open
      
      DPs:
       min#(s(x),s(y)) -> min#(x,y)
      TRS:
       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)
      Open
      
      DPs:
       max#(s(x),s(y)) -> max#(x,y)
      TRS:
       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)
      Open
      
      DPs:
       minus#(s(x),s(y)) -> minus#(x,y)
      TRS:
       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)
      Open
      
      DPs:
       cons#(cons(x,z),s(y)) -> transform#(x)
       transform#(s(x)) -> transform#(x)
       transform#(cons(x,y)) -> cons#(cons(x,x),x)
       cons#(x,cons(y,s(z))) -> cons#(y,x)
       transform#(cons(x,y)) -> cons#(x,x)
      TRS:
       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)
      Open