Library Controlled

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.