(VAR D P Q X Y Z d )
(RULES 
        +(X, X) -> X
        *(+(X, Y), Z) -> +(*(X, Z), *(Y, Z))
        *(*(X, Y), Z) -> *(X, *(Y, Z))
        +(X, delta) -> X
        *(delta, X) -> delta
        sigma() -> X
        +(sigma(), ) -> sigma()
        sigma() -> +(sigma(), sigma())
        *(sigma(), X) -> sigma()
        
)