Lvc.IL.EventsActivated

Require Import List.
Require Export Util Relations Val Exp AutoIndTac Relations2 Events StateType.

Set Implicit Arguments.

Definition activated {S} `{StateType S} (σ:S) :=
  ∃ ext σ´, step σ (EvtExtern ext) σ´.

Lemma activated_star_reach S `{StateType S} (σ σ´ σ´´:S)
: activated σ´´
  → star2 step σ nil σ´´
  → star2 step σ nil σ´
  → star2 step σ´ nil σ´´.

Lemma activated_normal S `{StateType S} (σ:S)
  : activated σ
    → normal2 step σ
    → False.


Lemma both_activated S `{StateType S} (σ1 σ2 σ3:S)
: star2 step σ1 nil σ2
  → star2 step σ1 nil σ3
  → activated σ2
  → activated σ3
  → σ2 = σ3.

Lemma activated_star_eq S `{StateType S} (σ1 σ2:S)
: star2 step σ1 nil σ2
  → activated σ1
  → σ1 = σ2.

Lemma activated_normal_star S `{StateType S} (σ σ´ σ´´:S)
  : star2 step σ nil σ´
    → activated σ´
    → star2 step σ nil σ´´
    → normal2 step σ´´
    → False.

Lemma no_activated_tau_step {S} `{StateType S} (σ σ´:S)
 : activated σ
  → step σ EvtTau σ´
  → False.