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.