NoPropSameDReps

{-# OPTIONS --safe #-}

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

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

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Prelude
open import Ledger.Conway.Specification.Properties txs abs

Claim (DReps unchanged if no gov proposals).

Informally.

If es is a NewEpochState, and if the GovState of es contains no governance proposals, then the set of activeDReps of es in Epoch e is equal to the set of activeDReps of es in the next epoch.

Formally.

prop≡∅⇒activeDReps-const : Epoch → NewEpochState → Type
prop≡∅⇒activeDReps-const e es =
  GovStateOf es ≡ [] → dom (activeDRepsOf es e) ≡ᵉ dom (activeDRepsOf es (sucᵉ e))

Proof. (coming soon)