| |
| x(∧/≥)y x∧.≥y | |
2-∞ |
| x(1∊≥)y | |
2-∞ |
| x(+/≥)y | |
1.4 |
|
Similarly,
| x (f g) y ←→ f (x g y) |
| ∴ x (∧/≥) y ←→ ∧/(x≥y) ←→ ∧/x≥y (←→ x∧.≥y) |
| |
| x (a f g) y ←→ a f (x g y) |
| ∴ x (1∊≥) y ←→ 1∊(x≥y) ←→ 1∊x≥y |
| |
| In general, the patterns are x (f/ comp) y
and x (b ∊ comp) y
|
| • f is + ∨ ∧ |
| • comp is < ≤ = ≠ ≥ > |
| • b is 0 or 1 |
|