commutation

The commutation command swaps the operands of commutative operators. There are two categories of commutations: elementary ones that are built-in to cadiz, and ones that are coded explicitly as Z rewrite rules. An example of the latter is as follows.

union_commutation ==

[X] $\vdash$ ? $\forall$ S, T : $\power$ X

S $\cup$ T = T $\cup$ S

The form of a rewrite rule must be as specified in rewrite by rule, and moreover its name must have commutation as a sub-string. The effect of a rewrite rule is also explained in rewrite by rule.

The built-in elementary commutations are as follows. They take precedence over any matching explicit rewrite rule.

`e₁ = e₂`		`e₂ = e₁`
`p₁ p₂`		`p₂ p₁`
`e₁ e₂`		`e₂ e₁`
`p₁ p₂`		`p₂ p₁`
`e₁ e₂`		`e₂ e₁`
`p₁ p₂`		`p₂ p₁`
`e₁ e₂`		`e₂ e₁`
`p₁ p₂`		`p₂ p₁`
`e₁ e₂`		`e₂ e₁`

Tactic example

"commutation" p₃ p₄

This example applies the commutation command to predicates p₃ and p₄.

IT 6-Jul-2000