```open import NeilPrelude1
open import Ord1

module Core1 where

-- We need lists of sets

data List1 (S : Set1) : Set1 where
[]      : List1 S
_∷_     : S → List1 S → List1 S

_++_ : {S : Set1} → List1 S → List1 S → List1 S
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)

[_] : {S : Set1} → S → List1 S
[ s ] = s ∷ []

-- Decoupledness Descriptors --

-- Rather than create a datatype for Dec, we use booleans so we can use existing
-- boolean proofs

Dec : Set
Dec = Bool

dec : Dec
dec = false

cau : Dec
cau = true

-- Signal Descriptors --

data SigDesc : Set1 where
E : Set → SigDesc
C : Set → SigDesc

SVDesc : Set1
SVDesc = List1 SigDesc

SigRep : SigDesc → Set
SigRep (C A) = A
SigRep (E A) = Maybe A

data SVRep : List1 SigDesc → Set1 where
⟨⟩  : SVRep []
_∷_ : {a : SigDesc} → {as : SVDesc} → SigRep a → SVRep as → SVRep (a ∷ as)

_+++_ : {as bs : SVDesc} → SVRep as → SVRep bs → SVRep (as ++ bs)
⟨⟩ +++ bs = bs
(a ∷ as) +++ bs = a ∷ (as +++ bs)

svsplit : {as bs : SVDesc} → SVRep (as ++ bs) → SVRep as 1×1 SVRep bs
svsplit {[]} asbs = ⟨⟩ & asbs
svsplit {_ ∷ AS} (a ∷ asbs) with svsplit {AS} asbs
... | as & bs = (a ∷ as) & bs

---------------------------------------------------------------------------------

Time : Set
Time = ℕ

Δt = Time

t0 = 0

-- Signal Function Representation --

infixl 91 _***_
infixl 90 _>>>_

data SF : SVDesc → SVDesc → Dec → Set1 where
prim    : {as bs : SVDesc} → {State : Set} → (Δt → State → SVRep as → State ×1 SVRep bs) → State    → SF as bs cau
dprim   : {as bs : SVDesc} → {State : Set} → (Δt → State → (SVRep as → State) 1×1 SVRep bs) → State → SF as bs dec
_>>>_   : {d₁ d₂ : Dec} → {as bs cs : SVDesc} → SF as bs d₁ → SF bs cs d₂                           → SF as cs (d₁ ∧ d₂)
_***_   : {d₁ d₂ : Dec} → {as bs cs ds : SVDesc} → SF as cs d₁ → SF bs ds d₂                        → SF (as ++ bs) (cs ++ ds) (d₁ ∨ d₂)
loop    : {d : Dec} → {as bs cs ds : SVDesc} → SF (as ++ cs) (bs ++ ds) d → SF ds cs dec            → SF as bs d
switch  : {d₁ d₂ : Dec} → {as bs : SVDesc} → {e : Set} → SF as (E e ∷ bs) d₁ → (e → SF as bs d₂)    → SF as bs (d₁ ∨ d₂)
dswitch : {d₁ d₂ : Dec} → {as bs : SVDesc} → {e : Set} → SF as (E e ∷ bs) d₁ → (e → SF as bs d₂)    → SF as bs (d₁ ∨ d₂)
weaken  : {d d' : Dec} → {as bs : SVDesc} → d ≤ d' → SF as bs d                                     → SF as bs d'

```