# Library Controlled

```
```

```
```

Require Export Theory.

```
Section RelaxedExpansion.
```

Variables A X Y: Type.

Variable TX: reduction_t A X.

Variable TY: reduction_t A Y.

Variable B: relation X.

Hypothesis HB: wexpansion1 TX TX B.

Silent case

```
Let wexpansion1_ctrl_t:
```

forall R, evolve_t TX TY R (comp (star B) R) -> simulation_t TX TY (comp (star B) R).

Lemma 3.10

```
Theorem wexpansion1_ctrl: wexpansion1 TX TX B -> controlled TX TY B.
```

End RelaxedExpansion.

```
Section PlusWf.
```

Variable A: Type.

Variable X: Set.

Variable Y: Type.

Variable TX: reduction_t A X.

Variable TY: reduction_t A Y.

Variable B: relation X.

Hypothesis HB: evolve TX TX B (plus B).

Hypothesis HB': well_founded (trans B).

Theorem 3.11

```
Theorem plus_wf_controlled: controlled TX TY B.
```

End PlusWf.

Section StarWf.

Variable A: Type.

Variable X: Set.

Variable Y: Type.

Variable TX: reduction_t A X.

Variable TY: reduction_t A Y.

Variable B: relation X.

Hypothesis HB: evolve TX TX B (star B).

Hypothesis HB': well_founded (trans (comp (plus B) (plus (TX (T _))))).

Theorem 3.12

```
Theorem star_wf_controlled: controlled TX TY B.
```

End StarWf.