Library NARMsgPosition

Require Import Equality.

Require Import ComhCoq.Extras.LibTactics.


Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.NetworkLanguage.
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.

Open Scope R_scope.

Theorem sent_outgoing (n : Network) (v : list BaseType) (t : Time) (i : nat)
  (p : reachableNet n) :
  sent v t i n p -> forall q : t < msgLatency,
  outgoing v (minusTime msgLatency t (Rlt_le t msgLatency q)) i n.

Theorem fst_sent (n : Network) (m : Mode) (t : Time) (i : nat)
  (p : reachableNet n) : nextSince m t i n p ->
  exists l0, sent [baseMode m, basePosition l0] t i n p.

Theorem sent_out_del (n : Network) (v : list BaseType) (i : nat)
  (p : reachableNet n) : sent v msgLatency i n p ->
  outgoing v zeroTime i n \/
  exists r l, delivered ([-v, l, r-]) zeroTime i n p.

Theorem sent_delivered (n : Network) (v : list BaseType) (t : Time) (i : nat)
  (p : reachableNet n) : sent v t i n p -> forall q : msgLatency < t,
  exists r l,
  delivered ([-v, l, r-]) (minusTime t msgLatency (Rlt_le msgLatency t q)) i n p.

Theorem sent_pos_bound (n : Network) (m : Mode) (t : Time) (i : nat)
  (l l0 : Position) (p : reachableNet n) :
  sent [baseMode m, basePosition l0] t i n p -> inPosNet l i n ->
  dist2d l l0 <= speedMax*t.

Theorem fst_delivered (n : Network) (m : Mode) (t : Time) (i : nat)
  (l : Position) (p : reachableNet n) :
  nextSince m t i n p -> inPosNet l i n -> forall q : msgLatency < t,
  exists l0 l1 r,
  delivered ([-[baseMode m, basePosition l0], l1, r-])
  (minusTime t msgLatency (Rlt_le msgLatency t q)) i n p /\
  dist2d l l0 <= speedMax*t.