{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base

module Ledger.Dijkstra.Specification.Gov.Actions (gs : _) (open GovStructure gs) where

open import Data.Nat.Properties using (+-0-monoid)
open import Data.Rational using (ℚ; 0ℚ; 1ℚ)

open import Tactic.Derive.Show

open import Ledger.Prelude as P hiding (yes; no)
open import Ledger.Core.Specification.ProtocolVersion


data GovRole : Type where
  CC DRep SPO : GovRole

GovRoleCredential : GovRole → Type
GovRoleCredential CC   = Credential
GovRoleCredential DRep = Credential
GovRoleCredential SPO  = KeyHash

data GovActionType : Type where
  NoConfidence        : GovActionType
  UpdateCommittee     : GovActionType
  NewConstitution     : GovActionType
  TriggerHardFork     : GovActionType
  ChangePParams       : GovActionType
  TreasuryWithdrawal  : GovActionType
  Info                : GovActionType

GovActionData : GovActionType → Type
GovActionData NoConfidence        = ⊤
GovActionData UpdateCommittee     = (Credential ⇀ Epoch) × ℙ Credential × ℚ
GovActionData NewConstitution     = DocHash × Maybe ScriptHash
GovActionData TriggerHardFork     = ProtVer
GovActionData ChangePParams       = PParamsUpdate
GovActionData TreasuryWithdrawal  = Withdrawals
GovActionData Info                = ⊤

record GovAction : Type where
  constructor ⟦_,_⟧ᵍᵃ
  field
    gaType : GovActionType
    gaData : GovActionData gaType

open GovAction public

-- Governance actions are uniquely identified by a `GovActionID`.
GovActionID : Type
GovActionID  = TxId × ℕ

data Vote : Type where
  yes no abstain  : Vote

record GovVoter : Type where
  constructor ⟦_,_⟧ᵍᵛ
  field
    gvRole       : GovRole
    gvCredential : GovRoleCredential gvRole

record Anchor : Type where
  -- context about why a vote was cast in a certain manner
  field
    url   : String
    hash  : DocHash -- abstract but instantiated with 32-bit hash type

record GovVote : Type where
  field
    gid         : GovActionID
    voter       : GovVoter
    vote        : Vote
    anchor      : Maybe Anchor

record GovVotes : Type where
  -- collects votes cast by members of each of the governance roles
  field
    gvCC   : Credential ⇀ Vote
    gvDRep : Credential ⇀ Vote
    gvSPO  : KeyHash ⇀ Vote

-- Vote Delegation
data VDeleg : Type where
  vDelegCredential   : Credential → VDeleg
  vDelegAbstain      : VDeleg
  vDelegNoConfidence : VDeleg

VoteDelegs : Type
VoteDelegs   = Credential ⇀ VDeleg

-- Hash Protection
NeedsHash : GovActionType → Type
NeedsHash NoConfidence        = GovActionID
NeedsHash UpdateCommittee     = GovActionID
NeedsHash NewConstitution     = GovActionID
NeedsHash TriggerHardFork     = GovActionID
NeedsHash ChangePParams       = GovActionID
NeedsHash TreasuryWithdrawal  = ⊤
NeedsHash Info                = ⊤

HashProtected : Type → Type
HashProtected A = A × GovActionID

Policy : Type
Policy = Maybe ScriptHash

record GovProposal : Type where
  field
    action      : GovAction
    prevAction  : NeedsHash (gaType action)  -- pointer to previous action
    policy      : Policy                     -- pointer to optional proposal policy
    deposit     : Coin                       -- to be returned to returnAddr
    returnAddr  : RewardAddress              -- reward address;  dep returned here when prop is removed
    anchor      : Anchor                     -- placeholder for further information about the proposal


-- state of an individual governance action
record GovActionState : Type where
  field
    votes       : GovVotes
    returnAddr  : RewardAddress
    expiresIn   : Epoch
    action      : GovAction
    prevAction  : NeedsHash (gaType action)

-- Governance Helper Functions
isGovVoterDRep : GovVoter → Maybe Credential
isGovVoterDRep $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{3745}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3752}{\htmlId{3752}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = just c
isGovVoterDRep _ = nothing

govVoterCredential : GovVoter → Credential
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{3859}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3866}{\htmlId{3866}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{3898}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3905}{\htmlId{3905}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = c
govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{3937}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3944}{\htmlId{3944}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = KeyHashObj kh

proposedCC : GovAction → ℙ Credential
proposedCC $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{4019}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{4037}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4038}{\htmlId{4038}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{4042}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{4046}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix}$ = dom x
proposedCC _ = ∅

