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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 8
  0() <-0|[]- max(0(),0()) -1|[]-> 0()
  x <-0|[]- max(x,0()) -3|[]-> max(0(),x)
  0() <-1|[]- max(0(),0()) -0|[]-> 0()
  y <-1|[]- max(0(),y) -3|[]-> max(y,0())
  s(max(x54,x55)) <-2|[]- max(s(x54),s(x55)) -3|[]-> max(s(x55),s(x54))
  max(0(),x) <-3|[]- max(x,0()) -0|[]-> x
  max(y,0()) <-3|[]- max(0(),y) -1|[]-> y
  max(s(y),s(x)) <-3|[]- max(s(x),s(y)) -2|[]-> s(max(x,y))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed