Problem:
 max(x,0()) -> x
 max(s(x),s(y)) -> s(max(x,y))
 max(x,y) -> max(y,x)

Proof:
 Commute Transformation Processor:
  max(x,0()) -> x
  max(0(),x) -> x
  max(s(x),s(y)) -> s(max(x,y))
  max(s(y),s(x)) -> s(max(x,y))
  max(x,y) -> max(y,x)
  Church Rosser Transformation Processor:
   
   strict:
    
   weak:
    
   critical peaks: 12
   0() <-0|[]- max(0(),0()) -1|[]-> 0()
   x <-0|[]- max(x,0()) -4|[]-> max(0(),x)
   0() <-1|[]- max(0(),0()) -0|[]-> 0()
   y <-1|[]- max(0(),y) -4|[]-> max(y,0())
   s(max(y,x)) <-2|[]- max(s(y),s(x)) -3|[]-> s(max(x,y))
   s(max(x96,x97)) <-2|[]- max(s(x96),s(x97)) -4|[]-> max(s(x97),s(x96))
   s(max(y,x)) <-3|[]- max(s(x),s(y)) -2|[]-> s(max(x,y))
   s(max(x101,x100)) <-3|[]- max(s(x100),s(x101)) -4|[]-> max(s(x101),s(x100))
   max(0(),x) <-4|[]- max(x,0()) -0|[]-> x
   max(x,0()) <-4|[]- max(0(),x) -1|[]-> x
   max(s(y),s(x)) <-4|[]- max(s(x),s(y)) -2|[]-> s(max(x,y))
   max(s(x),s(y)) <-4|[]- max(s(y),s(x)) -3|[]-> s(max(x,y))
   Closedness Processor (*parallel*):
    
    strict:
     
    weak:
     
    Qed