DReps : Type
DReps = Credential ⇀ Epoch


record HasGovActionType (A : Type) : Type where
  field GovActionTypeOf : A → GovActionType
open HasGovActionType ⦃...⦄ public

record HasVoteDelegs {a} (A : Type a) : Type a where
  field VoteDelegsOf : A → VoteDelegs
open HasVoteDelegs ⦃...⦄ public

record HasGovAction (A : Type) : Type where
  field GovActionOf : A → GovAction
open HasGovAction ⦃...⦄ public

record HasGovVoter {a} (A : Type a) : Type a where
  field GovVoterOf : A → GovVoter
open HasGovVoter ⦃...⦄ public

record HasGovVotes {a} (A : Type a) : Type a where
  field GovVotesOf : A → GovVotes
open HasGovVotes ⦃...⦄ public

record HasVote {a} (A : Type a) : Type a where
  field VoteOf : A → Vote
open HasVote ⦃...⦄ public

record HasPolicy {a} (A : Type a) : Type a where
  field PolicyOf : A → Policy
open HasPolicy ⦃...⦄ public

record HasDReps {a} (A : Type a) : Type a where
  field DRepsOf : A → DReps
open HasDReps ⦃...⦄ public

record HasAnchor {a} (A : Type a) : Type a where
  field AnchorOf : A → Anchor
open HasAnchor ⦃...⦄ public

record HasDeposit {a} (A : Type a) : Type a where
  field DepositOf : A → Coin
open HasDeposit ⦃...⦄ public

