{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)

module Ledger.Dijkstra.Specification.Account
  (gs : GovStructure) (open GovStructure gs) where

open import Ledger.Prelude
open import Tactic.Derive.DecEq


DirectDeposits : Type
DirectDeposits = Credential ⇀ Coin


data BalanceInterval : Type where
  ⟦_,_⦆ : Coin → Coin → BalanceInterval
  ⟦_,∞⦆ : Coin → BalanceInterval
  ⟦0,_⦆ : Coin → BalanceInterval


data InBalanceInterval (c : Coin) : BalanceInterval → Type where
  bounded       : {lb ub : Coin}  → lb ≤ c → c < ub  → InBalanceInterval c $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#542}{\htmlId{600}{\htmlClass{Bound}{\text{lb}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Account.html#545}{\htmlId{605}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#352}{\htmlId{608}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\,
  \,\href{Ledger.Dijkstra.Specification.Account.html#612}{\htmlId{612}{\htmlClass{InductiveConstructor}{\text{lowerBounded}}}}\,  \,\htmlId{626}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{628}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#629}{\htmlId{629}{\htmlClass{Bound}{\text{lb}}}}\, \,\htmlId{632}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#154}{\htmlId{634}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{638}{\htmlClass{Symbol}{\text{}}}}\,     \,\htmlId{644}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#629}{\htmlId{646}{\htmlClass{Bound}{\text{lb}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{649}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#482}{\htmlId{651}{\htmlClass{Bound}{\text{c}}}}\,           \,\htmlId{663}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#463}{\htmlId{665}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#482}{\htmlId{683}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#629}{\htmlId{687}{\htmlClass{Bound}{\text{lb}}}}\, \\
  \,\href{Ledger.Dijkstra.Specification.Account.html#696}{\htmlId{696}{\htmlClass{InductiveConstructor}{\text{upperBounded}}}}\,  \,\htmlId{710}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{712}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#713}{\htmlId{713}{\htmlClass{Bound}{\text{ub}}}}\, \,\htmlId{716}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Prelude.Base.html#154}{\htmlId{718}{\htmlClass{Function}{\text{Coin}}}}\,\,\htmlId{722}{\htmlClass{Symbol}{\text{}}}}\,     \,\htmlId{728}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#482}{\htmlId{730}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasOrder.Core.html#646}{\htmlId{732}{\htmlClass{Field Operator}{\text{<}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#713}{\htmlId{734}{\htmlClass{Bound}{\text{ub}}}}\,           \,\htmlId{747}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#463}{\htmlId{749}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#482}{\htmlId{767}{\htmlClass{Bound}{\text{c}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#713}{\htmlId{773}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#425}{\htmlId{776}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\,


\,\htmlId{780}{\htmlClass{Keyword}{\text{instance}}}\,
  \,\href{Ledger.Dijkstra.Specification.Account.html#791}{\htmlId{791}{\htmlClass{Function}{\text{Dec-InBalanceInterval}}}}\, \,\htmlId{813}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#463}{\htmlId{815}{\htmlClass{Datatype}{\text{InBalanceInterval}}}}\, \,\href{Class.Decidable.Core.html#590}{\htmlId{833}{\htmlClass{Function Operator}{\text{⁇²}}}}\,
  \,\href{Ledger.Dijkstra.Specification.Account.html#791}{\htmlId{838}{\htmlClass{Function}{\text{Dec-InBalanceInterval}}}}\, \,\htmlId{860}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#861}{\htmlId{861}{\htmlClass{Bound}{\text{c}}}}\,\,\htmlId{862}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{864}{\htmlClass{Symbol}{\text{{}}}\,\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#867}{\htmlId{867}{\htmlClass{Bound}{\text{lb}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Account.html#872}{\htmlId{872}{\htmlClass{Bound}{\text{ub}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#352}{\htmlId{875}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\,\,\htmlId{876}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{878}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.Decidable.Core.html#273}{\htmlId{879}{\htmlClass{Field}{\text{dec}}}}\, \,\htmlId{883}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#867}{\htmlId{888}{\htmlClass{Bound}{\text{lb}}}}\, \,\href{Class.HasOrder.Core.html#1016}{\htmlId{891}{\htmlClass{Function Operator}{\text{≤?}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#861}{\htmlId{894}{\htmlClass{Bound}{\text{c}}}}\, \,\htmlId{896}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#861}{\htmlId{898}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasOrder.Core.html#1076}{\htmlId{900}{\htmlClass{Function Operator}{\text{<?}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#872}{\htmlId{903}{\htmlClass{Bound}{\text{ub}}}}\,
  \,\htmlId{908}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{912}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{914}{\htmlClass{InductiveConstructor}{\text{no}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#917}{\htmlId{917}{\htmlClass{Bound}{\text{¬p}}}}\,  \,\htmlId{921}{\htmlClass{Symbol}{\text{|}}}\, \,\htmlId{923}{\htmlClass{Symbol}{\text{\_}}}\,      \,\htmlId{930}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{932}{\htmlClass{InductiveConstructor}{\text{no}}}}\, \,\htmlId{935}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{937}{\htmlClass{Keyword}{\text{where}}}\, \,\htmlId{943}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#525}{\htmlId{944}{\htmlClass{InductiveConstructor}{\text{bounded}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#952}{\htmlId{952}{\htmlClass{Bound}{\text{lbp}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#956}{\htmlId{956}{\htmlClass{Bound}{\text{ubp}}}}\,\,\htmlId{959}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{961}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#917}{\htmlId{963}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#952}{\htmlId{966}{\htmlClass{Bound}{\text{lbp}}}}\,
  \,\htmlId{972}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{976}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{978}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#982}{\htmlId{982}{\htmlClass{Bound}{\text{p₁}}}}\, \,\htmlId{985}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{987}{\htmlClass{InductiveConstructor}{\text{no}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#990}{\htmlId{990}{\htmlClass{Bound}{\text{¬p₂}}}}\, \,\htmlId{994}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{996}{\htmlClass{InductiveConstructor}{\text{no}}}}\, \,\htmlId{999}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{1001}{\htmlClass{Keyword}{\text{where}}}\, \,\htmlId{1007}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#525}{\htmlId{1008}{\htmlClass{InductiveConstructor}{\text{bounded}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1016}{\htmlId{1016}{\htmlClass{Bound}{\text{lbp}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1020}{\htmlId{1020}{\htmlClass{Bound}{\text{ubp}}}}\,\,\htmlId{1023}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{1025}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#990}{\htmlId{1027}{\htmlClass{Bound}{\text{¬p₂}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1020}{\htmlId{1031}{\htmlClass{Bound}{\text{ubp}}}}\,
  \,\htmlId{1037}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{1041}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{1043}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1047}{\htmlId{1047}{\htmlClass{Bound}{\text{p₁}}}}\, \,\htmlId{1050}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{1052}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1056}{\htmlId{1056}{\htmlClass{Bound}{\text{p₂}}}}\, \,\htmlId{1059}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{1061}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\htmlId{1065}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#525}{\htmlId{1066}{\htmlClass{InductiveConstructor}{\text{bounded}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1047}{\htmlId{1074}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1056}{\htmlId{1077}{\htmlClass{Bound}{\text{p₂}}}}\,\,\htmlId{1079}{\htmlClass{Symbol}{\text{)}}}\,
  \,\href{Ledger.Dijkstra.Specification.Account.html#791}{\htmlId{1083}{\htmlClass{Function}{\text{Dec-InBalanceInterval}}}}\, \,\htmlId{1105}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1106}{\htmlId{1106}{\htmlClass{Bound}{\text{c}}}}\,\,\htmlId{1107}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{1109}{\htmlClass{Symbol}{\text{{}}}\,\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1112}{\htmlId{1112}{\htmlClass{Bound}{\text{lo}}}}\, \\\,\htmlId{1118}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{1120}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.Decidable.Core.html#273}{\htmlId{1121}{\htmlClass{Field}{\text{dec}}}}\, \,\htmlId{1125}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1112}{\htmlId{1130}{\htmlClass{Bound}{\text{lo}}}}\, \,\href{Class.HasOrder.Core.html#1016}{\htmlId{1133}{\htmlClass{Function Operator}{\text{≤?}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1106}{\htmlId{1136}{\htmlClass{Bound}{\text{c}}}}\,
  \,\htmlId{1140}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{1144}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{1146}{\htmlClass{InductiveConstructor}{\text{no}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1149}{\htmlId{1149}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{1152}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{1154}{\htmlClass{InductiveConstructor}{\text{no}}}}\,  \,\htmlId{1158}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{1161}{\htmlClass{Keyword}{\text{where}}}\, \,\htmlId{1167}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#612}{\htmlId{1168}{\htmlClass{InductiveConstructor}{\text{lowerBounded}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1181}{\htmlId{1181}{\htmlClass{Bound}{\text{lbp}}}}\,\,\htmlId{1184}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{1186}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1149}{\htmlId{1188}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1181}{\htmlId{1191}{\htmlClass{Bound}{\text{lbp}}}}\,\,\htmlId{1194}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{1198}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{1202}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{1204}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1208}{\htmlId{1208}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{1210}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{1212}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\htmlId{1216}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#612}{\htmlId{1217}{\htmlClass{InductiveConstructor}{\text{lowerBounded}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1208}{\htmlId{1230}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{1231}{\htmlClass{Symbol}{\text{)}}}\,
  \,\href{Ledger.Dijkstra.Specification.Account.html#791}{\htmlId{1235}{\htmlClass{Function}{\text{Dec-InBalanceInterval}}}}\, \,\htmlId{1257}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#1258}{\htmlId{1258}{\htmlClass{Bound}{\text{c}}}}\,\,\htmlId{1259}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{1261}{\htmlClass{Symbol}{\text{{}}}\,\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Account.html#1266}{\htmlId{1266}{\htmlClass{Bound}{\text{hi}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#425}{\htmlId{1269}{\htmlClass{InductiveConstructor Operator}{\text{⦆}}}}\,\,\htmlId{1270}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{1272}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.Decidable.Core.html#273}{\htmlId{1273}{\htmlClass{Field}{\text{dec}}}}\, \,\htmlId{1277}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1258}{\htmlId{1282}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasOrder.Core.html#1076}{\htmlId{1284}{\htmlClass{Function Operator}{\text{<?}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1266}{\htmlId{1287}{\htmlClass{Bound}{\text{hi}}}}\,
  \,\htmlId{1292}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{1296}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{1298}{\htmlClass{InductiveConstructor}{\text{no}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1301}{\htmlId{1301}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{1304}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{1306}{\htmlClass{InductiveConstructor}{\text{no}}}}\,  \,\htmlId{1310}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{1313}{\htmlClass{Keyword}{\text{where}}}\, \,\htmlId{1319}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#696}{\htmlId{1320}{\htmlClass{InductiveConstructor}{\text{upperBounded}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1333}{\htmlId{1333}{\htmlClass{Bound}{\text{ubp}}}}\,\,\htmlId{1336}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{1338}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1301}{\htmlId{1340}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1333}{\htmlId{1343}{\htmlClass{Bound}{\text{ubp}}}}\,\,\htmlId{1346}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{1350}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{1354}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{1356}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1360}{\htmlId{1360}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{1362}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{1364}{\htmlClass{InductiveConstructor}{\text{yes}}}}\, \,\htmlId{1368}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Account.html#696}{\htmlId{1369}{\htmlClass{InductiveConstructor}{\text{upperBounded}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1360}{\htmlId{1382}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{1383}{\htmlClass{Symbol}{\text{)}}}\,

  \,\htmlId{1388}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#1400}{\htmlId{1400}{\htmlClass{Function}{\text{DecEq-BalanceInterval}}}}\, \,\htmlId{1422}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.DecEq.html#5150}{\htmlId{1424}{\htmlClass{Function}{\text{derive-DecEq}}}}\,
    \,\htmlId{1441}{\htmlClass{Symbol}{\text{((}}}\,\,\htmlId{1443}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#321}{\htmlId{1449}{\htmlClass{Datatype}{\text{BalanceInterval}}}}\, , \,\href{Ledger.Dijkstra.Specification.Account.html#1400}{\htmlId{1467}{\htmlClass{Function}{\text{DecEq-BalanceInterval}}}}\,\,\htmlId{1488}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Agda.Builtin.List.html#199}{\htmlId{1490}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Agda.Builtin.List.html#184}{\htmlId{1492}{\htmlClass{InductiveConstructor}{\text{[]}}}}\,\,\htmlId{1494}{\htmlClass{Symbol}{\text{)}}}\,


\,\href{Ledger.Dijkstra.Specification.Account.html#1498}{\htmlId{1498}{\htmlClass{Function}{\text{AccountBalanceIntervals}}}}\, \,\htmlId{1522}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{1524}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Dijkstra.Specification.Account.html#1498}{\htmlId{1529}{\htmlClass{Function}{\text{AccountBalanceIntervals}}}}\, \,\htmlId{1553}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{1555}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#633}{\htmlId{1566}{\htmlClass{Function Operator}{\text{⇀}}}}\, \,\href{Ledger.Dijkstra.Specification.Account.html#321}{\htmlId{1568}{\htmlClass{Datatype}{\text{BalanceInterval}}}}\,