### Definitional Expansions

#### Definitional Expansions - Predicates

non permissive definitions

Simple:
```definition
let X, Y be set;
pred X c= Y means phi_1[X,Y];
end;

X c= Y
proof
thus phi_1[X,Y];
end;
```

Complex:
```definition
let X, Y be set;
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;
connectedness;
end;

X c= Y
proof
per cases;
case C1[X,Y];
thus phi_1[X,Y];
case C2[X,Y];
thus phi_2[X,Y];
case C3[X,Y];
thus phi_3[X,Y];
case not C1[X,Y] & not C2[X,Y] & not C3[X,Y];
thus phi_4[X,Y];
end;
```
permissive definitions

Simple:
```definition
let X, Y be set;
assume alpha[X,Y];
pred X c= Y means phi_1[X,Y];
end;

X c= Y
proof
thus alpha[X,Y];
thus phi_1[X,Y];
end;
```

Complex:
```definition
let X, Y be set;
assume alpha[X,Y];
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;
end;

X c= Y
proof
thus alpha[X,Y];
per cases;
case C1[X,Y];
thus phi_1[X,Y];
case C2[X,Y];
thus phi_2[X,Y];
case C3[X,Y];
thus phi_3[X,Y];
case not C1[X,Y] & not C2[X,Y] & not C3[X,Y];
thus phi_4[X,Y];
end;
```

#### Definitional Expansions - Modes

non permissive definitions

Simple:
```definition
let X be set;
mode Subset of X -> set means phi_1[it,X];
existence;
end;

Y is Subset of X
proof
thus phi_1[Y,X];
end;
```

Complex:
```definition
let X be set;
mode Subset of X -> set 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];
existence;
consistency;
end;

Y is Subset of X
proof
per cases;
case G1[X];
thus phi_1[Y,X];
case G2[X];
thus phi_2[Y,X];
case G3[X];
thus phi_3[Y,X];
case not G1[X] & not G2[X] & not G3[X];
thus phi_4[Y,X];
end;
```
permissive definitions

Simple:
```definition
let X be set;
assume beta[X];
mode Subset of X -> set means phi_1[it,X];
existence;
end;

Y is Subset of X
proof
thus beta[X];
thus phi_1[Y,X];
end;
```

Complex:
```definition
let X be set;
assume beta[X];
mode Subset of X -> set 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];
existence;
consistency;
end;

Y is Subset of X
proof
thus beta[X];
per cases;
case G1[X];
thus phi_1[Y,X];
case G2[X];
thus phi_2[Y,X];
case G3[X];
thus phi_3[Y,X];
case not G1[X] & not G2[X] & not G3[X];
thus phi_4[Y,X];
end;
```

#### Definitional Expansions - Attributes

non permissive definitions

Simple:
```definition
let X be set;
attr X is empty means phi_1[X];
end;

X is empty
proof
thus phi_1[X];
end;
```

Complex:
```definition
let X be set;
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];
consistency;
end;

X is empty
proof
per cases;
case C1[X];
thus phi_1[X];
case C2[X];
thus phi_2[X];
case C3[X];
thus phi_3[X];
case not C1[X] & not C2[X] & not C3[X];
thus phi_4[X];
end;
```
permissive definitions

Simple:
```definition
let X be set;
assume beta[X];
attr X is empty means phi_1[X];
end;

X is empty
proof
thus beta[X];
thus phi_1[X];
end;
```

Complex:
```definition
let X be set;
assume beta[X];
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];
consistency;
end;

X is empty
proof
thus beta[X];
per cases;
case C1[X];
thus phi_1[X];
case C2[X];
thus phi_2[X];
case C3[X];
thus phi_3[X];
case not C1[X] & not C2[X] & not C3[X];
thus phi_4[X];
end;
```