``` ```

# Application to the bisimulation case

``` Require Export Settings. Require Import Theory. Section Modular.   Variables A X: Type.   Variable TX: reduction_t A X.   Let F := Comp (chaining_l (expand TX TX)) (chaining_r (bisim TX TX)).   Let G := Comp (star (X:=X)) (Union2 (identity (X:=X) (Y:=X)) (constant (bisim TX TX))).   Lemma F_mon: monotonic TX TX F.   Lemma G_wmon: wmonotonic TX TX G.   Lemma FG: contains F G.   Lemma G_reverse: forall R, eeq (trans (G R)) (G (trans R)).   Variable R: relation X.   Hypothesis HRt: evolve_t TX TX R (F R).   Hypothesis HRa: evolve_a TX TX R (G R).   Hypothesis HRt': evolve_t TX TX (trans R) (F (trans R)).   Hypothesis HRa': evolve_a TX TX (trans R) (G (trans R)). ```
Theorem 2.5
```   Theorem upto: incl R (bisim TX TX). End Modular. Section Controlled.   Variables A X: Type.   Variable TX: reduction_t A X.   Variables B B': relation X.   Hypothesis HB: bicontrolled TX B.   Hypothesis HB': bicontrolled TX B'.   Let F := chaining_r (X:=X) (bisim TX TX).   Let G := Comp (star (X:=X)) (Union2 (identity (X:=X) (Y:=X)) (constant (bisim TX TX))).   Let F_mon: monotonic TX TX F.   Let FG: contains F G.   Let BG: contains (chaining_l (star B)) G.   Let B'G: contains (chaining_l (star B')) G.   Variable R: relation X.   Hypothesis HRt: evolve_t TX TX R (comp (star B) (F R)).   Hypothesis HRa: evolve_a TX TX R (G R).   Hypothesis HRt': evolve_t TX TX (trans R) (comp (star B') (F (trans R))).   Hypothesis HRa': evolve_a TX TX (trans R) (G (trans R)). ```
Theorem 3.6
```   Theorem upto_ctrl: incl R (bisim TX TX). End Controlled. ```