VoteDelegsVDeleg
Claim (voteDelegs
by credVoter
constructor).
Informally.
A CertState
has a DState
, a PState
, and a
GState
. The DState
contains a field
voteDelegs
which is a mapping from Credential
to
VDeleg
.
VDeleg
is a datatype with three constructors; the one of interest to
us here is vDelegCredential{.AgdaInductiveConstructor}, which takes a
Credential`{.AgdaDatatype}.
Now suppose we have a collection C
of credentials---for
instance, given d
: DState
, take
C
to be the domain of the voteDelegs
field
of d
. We could then obtain a set of VDeleg
s
by applying vDelegCredential{.AgdaInductiveConstructor} to
each element of
C`{.AgdaBound}.
The present property asserts that the set of VDeleg
s
that results from the application of
vDelegCredential
to the
domain of the voteDelegs
of d
contains the range
of the voteDelegs
of d
.
Formally.
voteDelegsVDeleg : DState → Type voteDelegsVDeleg d = range (VoteDelegsOf d) ⊆ mapˢ vDelegCredential (dom (VoteDelegsOf d))
Proof. (coming soon)