Problem:
 D (\x. C) z -> 0
 D (\x. x) z -> 1
 D (\x. min (F x)) z -> min (D (\x. F x) z)
 D (\x. add (F x) (G x)) z -> add (D (\x. F x) z) (D (\x. G x) z)
 D (\x. mul (F x) (G x)) z -> add (mul (D (\x. F x) z) (G z)) (mul (F z) (D (\x. G x) z))
 D (\x. sin (F x)) z -> mul (cos z) (D (\x. F x) z)
 D (\x. cos (F x)) z -> mul (min (sin z)) (D (\x. F x) z)

Proof:
 Higher-Order Church Rosser Processor:
  D (\x. C) z -> 0
  D (\x. x) z -> 1
  D (\x. min (F x)) z -> min (D (\x. F x) z)
  D (\x. add (F x) (G x)) z -> add (D (\x. F x) z) (D (\x. G x) z)
  D (\x. mul (F x) (G x)) z -> add (mul (D (\x. F x) z) (G z)) (mul (F z) (D (\x. G x) z))
  D (\x. sin (F x)) z -> mul (cos z) (D (\x. F x) z)
  D (\x. cos (F x)) z -> mul (min (sin z)) (D (\x. F x) z)
  critical peaks: 10
   0 <-[]-> min (D (\23. 21) 22)
   0 <-[]-> add (D (\35. 32) 34) (D (\36. 33) 34)
   0 <-[]-> add (mul (D (\48. 45) 47) 46) (mul 45 (D (\49. 46) 47))
   0 <-[]-> mul (cos 59) (D (\60. 58) 59)
   0 <-[]-> mul (min (sin 70)) (D (\71. 69) 70)
   min (D (\116. 114) 115) <-[]-> 0
   add (D (\175. 172) 174) (D (\176. 173) 174) <-[]-> 0
   add (mul (D (\254. 251) 253) 252) (mul 251 (D (\255. 252) 253)) <-[]-> 0
   mul (cos 330) (D (\331. 329) 330) <-[]-> 0
   mul (min (sin 387)) (D (\388. 386) 387) <-[]-> 0
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    0 *<- 0 <- . -> min (D (\23. 21) 22) ->* min 0
    Qed