``` ```

# Study of controlled simulations

``` Require Export Theory. ```

## Relaxed expansion: Subsection 3.2

``` 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. ```

## Termination Guarantees: Subsection 3.3

``` 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. ```