instance
  HasGovActionType-GovAction : HasGovActionType GovAction
  HasGovActionType-GovAction .GovActionTypeOf = GovAction.gaType

  HasCast-GovAction-Sigma : HasCast GovAction (Σ GovActionType GovActionData)
  HasCast-GovAction-Sigma .cast x = x .gaType , x .gaData

  HasCast-HashProtected : ∀ {A : Type} → HasCast (HashProtected A) A
  HasCast-HashProtected .cast = proj₁

  HasCast-HashProtected-MaybeScriptHash : HasCast (HashProtected (DocHash × Maybe ScriptHash)) (Maybe ScriptHash)
  HasCast-HashProtected-MaybeScriptHash .cast = proj₂ ∘ proj₁

  HasGovVoter-GovVote : HasGovVoter GovVote
  HasGovVoter-GovVote .GovVoterOf = GovVote.voter

  HasVote-GovVote : HasVote GovVote
  HasVote-GovVote .VoteOf = GovVote.vote

  HasPolicy-GovProposal : HasPolicy GovProposal
  HasPolicy-GovProposal .PolicyOf = GovProposal.policy

  HasAnchor-GovProposal : HasAnchor GovProposal
  HasAnchor-GovProposal .AnchorOf = GovProposal.anchor

  HasDeposit-GovProposal : HasDeposit GovProposal
  HasDeposit-GovProposal .DepositOf = GovProposal.deposit

  HasGovAction-GovProposal : HasGovAction GovProposal
  HasGovAction-GovProposal .GovActionOf = GovProposal.action

  HasGovAction-GovActionState : HasGovAction GovActionState
  HasGovAction-GovActionState .GovActionOf = GovActionState.action

  HasGovActionType-GovProposal : HasGovActionType GovProposal
  HasGovActionType-GovProposal .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf

  HasGovActionType-GovActionState : HasGovActionType GovActionState
  HasGovActionType-GovActionState .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf

  HasGovVotes-GovActionState : HasGovVotes GovActionState
  HasGovVotes-GovActionState .GovVotesOf = GovActionState.votes

  HasRewardAddress-GovActionState : HasRewardAddress GovActionState
  HasRewardAddress-GovActionState .RewardAddressOf = GovActionState.returnAddr

  HasRewardAddress-GovProposal : HasRewardAddress GovProposal
  HasRewardAddress-GovProposal .RewardAddressOf = GovProposal.returnAddr

  unquoteDecl Show-GovRole        = derive-Show [ (quote GovRole , Show-GovRole) ]
  unquoteDecl DecEq-GovActionType = derive-DecEq ((quote GovActionType , DecEq-GovActionType) ∷ [])
  unquoteDecl DecEq-GovRole       = derive-DecEq ((quote GovRole , DecEq-GovRole) ∷ [])
  unquoteDecl DecEq-Vote          = derive-DecEq ((quote Vote    , DecEq-Vote)    ∷ [])
  unquoteDecl DecEq-VDeleg        = derive-DecEq ((quote VDeleg  , DecEq-VDeleg)  ∷ [])

  DecEq-GovVoter : DecEq GovVoter
  DecEq-GovVoter ._≟_ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7743}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7750}{\htmlId{7750}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7758}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7765}{\htmlId{7765}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
    with c ≟ c'
  ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7820}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7802}{\htmlId{7829}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{7830}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{7834}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{7838}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7840}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7845}{\htmlId{7845}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{7848}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7850}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7855}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{7858}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7860}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{7865}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7845}{\htmlId{7867}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7870}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{7874}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{7879}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7894}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7895}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7901}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7908}{\htmlId{7908}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{7916}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7923}{\htmlId{7923}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7930}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7932}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7937}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7939}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{7944}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7959}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7960}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{7966}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7973}{\htmlId{7973}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{7981}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7988}{\htmlId{7988}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7995}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7997}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8002}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8004}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8009}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8024}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8025}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8031}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8038}{\htmlId{8038}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{8046}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8053}{\htmlId{8053}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8060}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8062}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8067}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8069}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8074}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8089}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8090}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8096}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8103}{\htmlId{8103}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8111}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8118}{\htmlId{8118}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8129}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8103}{\htmlId{8134}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8136}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8118}{\htmlId{8138}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8143}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8147}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8149}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8155}{\htmlId{8155}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8157}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8159}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8165}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8166}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8173}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8155}{\htmlId{8184}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8185}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8189}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8193}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8195}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8200}{\htmlId{8200}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8203}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8205}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8210}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8213}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8215}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8220}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8200}{\htmlId{8222}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8225}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8229}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8234}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8249}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8250}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8256}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8263}{\htmlId{8263}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8271}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8278}{\htmlId{8278}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8285}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8287}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8292}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8294}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8299}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8314}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8315}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8321}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8328}{\htmlId{8328}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#427}{\htmlId{8336}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8343}{\htmlId{8343}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8350}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8352}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8357}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8359}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8364}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8379}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8380}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8386}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8393}{\htmlId{8393}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#430}{\htmlId{8401}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8408}{\htmlId{8408}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8415}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8417}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8422}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8424}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#7687}{\htmlId{8429}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8444}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8445}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8451}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8458}{\htmlId{8458}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8466}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8473}{\htmlId{8473}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{8484}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8458}{\htmlId{8489}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8491}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8473}{\htmlId{8493}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{8498}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8502}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8504}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8510}{\htmlId{8510}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8512}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8514}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8520}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8521}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#435}{\htmlId{8528}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8510}{\htmlId{8538}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8539}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{8543}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8547}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8549}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8554}{\htmlId{8554}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8557}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8559}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8564}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8567}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8569}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8574}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8554}{\htmlId{8576}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8579}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8583}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{8589}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8601}{\htmlId{8601}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{8617}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{8619}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8634}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{8636}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8637}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1912}{\htmlId{8643}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8601}{\htmlId{8653}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{8668}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8670}{\htmlClass{Function Operator}{\text{]}}}}\,
  \,\htmlId{8674}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8686}{\htmlId{8686}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{8698}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{8700}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8712}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{8714}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8715}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2273}{\htmlId{8721}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8686}{\htmlId{8730}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{8741}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{8743}{\htmlClass{Function Operator}{\text{]}}}}\,
  \,\htmlId{8747}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8759}{\htmlId{8759}{\htmlClass{Function}{\text{DecEq-Anchor}}}}\,        \,\htmlId{8779}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.DecEq.html#5150}{\htmlId{8781}{\htmlClass{Function}{\text{derive-DecEq}}}}\, \,\htmlId{8794}{\htmlClass{Symbol}{\text{((}}}\,\,\htmlId{8796}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1727}{\htmlId{8802}{\htmlClass{Record}{\text{Anchor}}}}\,  , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8759}{\htmlId{8812}{\htmlClass{Function}{\text{DecEq-Anchor}}}}\,\,\htmlId{8824}{\htmlClass{Symbol}{\text{)}}}\,  \,\href{Agda.Builtin.List.html#199}{\htmlId{8827}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Agda.Builtin.List.html#184}{\htmlId{8829}{\htmlClass{InductiveConstructor}{\text{[]}}}}\,\,\htmlId{8831}{\htmlClass{Symbol}{\text{)}}}\,

