Problem:
 d (\x. C) z -> 0
 d (\x. x) z -> 1
 d (\x. - (F x)) z -> - (d (\x. F x) z)
 d (\x. + (F x) (G x)) z -> + (d (\x. F x) z) (d (\x. G x) z)
 d (\x. * (F x) (G x)) z -> + (* (d (\x. F x) z) (G z)) (* (F z) (d (\x. G x) z))
 d (\x. sin (F x)) z -> * (cos z) (d (\x. F x) z)
 d (\x. cos (F x)) z -> * (- (sin z)) (d (\x. F x) z)
 - 0 -> 0
 * 0 x -> 0
 * x 0 -> 0
 + 0 x -> x

Proof:
 Higher-Order Church Rosser Processor (kb):
  d (\x. C) z -> 0
  d (\x. x) z -> 1
  d (\x. - (F x)) z -> - (d (\x. F x) z)
  d (\x. + (F x) (G x)) z -> + (d (\x. F x) z) (d (\x. G x) z)
  d (\x. * (F x) (G x)) z -> + (* (d (\x. F x) z) (G z)) (* (F z) (d (\x. G x) z))
  d (\x. sin (F x)) z -> * (cos z) (d (\x. F x) z)
  d (\x. cos (F x)) z -> * (- (sin z)) (d (\x. F x) z)
  - 0 -> 0
  * 0 x -> 0
  * x 0 -> 0
  + 0 x -> x
  critical peaks: 16, all joinable
   0 <-[]-> - (d (\744. 742) 743)
   0 <-[]-> + (d (\756. 753) 755) (d (\757. 754) 755)
   0 <-[]-> + (* (d (\769. 766) 768) 767) (* 766 (d (\770. 767) 768))
   0 <-[]-> * (cos 780) (d (\781. 779) 780)
   0 <-[]-> * (- (sin 791)) (d (\792. 790) 791)
   - (d (\837. 835) 836) <-[]-> 0
   + (d (\896. 893) 895) (d (\897. 894) 895) <-[]-> 0
   + (* (d (\975. 972) 974) 973) (* 972 (d (\976. 973) 974)) <-[]-> 0
   * (cos 1051) (d (\1052. 1050) 1051) <-[]-> 0
   * (- (sin 1108)) (d (\1109. 1107) 1108) <-[]-> 0
   d (\x. 0) z <-[0,1,0]-> - (d (\x. 0) z)
   d (\x. 0) z <-[0,1,0]-> + (* (d (\x. 0) z) (1165 z)) (* 0 (d (\x. 1165 x) z))
   0 <-[]-> 0
   d (\x. 0) z <-[0,1,0]-> + (* (d (\x. 1180 x) z) 0) (* (1180 z) (d (\x. 0) z))
   0 <-[]-> 0
   d (\x. 1195 x) z <-[0,1,0]-> + (d (\x. 0) z) (d (\x. 1195 x) z)
   
   HORPO Processor:
    precedence:
     d > 1 ~ 0 ~ cos ~ sin ~ * ~ + ~ -
    problem:
     
    Qed