Library Applications
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.