\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8834}{\htmlId{8834}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{8841}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{8843}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{8845}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8846}{\htmlId{8846}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{8847}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{8849}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8851}{\htmlId{8851}{\htmlClass{Bound}{\text{dA}}}}\, \,\htmlId{8854}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{8856}{\htmlClass{Record}{\text{DecEq}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8846}{\htmlId{8862}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8864}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{8866}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{8868}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8846}{\htmlId{8870}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8872}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{8874}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8846}{\htmlId{8876}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8878}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{8880}{\htmlClass{Datatype}{\text{Bool}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8834}{\htmlId{8885}{\htmlClass{Function}{\text{==-Set}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8892}{\htmlId{8892}{\htmlClass{Bound}{\text{xs}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8895}{\htmlId{8895}{\htmlClass{Bound}{\text{ys}}}}\, \,\htmlId{8898}{\htmlClass{Symbol}{\text{=}}}\,
    \,\href{Data.Bool.ListAction.html#927}{\htmlId{8904}{\htmlClass{Function}{\text{all}}}}\, \,\htmlId{8908}{\htmlClass{Symbol}{\text{(λ}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8911}{\htmlId{8911}{\htmlClass{Bound}{\text{x}}}}\, \,\htmlId{8913}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{8915}{\htmlClass{Function Operator}{\text{⌊}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8911}{\htmlId{8917}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Axiom.Set.html#11038}{\htmlId{8919}{\htmlClass{Function Operator}{\text{∈?}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8895}{\htmlId{8922}{\htmlClass{Bound}{\text{ys}}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{8925}{\htmlClass{Function Operator}{\text{⌋}}}}\,\,\htmlId{8926}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8928}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#2617}{\htmlId{8929}{\htmlClass{Function}{\text{setToList}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8892}{\htmlId{8939}{\htmlClass{Bound}{\text{xs}}}}\,\,\htmlId{8941}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{8943}{\htmlClass{Function Operator}{\text{∧}}}}\,
    \,\href{Data.Bool.ListAction.html#927}{\htmlId{8949}{\htmlClass{Function}{\text{all}}}}\, \,\htmlId{8953}{\htmlClass{Symbol}{\text{(λ}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8956}{\htmlId{8956}{\htmlClass{Bound}{\text{y}}}}\, \,\htmlId{8958}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{8960}{\htmlClass{Function Operator}{\text{⌊}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8956}{\htmlId{8962}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Axiom.Set.html#11038}{\htmlId{8964}{\htmlClass{Function Operator}{\text{∈?}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8892}{\htmlId{8967}{\htmlClass{Bound}{\text{xs}}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{8970}{\htmlClass{Function Operator}{\text{⌋}}}}\,\,\htmlId{8971}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8973}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#2617}{\htmlId{8974}{\htmlClass{Function}{\text{setToList}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8895}{\htmlId{8984}{\htmlClass{Bound}{\text{ys}}}}\,\,\htmlId{8986}{\htmlClass{Symbol}{\text{)}}}\,

\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{8989}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\htmlId{9006}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9008}{\htmlClass{Symbol}{\text{∀}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9010}{\htmlId{9010}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9012}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#890}{\htmlId{9014}{\htmlClass{Function}{\text{GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9010}{\htmlId{9028}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9030}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#890}{\htmlId{9032}{\htmlClass{Function}{\text{GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9010}{\htmlId{9046}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9048}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9050}{\htmlClass{Datatype}{\text{Bool}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9055}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#625}{\htmlId{9072}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \,\htmlId{9085}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9087}{\htmlClass{Function Operator}{\text{\_==\_}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9092}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{9109}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \,\htmlId{9125}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9126}{\htmlId{9126}{\htmlClass{Bound}{\text{m0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9131}{\htmlId{9131}{\htmlClass{Bound}{\text{s0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9136}{\htmlId{9136}{\htmlClass{Bound}{\text{q0}}}}\,\,\htmlId{9138}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9140}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9141}{\htmlId{9141}{\htmlClass{Bound}{\text{m1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9146}{\htmlId{9146}{\htmlClass{Bound}{\text{s1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9151}{\htmlId{9151}{\htmlClass{Bound}{\text{q1}}}}\,\,\htmlId{9153}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9155}{\htmlClass{Symbol}{\text{=}}}\,
    \,\htmlId{9161}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8834}{\htmlId{9162}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9169}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9126}{\htmlId{9170}{\htmlClass{Bound}{\text{m0}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9173}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9174}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9176}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9141}{\htmlId{9177}{\htmlClass{Bound}{\text{m1}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9180}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9181}{\htmlClass{Symbol}{\text{))}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9184}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{9186}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9131}{\htmlId{9187}{\htmlClass{Bound}{\text{s0}}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9190}{\htmlClass{Function Operator}{\text{==}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9146}{\htmlId{9193}{\htmlClass{Bound}{\text{s1}}}}\,\,\htmlId{9195}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9197}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{9199}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9136}{\htmlId{9200}{\htmlClass{Bound}{\text{q0}}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9203}{\htmlClass{Function Operator}{\text{==}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9151}{\htmlId{9206}{\htmlClass{Bound}{\text{q1}}}}\,\,\htmlId{9208}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9210}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#701}{\htmlId{9227}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \,\htmlId{9243}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9245}{\htmlClass{Function Operator}{\text{\_==\_}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9250}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#739}{\htmlId{9267}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \,\htmlId{9283}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9285}{\htmlClass{Function Operator}{\text{\_==\_}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9290}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#777}{\htmlId{9307}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \,\htmlId{9321}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9323}{\htmlClass{Function Operator}{\text{\_==\_}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9328}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#815}{\htmlId{9345}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9364}{\htmlId{9364}{\htmlClass{Bound}{\text{w0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9367}{\htmlId{9367}{\htmlClass{Bound}{\text{w1}}}}\, \,\htmlId{9370}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8834}{\htmlId{9372}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9379}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9364}{\htmlId{9380}{\htmlClass{Bound}{\text{w0}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9383}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9384}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9386}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9367}{\htmlId{9387}{\htmlClass{Bound}{\text{w1}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9390}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9391}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9393}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#853}{\htmlId{9410}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \,\htmlId{9415}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9417}{\htmlClass{Function Operator}{\text{\_==\_}}}}\,

\,\htmlId{9423}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9472}{\htmlId{9472}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{9485}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1292}{\htmlId{9487}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{9497}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1292}{\htmlId{9499}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{9509}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9511}{\htmlClass{Datatype}{\text{Bool}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9472}{\htmlId{9516}{\htmlClass{Function}{\text{==-GovAction}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9531}{\htmlId{9531}{\htmlClass{Bound}{\text{t0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9536}{\htmlId{9536}{\htmlClass{Bound}{\text{d0}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9545}{\htmlId{9545}{\htmlClass{Bound}{\text{t1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9550}{\htmlId{9550}{\htmlClass{Bound}{\text{d1}}}}\, \end{pmatrix}
    \,\htmlId{9561}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9531}{\htmlId{9566}{\htmlClass{Bound}{\text{t0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{9569}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9545}{\htmlId{9571}{\htmlClass{Bound}{\text{t1}}}}\,
\,\htmlId{9574}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{9578}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{9580}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{9586}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{9591}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8989}{\htmlId{9593}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\htmlId{9610}{\htmlClass{Bound}{\text{t1}}}\, \,\htmlId{9613}{\htmlClass{Bound}{\text{d0}}}\, \,\htmlId{9616}{\htmlClass{Bound}{\text{d1}}}\,
\,\htmlId{9619}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{9623}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{9625}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{9630}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{9632}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{9634}{\htmlClass{InductiveConstructor}{\text{false}}}}\,

\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{9641}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{9657}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9659}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{9661}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9662}{\htmlId{9662}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{9663}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9665}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{9667}{\htmlClass{Record}{\text{DecEq}}}}\, \,\htmlId{9673}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2470}{\htmlId{9674}{\htmlClass{Function}{\text{NeedsHash}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9662}{\htmlId{9684}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{9685}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{9687}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{9703}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#625}{\htmlId{9704}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,\,\htmlId{9716}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9718}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{9719}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9723}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{9725}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9729}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{9731}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{9740}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{9742}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{9758}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{9759}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,\,\htmlId{9774}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9776}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{9777}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9781}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{9783}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9787}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{9789}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{9798}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{9800}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{9816}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#701}{\htmlId{9817}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,\,\htmlId{9832}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9834}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{9835}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9839}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{9841}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9845}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{9847}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{9856}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{9858}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{9874}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#739}{\htmlId{9875}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,\,\htmlId{9890}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9892}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{9893}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9897}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{9899}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9903}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{9905}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{9914}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{9916}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{9932}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#777}{\htmlId{9933}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,\,\htmlId{9946}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9948}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{9949}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9953}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{9955}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{9959}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{9961}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{9970}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{9972}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{9988}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#815}{\htmlId{9989}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,\,\htmlId{10007}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10009}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10010}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10014}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10016}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10020}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{10022}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{10030}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{10032}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10048}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#853}{\htmlId{10049}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,\,\htmlId{10053}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10055}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10056}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10060}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10062}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10066}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{10068}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{10076}{\htmlClass{Symbol}{\text{⦄}}}\,

\,\htmlId{10079}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10128}{\htmlId{10128}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\htmlId{10143}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2903}{\htmlId{10145}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{10157}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2903}{\htmlId{10159}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{10171}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{10173}{\htmlClass{Datatype}{\text{Bool}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10128}{\htmlId{10178}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10193}{\htmlId{10193}{\htmlClass{Bound Operator}{\text{\_gp0}}}}\,\,\htmlId{10197}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{10199}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10223}{\htmlId{10223}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10226}{\htmlId{10226}{\htmlClass{Bound}{\text{b0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10229}{\htmlId{10229}{\htmlClass{Bound}{\text{c0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10232}{\htmlId{10232}{\htmlClass{Bound}{\text{d0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10235}{\htmlId{10235}{\htmlClass{Bound}{\text{e0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10238}{\htmlId{10238}{\htmlClass{Bound}{\text{f0}}}}\,\,\htmlId{10240}{\htmlClass{Symbol}{\text{)}}}\,
               \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10257}{\htmlId{10257}{\htmlClass{Bound Operator}{\text{\_gp1}}}}\,\,\htmlId{10261}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{10263}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10287}{\htmlId{10287}{\htmlClass{Bound}{\text{a1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10290}{\htmlId{10290}{\htmlClass{Bound}{\text{b1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10293}{\htmlId{10293}{\htmlClass{Bound}{\text{c1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10296}{\htmlId{10296}{\htmlClass{Bound}{\text{d1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10299}{\htmlId{10299}{\htmlClass{Bound}{\text{e1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10302}{\htmlId{10302}{\htmlClass{Bound}{\text{f1}}}}\,\,\htmlId{10304}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{10308}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1349}{\htmlId{10313}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10223}{\htmlId{10330}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10333}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1349}{\htmlId{10335}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10287}{\htmlId{10352}{\htmlClass{Bound}{\text{a1}}}}\,
\,\htmlId{10355}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10359}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{10361}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10367}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{10372}{\htmlClass{Symbol}{\text{=}}}\,
    \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9472}{\htmlId{10378}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{10391}{\htmlClass{Bound}{\text{a0}}}\, \,\htmlId{10394}{\htmlClass{Bound}{\text{a1}}}\,
    \,\href{Data.Bool.Base.html#1005}{\htmlId{10401}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10403}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10404}{\htmlClass{Bound}{\text{b0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10407}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10410}{\htmlClass{Bound}{\text{b1}}}\,\,\htmlId{10412}{\htmlClass{Symbol}{\text{)}}}\,
    \,\href{Data.Bool.Base.html#1005}{\htmlId{10418}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10420}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10421}{\htmlClass{Bound}{\text{c0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10424}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10427}{\htmlClass{Bound}{\text{c1}}}\,\,\htmlId{10429}{\htmlClass{Symbol}{\text{)}}}\,
    \,\href{Data.Bool.Base.html#1005}{\htmlId{10435}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10437}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10438}{\htmlClass{Bound}{\text{d0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10441}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10444}{\htmlClass{Bound}{\text{d1}}}\,\,\htmlId{10446}{\htmlClass{Symbol}{\text{)}}}\,
    \,\href{Data.Bool.Base.html#1005}{\htmlId{10452}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10454}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10455}{\htmlClass{Bound}{\text{e0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10458}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10461}{\htmlClass{Bound}{\text{e1}}}\,\,\htmlId{10463}{\htmlClass{Symbol}{\text{)}}}\,
    \,\href{Data.Bool.Base.html#1005}{\htmlId{10469}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10471}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10472}{\htmlClass{Bound}{\text{f0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10475}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10478}{\htmlClass{Bound}{\text{f1}}}\,\,\htmlId{10480}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{10484}{\htmlClass{Keyword}{\text{where}}}\,
    \,\htmlId{10494}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2903}{\htmlId{10499}{\htmlClass{Module}{\text{GovProposal}}}}\,
    \,\htmlId{10515}{\htmlClass{Keyword}{\text{instance}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10524}{\htmlId{10524}{\htmlClass{Function}{\text{\_}}}}\, \,\htmlId{10526}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9641}{\htmlId{10528}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\,
\,\htmlId{10544}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10548}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10550}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10555}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{10557}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{10559}{\htmlClass{InductiveConstructor}{\text{false}}}}\,


\,\htmlId{10567}{\htmlClass{Comment}{\text{-- return the DReps of A that expire in epoch e or later}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10624}{\htmlId{10624}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\htmlId{10638}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{10640}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{10646}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{10648}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{10659}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{10661}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{10667}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{10669}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10624}{\htmlId{10674}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10688}{\htmlId{10688}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{10690}{\htmlClass{Symbol}{\text{(\_}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10695}{\htmlId{10695}{\htmlClass{Bound}{\text{expEpoch}}}}\,\,\htmlId{10703}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{10705}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10688}{\htmlId{10707}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{10709}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10695}{\htmlId{10711}{\htmlClass{Bound}{\text{expEpoch}}}}\,

\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10721}{\htmlId{10721}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\htmlId{10735}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{10737}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10738}{\htmlId{10738}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{10740}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{10742}{\htmlClass{Primitive}{\text{Type}}}}\,\,\htmlId{10746}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10748}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10750}{\htmlId{10750}{\htmlClass{Bound}{\text{\_}}}}\, \,\htmlId{10752}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4932}{\htmlId{10754}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10738}{\htmlId{10763}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{10765}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{10767}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10738}{\htmlId{10769}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{10771}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{10773}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{10779}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4079}{\htmlId{10781}{\htmlClass{Function}{\text{DReps}}}}\,
\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10721}{\htmlId{10787}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10801}{\htmlId{10801}{\htmlClass{Bound}{\text{a}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10803}{\htmlId{10803}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{10805}{\htmlClass{Symbol}{\text{=}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#4102}{\htmlId{10807}{\htmlClass{Function}{\text{filterᵐ}}}}\, \,\htmlId{10815}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10624}{\htmlId{10816}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10803}{\htmlId{10830}{\htmlClass{Bound}{\text{e}}}}\,\,\htmlId{10831}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{10833}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4981}{\htmlId{10834}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10801}{\htmlId{10842}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{10843}{\htmlClass{Symbol}{\text{)}}}\,