Library NARNonFS_currSince

Require Import ComhCoq.Extras.LibTactics.


Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARMisc.

Lemma ovWait_nextSinceState_net m t x y i n :
  ovWaitStateNet m t x y i n -> nextSinceStateNet i n.

Theorem ovWait_nextSince_pending (n : Network) (m : Mode) (t x y : Time) (i : nat)
  (p : reachableNet n) :
  ovWaitStateNet m t x y i n -> pending i n p \/ exists t, nextSince m t i n p.

Theorem ovReady_nextSince_pending (n : Network) (m : Mode) (t : Time) (i : nat)
  (l : Position) (p : reachableNet n) :
  ovReadyStateNet m t l i n -> pending i n p \/ exists t, nextSince m t i n p.

Lemma pending_urgent i n n' p d :
  pending i n p -> n -ND- d -ND> n' -> False.
Theorem ovWait_zero_nextSince (n : Network) (m : Mode) (t y : Time) (i : nat)
  (p : reachableNet n) : ovWaitStateNet m t zeroTime y i n ->
  exists t, nextSince m t i n p.
Theorem switchBc_nextSince (n : Network) (m : Mode) (i : nat)
  (p : reachableNet n) : switchBcStateNet m i n -> exists t, nextSince m t i n p.

Theorem switchCurr_nextSince (n : Network) (m : Mode) (i : nat)
  (p : reachableNet n) : switchCurrStateNet i n ->
  exists t, nextSince m t i n p.
Theorem nonFS_currSince (m : Mode) (i : nat) (n : Network)
  (p : reachableNet n) : currModeNet m i n -> ~failSafe m ->
  exists t, currSince m t i n p.