Library NAROvlpTime

Require Import Equality.

Require Import ComhCoq.Extras.LibTactics.


Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.

Theorem pending_urgent (n n' : Network) (d : Delay) (i : nat) (p : reachableNet n) :
  pending i n p -> ~ n -ND- d -ND> n'.
Theorem pending_time1 (n : Network) (m : Mode) (i : nat)
  (u x y : Time) (p : reachableNet n) :
  pending i n p -> ovWaitStateNet m u x y i n -> exists m0 q,
  u = addTime (waitTime m0 m q) (period m).
Theorem pending_time2 (n : Network) (m : Mode) (i : nat)
  (u : Time) (l : Position) (p : reachableNet n) :
  pending i n p -> ovReadyStateNet m u l i n ->
  exists m0 q, u = addTime (waitTime m0 m q) (period m).

Theorem nextSince_ovWait_ovReady_time (n : Network) (m : Mode) (i : nat)
  (t u x y : Time) (l : Position) (p : reachableNet n) :
  (nextSince m t i n p -> ovWaitStateNet m u x y i n ->
  exists m0 q, addTime t x = waitTime m0 m q
  /\ addTime u y = addTime x (period m)) /\
  (nextSince m t i n p -> ovReadyStateNet m u l i n ->
  exists m0 q,
  addTime t u = addTime (waitTime m0 m q) (period m)).
Theorem nextSince_switchBc_lower (n : Network) (m : Mode) (i : nat)
  (t : Time) (p : reachableNet n) :
  nextSince m t i n p -> switchBcStateNet m i n ->
  msgLatency + Rmax adaptNotif transMax < t.
Theorem nextSince_switchCurr_lower (n : Network) (m : Mode) (i : nat)
  (t : Time) (p : reachableNet n) :
  nextSince m t i n p -> switchCurrStateNet i n ->
  msgLatency + Rmax adaptNotif transMax < t.