| + | : | [proc × proc] ⟶ proc |
| * | : | [proc × proc] ⟶ proc |
| delta | : | proc |
| sigma | : | [data → proc] ⟶ proc |
| X | : | proc |
| Y | : | proc |
| Z | : | proc |
| D | : | data |
| P | : | data → proc |
| Q | : | data → proc |
| +(X, X) | ⇒ | X |
| *(+(X, Y), Z) | ⇒ | +(*(X, Z), *(Y, Z)) |
| *(*(X, Y), Z) | ⇒ | *(X, *(Y, Z)) |
| +(X, delta) | ⇒ | X |
| *(delta, X) | ⇒ | delta |
| sigma(λd:data.X) | ⇒ | X |
| +(sigma(λd:data.P · d), P · D) | ⇒ | sigma(λd:data.P · d) |
| sigma(λd:data.+(P · d, Q · d)) | ⇒ | +(sigma(λd:data.P · d), sigma(λd:data.Q · d)) |
| *(sigma(λd:data.P · d), X) | ⇒ | sigma(λd:data.*(P · d, X)) |