| d · (λ%X:R.X) · Y | ⇒ | 0
|
| d · (λ%Y:R.%Y) · U | ⇒ | 1
|
| d · (λ%Z:R.minus · (H · %Z)) · W | ⇒ | minus · (d · (λ%U:R.H · %U) · W)
|
| d · (λ%V:R.pls · (J · %V) · (F1 · %V)) · Y1 | ⇒ | pls · (d · (λ%F:R.J · %F) · Y1) · (d · (λ%W:R.F1 · %W) · Y1)
|
| d · (λ%G:R.mul · (G1 · %G) · (H1 · %G)) · W1 | ⇒ | pls · (mul · (d · (λ%I:R.G1 · %I) · W1) · (H1 · W1)) · (mul · (G1 · W1) · (d · (λ%H:R.H1 · %H) · W1))
|
| d · (λ%J:R.sin · (J1 · %J)) · X2 | ⇒ | mul · (cos · X2) · (d · (λ%P:R.J1 · %P) · X2)
|
| d · (λ%Q:R.cos · (Z2 · %Q)) · U2 | ⇒ | mul · (minus · (sin · U2)) · (d · (λ%R:R.Z2 · %R) · U2)
|
| minus · 0 | ⇒ | 0
|
| mul · 0 · V2 | ⇒ | 0
|
| mul · W2 · 0 | ⇒ | 0
|
| pls · 0 · P2 | ⇒ | P2
|