ConstRwds

{-# OPTIONS --safe #-}

open import Ledger.Conway.Transaction
open import Ledger.Conway.Abstract

module Ledger.Conway.Epoch.Properties.ConstRwds
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Conway.Certs govStructure
open import Ledger.Conway.Epoch txs abs
open import Ledger.Prelude

- *Informally*. Rewards are left unchanged by the `NEWEPOCH`{.AgdaOperator} rule. That is, if and are two `NewEpochState`{.AgdaRecord}s such that `⇀⦇`{.AgdaDatatype} `,NEWEPOCH⦈`{.AgdaDatatype} , then the rewards of and are equal. - *Formally*.

dom-rwds-const : {e : Epoch} (es es' : NewEpochState)
  → _ ⊢ es ⇀⦇ e ,NEWEPOCH⦈ es' → Type

dom-rwds-const es es' step = dom (RewardsOf es) ≡ dom (RewardsOf es')

- *Proof*. *To appear* (in the module of the [formal ledger repository](\repourl)).