{-# OPTIONS --without-K #-}
module Securability where
open import Basis
open import Spread.Baire
open import Dialogue as ๐
open import SystemT.Syntax
open import SystemT.Semantics
infixl 4 _โ_
data _โ_ (U : Node) (ฯ : Species) : Set where
spit : ฯ U โ U โ ฯ
bite : (โ x โ U โข x โ ฯ) โ U โ ฯ
_โฉ_โ_
: ๐
โ โ
โ Node
โ Species
โ Set
d โฉ U โ ฯ =
(ฮฑ : Point)
โ ฯ (U <++ ฮฑ [ ๐
[ d โ ฮฑ ] + โฃ U โฃ ])
_โฉ_โแต_
: โขแต (nat โ nat) โ nat
โ Node
โ Species
โ Set
F โฉ U โแต ฯ =
(ฮฑ : Point)
โ ฯ (U <++ ฮฑ [ tmโฆ F โงโ ฮฑ + โฃ U โฃ ])