Alphabet

0:real
1:real
-:[real] ⟶ real
sin:[real] ⟶ real
cos:[real] ⟶ real
ln:[real] ⟶ real
+:[real × real] ⟶ real
*:[real × real] ⟶ real
/:[real × real] ⟶ real
der:[real → real] ⟶ real → real

Variables

y:real
F:real → real
G:real → real

Rules

der(λx:real.y)⇒λx:real.0
der(λx:real.x)⇒λx:real.1
der(λx:real.sin(x))⇒λx:real.cos(x)
der(λx:real.cos(x))⇒λx:real.-(sin(x))
der(λx:real.+(F · x, G · x))⇒λx:real.+(der(F) · x, der(G) · x)
der(λx:real.*(F · x, G · x))⇒λx:real.+(*(der(F) · x, G · x), *(F · x, der(G) · x))
der(λx:real.ln(F · x))⇒λx:real./(der(F) · x, F · x)