Library Main

This file was written by Colm Bhandal, PhD student, Foundations and Methods group, School of Computer Science and Statistics, Trinity College, Dublin, Ireland.

In this file is the main result. We could also include any other results of interest here if time allowed it.

*************************** Standard Imports

Require Import Reals.
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.EntityLanguage.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARNonFS_currSince.
Require Import ComhCoq.NARMisc.
Require Import ComhCoq.NARIncomp.
Require Import ComhCoq.NARTop.

Theorem safety_aux (n : Network) (X : reachableNet n) (e1 e2 : Entity)
  (i j : nat) (H : (i <> j)%nat) (H0 : e1 @ i .: n) (H1 : e2 @ j .: n)
  (x : Distance) (Heqx : x = mkDistance (dist2d e1 e2)) (mdc : Distance) (m1 : Mode)
  (Heqm1 : m1 = e1) (m2 : Mode) (Heqm2 : m2 = e2) (Heqmdc : mdc = minDistComp m1 m2)
  (H2 : x < mdc) (H3 : ~ failSafe m1) (H4 : ~ failSafe m2) (H5 : currModeNet m1 i n)
  (H6 : currModeNet m2 j n) (t1 : Time) (H7 : currSince m1 t1 i n X) (t2 : Time)
  (H8 : currSince m2 t2 j n X) (H9 : msgLatency + Rmax adaptNotif transMax < t1)
  (H10 : msgLatency + Rmax adaptNotif transMax < t2) (H11 : t1 <= t2) : False.

Theorem safety (n : Network) : reachableNet n -> safe n.

This page has been generated by coqdoc