# Right tightening

BEWARE!This term is nonstandard and is being used locally within the wiki. [SHOW MORE]

## Definition

### Symbol-free definition

Given a restriction formal expression or extension formal expression for a property, a right tightening of the expression is another formal expression for the *same* property with the *same* left side but with the right side stronger than before.

### Definition with symbols

Given a restriction formal expression or extension formal expression for a property, say → , a **right tightening** for the property is another expression ≤ such that → = → .

## Property theory

### Maximal right tightening and right tight expressions

For any expression, there is a maximal right tightening, after which no further proper right tightening is possible. A restriction (respectively extension) formal expression for which no further tight tightening is possible is termed a right tight restriction formal expression (respectively right tight extension formal expression). The maximal right tightening operator is thus an idempotent operator on the collection of all restriction formal expressions and its image is the collection of right tight restriction formal expressions.