### Redefinitions

#### Predicates

```definition
let X, Y be set;
redefine pred X c= Y means phi_1[X,Y];
compatibility
proof
thus X c= Y iff phi_1[X,Y];
end;
end;
```
```definition
let X, Y be set;
redefine pred X c= Y means
phi_1[X,Y] if C1[X,Y],
phi_2[X,Y] if C2[X,Y],
phi_3[X,Y] if C3[X,Y]
otherwise phi_4[X,Y];
consistency;
compatibility
proof
thus C1[X,Y] implies (X c= Y iff phi_1[X,Y]);
thus C2[X,Y] implies (X c= Y iff phi_2[X,Y]);
thus C3[X,Y] implies (X c= Y iff phi_3[X,Y]);
thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies
(X c= Y iff phi_4[X,Y]);
end;
end;
```

#### Modes

Modes - result type is being changed
```definition
let X be set;
redefine mode Subset of X -> new_type;
coherence
proof
thus for A being Subset of X holds A is new_type;
end;
end;
```
Modes - definiens is being changed
```definition
let X be set;
redefine mode Subset of X means phi_1[it,X];
compatibility
proof
let A be set;
thus A is Subset of X iff phi_1[A,X];
end;
end;
```
```definition
let X be set;
redefine mode Subset of X means
phi_1[it,X] if G1[X],
phi_2[it,X] if G2[X],
phi_3[it,X] if G3[X]
otherwise phi_4[it,X];
compatibility
proof
let A be set;
thus G1[X] implies (A is Subset of X iff phi_1[A,X]);
thus G2[X] implies (A is Subset of X iff phi_2[A,X]);
thus G3[X] implies (A is Subset of X iff phi_3[A,X]);
thus not G1[X] & not G2[X] & not G3[X] implies
(A is Subset of X iff phi_4[A,X]);
end;
consistency;
end;
```

#### Functors

Functors - result type is being changed
```definition
let X be set;
redefine func +X -> new_type;
coherence
proof
thus +X is new_type;
end;
end;
```

#### Functors - means

Functors - means - definiens is being changed
```definition
let X be set;
redefine func +X means phi_1[it,X];
compatibility
proof
let A be set;
thus A = +X iff phi_1[A,X];
end;
end;
```
```definition
let X be set;
redefine func +X means
phi_1[it,X] if G1[X],
phi_2[it,X] if G2[X],
phi_3[it,X] if G3[X]
otherwise phi_4[it,X];
consistency;
compatibility
proof
let A be set;
thus G1[X] implies (A = +X iff phi_1[A,X]);
thus G2[X] implies (A = +X iff phi_2[A,X]);
thus G3[X] implies (A = +X iff phi_3[A,X]);
thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff phi_4[A,X]);
end;
end;
```

#### Functors - equals

Functors - equals - definiens is being changed
```definition
let X be set;
redefine func +X equals tau_1(X);
compatibility
proof
let A be set;
thus A = +X iff A = tau_1(X);
end;
end;
```
```definition
let X be set;
redefine func +X equals
tau_1(X) if G1[X],
tau_2(X) if G2[X],
tau_3(X) if G3[X]
otherwise tau_4(X);
consistency;
compatibility
proof
let A be set;
thus G1[X] implies (A = +X iff A = tau_1(A));
thus G2[X] implies (A = +X iff A = tau_2(A));
thus G3[X] implies (A = +X iff A = tau_3(A));
thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff A = tau_4(A));
end;
end;
```

#### Attributes

```definition
let X be set;
redefine attr X is empty means phi_1[X];
compatibility
proof
thus X is empty iff phi_1[X];
end;
end;
```
```definition
let X be set;
redefine attr X is empty means
phi_1[X] if C1[X],
phi_2[X] if C2[X],
phi_3[X] if C3[X]
otherwise phi_4[X];
compatibility
proof
thus C1[X] implies (X is empty iff phi_1[X]);
thus C2[X] implies (X is empty iff phi_2[X]);
thus C3[X] implies (X is empty iff phi_3[X]);
thus not C1[X] & not C2[X] & not C3[X] implies (X is empty iff phi_4[X]);
end;
consistency;
end;
```