From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude finite.
From Coq Require Import FinFun FunctionalExtensionality Reals.
From VLSM.Lib Require Import Preamble ListSetExtras StdppExtras.
From VLSM.Lib Require Import NatExtras Measurable.[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
[Loading ML file equations_plugin.cmxs (using legacy method) ... done]
From VLSM.Core Require Import VLSM VLSMProjections Plans Composition Equivocation.
From VLSM.Core Require Import SubProjectionTraces.
From VLSM.Core Require Import Equivocation.NoEquivocation.
From VLSM.Core Require Import Equivocators.Equivocators.
From VLSM.Core Require Import Equivocators.MessageProperties.

Core: VLSM Equivocator Composition

Given a composition X of VLSMs, we can model equivocator behavior by creating an equivocator composition which replaces each component of X with its equivocator version and strengthens the composition constraint to allow no (additional) equivocations, that is, all messages being received must have been previously sent by one of the (equivocator) VLSMs in the composition.

Extracting equivocator traces from equivocator composition traces

To recover the equivocator trace for the regular composition X from the traces of the equivocator composition, we'll assume that only the first state copy of each machine is observable in the composition and we ignore the activity corresponding to any other state copy, including the forks.

This amounts to removing from the trace all transitions in which the state copy index is not 1, forgetting the additional components of the label, and keeping only the copy of index 1 for each machine.

Section sec_fully_equivocating_composition.

Context
  {message : Type}
  `{finite.Finite index}
  (IM : index -> VLSM message)
  `{forall i : index, HasBeenSentCapability (IM i)}
  `{forall i : index, HasBeenReceivedCapability (IM i)}
  (Free := free_composite_vlsm IM)
  .

Definition equivocator_IM
  (i : index)
  : VLSM message
  :=
  equivocator_vlsm (IM i).

Definition equivocating_indices
  (index_listing : list index)
  (s : composite_state equivocator_IM)
  : list index
  :=
  filter (fun i => is_equivocating_state (IM i) (s i)) index_listing.

Lemma equivocating_indices_initially_empty
  (index_listing : list index)
  (s : composite_state equivocator_IM)
  (Hs : composite_initial_state_prop equivocator_IM s)
  : equivocating_indices index_listing s = [].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
Hs: composite_initial_state_prop equivocator_IM s
equivocating_indices index_listing s = []
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
Hs: composite_initial_state_prop equivocator_IM s
equivocating_indices index_listing s = []
  apply Forall_filter_nil.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
Hs: composite_initial_state_prop equivocator_IM s
Forall
  (λ a : index, ¬ is_equivocating_state (IM a) (s a))
  index_listing
  apply Forall_forall.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
Hs: composite_initial_state_prop equivocator_IM s
∀ x : index,
  x ∈ index_listing
  → ¬ is_equivocating_state (IM x) (s x)
  intros i _.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
Hs: composite_initial_state_prop equivocator_IM s
i: index
¬ is_equivocating_state (IM i) (s i)
  specialize (Hs i).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
i: index
Hs: initial_state_prop (s i)
¬ is_equivocating_state (IM i) (s i)
  destruct Hs as [Hs _].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
i: index
Hs: is_singleton_state (IM i) (s i)
¬ is_equivocating_state (IM i) (s i)
  by congruence.
Qed.

Section sec_equivocating_indices_BasicEquivocation.

Context
  (threshold : R)
  `{ReachableThreshold index Ci threshold}
  .

Program Instance equivocating_indices_BasicEquivocation :
  BasicEquivocation (composite_state equivocator_IM) index Ci threshold
  := {
    is_equivocating := fun s v => v ∈ equivocating_indices (enum index) s ;
    state_validators := fun s => list_to_set(enum index)
  }.
Next Obligation.message, index: Type
IM: index → VLSM message
EqDecision0: EqDecision index
H: finite.Finite index
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
x: composite_state equivocator_IM
y: index
Decision (y ∈ equivocating_indices (enum index) x)
Proof.message, index: Type
IM: index → VLSM message
EqDecision0: EqDecision index
H: finite.Finite index
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
x: composite_state equivocator_IM
y: index
Decision (y ∈ equivocating_indices (enum index) x)
  by typeclasses eauto.
Qed.

Lemma equivocating_indices_equivocating_validators
  : forall s, equivocating_validators s ≡@{Ci} list_to_set(equivocating_indices (enum index) s).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
∀ s : composite_state equivocator_IM,
  equivocating_validators s
  ≡ list_to_set (equivocating_indices (enum index) s)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
∀ s : composite_state equivocator_IM,
  equivocating_validators s
  ≡ list_to_set (equivocating_indices (enum index) s)
  intros s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
equivocating_validators s
≡ list_to_set (equivocating_indices (enum index) s)
  apply set_eq_fin_set.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
set_eq (elements (equivocating_validators s))
  (elements
     (list_to_set
        (equivocating_indices (enum index) s)))
  unfold equivocating_validators, is_equivocating.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
set_eq
  (elements
     (filter
        (λ v : index,
           (let
              (is_equivocating, is_equivocating_dec,
               state_validators,
               equivocating_validators,
               equivocation_fault, not_heavy) :=
              equivocating_indices_BasicEquivocation in
            is_equivocating) s v) (state_validators s)))
  (elements
     (list_to_set
        (equivocating_indices (enum index) s)))
  simpl.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
set_eq
  (elements
     (filter
        (λ v : index,
           v ∈ equivocating_indices (enum index) s)
        (list_to_set (enum index))))
  (elements
     (list_to_set
        (equivocating_indices (enum index) s)))
  split; intro Hin
  ; rewrite !elem_of_elements, elem_of_filter, !elem_of_list_to_set.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
Hin: index
Hin ∈ equivocating_indices (enum index) s
∧ Hin ∈ enum index
→ Hin ∈ equivocating_indices (enum index) s
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
Hin: index
Hin ∈ equivocating_indices (enum index) s
→ Hin ∈ equivocating_indices (enum index) s
  ∧ Hin ∈ enum index
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
Hin: index
Hin ∈ equivocating_indices (enum index) s
∧ Hin ∈ enum index
→ Hin ∈ equivocating_indices (enum index) s by intros [].
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s: composite_state equivocator_IM
Hin: index
Hin ∈ equivocating_indices (enum index) s
→ Hin ∈ equivocating_indices (enum index) s
  ∧ Hin ∈ enum index by split; auto using elem_of_enum.
Qed.

Lemma eq_equivocating_indices_equivocation_fault :
  forall s1 s2,
    list_to_set (equivocating_indices (enum index) s1) ≡@{Ci}
    list_to_set (equivocating_indices (enum index) s2) ->
      equivocation_fault s1 = equivocation_fault s2.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
∀ s1 s2 : composite_state equivocator_IM,
  list_to_set (equivocating_indices (enum index) s1)
  ≡ list_to_set (equivocating_indices (enum index) s2)
  → equivocation_fault s1 = equivocation_fault s2
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
∀ s1 s2 : composite_state equivocator_IM,
  list_to_set (equivocating_indices (enum index) s1)
  ≡ list_to_set (equivocating_indices (enum index) s2)
  → equivocation_fault s1 = equivocation_fault s2
  intros s1 s2 Heq.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq: list_to_set
  (equivocating_indices (enum index) s1)
≡ list_to_set
    (equivocating_indices (enum index) s2)
equivocation_fault s1 = equivocation_fault s2
  rewrite <- !equivocating_indices_equivocating_validators in Heq.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq: equivocating_validators s1
≡ equivocating_validators s2
equivocation_fault s1 = equivocation_fault s2
  unfold equivocation_fault.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq: equivocating_validators s1
≡ equivocating_validators s2
sum_weights (equivocating_validators s1) =
sum_weights (equivocating_validators s2)
  apply set_eq_fin_set in Heq as [Heq1 Heq2].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq1: elements (equivocating_validators s1)
⊆ elements (equivocating_validators s2)
Heq2: elements (equivocating_validators s2)
⊆ elements (equivocating_validators s1)
sum_weights (equivocating_validators s1) =
sum_weights (equivocating_validators s2)
  apply sum_weights_subseteq_list in Heq1, Heq2;
    [| by apply NoDup_elements..].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq1: (sum_weights_list
   (elements (equivocating_validators s1)) <=
 sum_weights_list
   (elements (equivocating_validators s2)))%R
Heq2: (sum_weights_list
   (elements (equivocating_validators s2)) <=
 sum_weights_list
   (elements (equivocating_validators s1)))%R
sum_weights (equivocating_validators s1) =
sum_weights (equivocating_validators s2)
  by apply Rle_antisym.
Qed.

Lemma eq_equivocating_indices_equivocation_fault' :
  forall s1 s2,
    list_to_set (equivocating_indices (enum index) s1)
      ≡@{Ci}
    list_to_set (equivocating_indices (enum index) s2) ->
      equivocation_fault s1 = equivocation_fault s2.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
∀ s1 s2 : composite_state equivocator_IM,
  list_to_set (equivocating_indices (enum index) s1)
  ≡ list_to_set (equivocating_indices (enum index) s2)
  → equivocation_fault s1 = equivocation_fault s2
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
∀ s1 s2 : composite_state equivocator_IM,
  list_to_set (equivocating_indices (enum index) s1)
  ≡ list_to_set (equivocating_indices (enum index) s2)
  → equivocation_fault s1 = equivocation_fault s2
  intros s1 s2 Heq.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq: list_to_set
  (equivocating_indices (enum index) s1)
≡ list_to_set
    (equivocating_indices (enum index) s2)
equivocation_fault s1 = equivocation_fault s2
  rewrite <- !equivocating_indices_equivocating_validators in Heq.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq: equivocating_validators s1
≡ equivocating_validators s2
equivocation_fault s1 = equivocation_fault s2
  apply set_equiv_subseteq in Heq as [Heq1 Heq2].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
threshold: R
Ci: Type
Hm: Measurable index
H2: ElemOf index Ci
H3: Empty Ci
H4: Singleton index Ci
H5: Union Ci
H6: Intersection Ci
H7: Difference Ci
H8: Elements index Ci
EqDecision1: EqDecision index
H9: FinSet index Ci
H10: ReachableThreshold index Ci threshold
s1, s2: composite_state equivocator_IM
Heq1: equivocating_validators s1
⊆ equivocating_validators s2
Heq2: equivocating_validators s2
⊆ equivocating_validators s1
equivocation_fault s1 = equivocation_fault s2
  by apply Rle_antisym; apply sum_weights_subseteq.
Qed.

End sec_equivocating_indices_BasicEquivocation.

The statement below is obvious a transition cannot make an already equivocating component non-equivocating.

Lemma equivocators_transition_preserves_equivocating_indices
  (index_listing : list index)
  (s : composite_state equivocator_IM)
  (iom oom : option message)
  (l : composite_label equivocator_IM)
  (s0 : composite_state equivocator_IM)
  (Ht : composite_transition equivocator_IM l (s0, iom) = (s, oom))
  : equivocating_indices index_listing s0 ⊆ equivocating_indices index_listing s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
equivocating_indices index_listing s0
⊆ equivocating_indices index_listing s
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
equivocating_indices index_listing s0
⊆ equivocating_indices index_listing s
  intros i Hi.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hi: i ∈ equivocating_indices index_listing s0
i ∈ equivocating_indices index_listing s
  apply elem_of_list_filter.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hi: i ∈ equivocating_indices index_listing s0
is_equivocating_state (IM i) (s i) ∧ i ∈ index_listing
  apply elem_of_list_filter in Hi.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hi: is_equivocating_state (IM i) (s0 i)
∧ i ∈ index_listing
is_equivocating_state (IM i) (s i) ∧ i ∈ index_listing
  split; [| by apply Hi].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hi: is_equivocating_state (IM i) (s0 i)
∧ i ∈ index_listing
is_equivocating_state (IM i) (s i)
  destruct Hi as [Hi _].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hi: is_equivocating_state (IM i) (s0 i)
is_equivocating_state (IM i) (s i)
  intro Hsi.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hi: is_equivocating_state (IM i) (s0 i)
Hsi: is_singleton_state (IM i) (s i)
False elim Hi.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hi: is_equivocating_state (IM i) (s0 i)
Hsi: is_singleton_state (IM i) (s i)
is_singleton_state (IM i) (s0 i) clear Hi.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hsi: is_singleton_state (IM i) (s i)
is_singleton_state (IM i) (s0 i) unfold is_singleton_state in *.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: composite_transition equivocator_IM l (s0, iom) =
(s, oom)
i: index
Hsi: equivocator_state_n (s i) = 1
equivocator_state_n (s0 i) = 1
  simpl in *.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
l: composite_label equivocator_IM
s0: composite_state equivocator_IM
Ht: (let (i, li) := l in
 let (si', om') :=
   equivocator_transition (IM i) li (s0 i, iom) in
 (state_update equivocator_IM s0 i si', om')) =
(s, oom)
i: index
Hsi: equivocator_state_n (s i) = 1
equivocator_state_n (s0 i) = 1
  destruct l as (j, lj).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
s: composite_state equivocator_IM
iom, oom: option message
j: index
lj: label (equivocator_IM j)
s0: composite_state equivocator_IM
Ht: (let (si', om') :=
   equivocator_transition (IM j) lj (s0 j, iom) in
 (state_update equivocator_IM s0 j si', om')) =
(s, oom)
i: index
Hsi: equivocator_state_n (s i) = 1
equivocator_state_n (s0 i) = 1
  case_match; inversion Ht; subst; clear Ht.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
iom, oom: option message
j: index
lj: label (equivocator_IM j)
s0: composite_state equivocator_IM
e: equivocator_state (IM j)
H2: equivocator_transition (IM j) lj (s0 j, iom) =
(e, oom)
i: index
Hsi: equivocator_state_n
  (state_update equivocator_IM s0 j e i) = 1
equivocator_state_n (s0 i) = 1
  destruct (decide (i = j)); subst; state_update_simpl; [| done].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
index_listing: list index
iom, oom: option message
j: index
lj: label (equivocator_IM j)
s0: composite_state equivocator_IM
e: equivocator_state (IM j)
H2: equivocator_transition (IM j) lj (s0 j, iom) =
(e, oom)
Hsi: equivocator_state_n e = 1
equivocator_state_n (s0 j) = 1
  by revert Hsi; apply equivocator_transition_reflects_singleton_state with iom oom lj.
Qed.

Lemma equivocators_transition_cannot_decrease_state_size
  l s iom s' oom
  (Ht : composite_transition equivocator_IM l (s, iom) = (s', oom))
  : forall eqv, equivocator_state_n (s eqv) <= equivocator_state_n (s' eqv).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
l: composite_label equivocator_IM
s: composite_state equivocator_IM
iom: option message
s': composite_state equivocator_IM
oom: option message
Ht: composite_transition equivocator_IM l (s, iom) =
(s', oom)
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
l: composite_label equivocator_IM
s: composite_state equivocator_IM
iom: option message
s': composite_state equivocator_IM
oom: option message
Ht: composite_transition equivocator_IM l (s, iom) =
(s', oom)
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
  intro eqv.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
l: composite_label equivocator_IM
s: composite_state equivocator_IM
iom: option message
s': composite_state equivocator_IM
oom: option message
Ht: composite_transition equivocator_IM l (s, iom) =
(s', oom)
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n (s' eqv)
  destruct l as [j lj]; cbn in Ht.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
j: index
lj: label (equivocator_IM j)
s: composite_state equivocator_IM
iom: option message
s': composite_state equivocator_IM
oom: option message
Ht: (let (si', om') :=
   equivocator_transition (IM j) lj (s j, iom) in
 (state_update equivocator_IM s j si', om')) =
(s', oom)
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n (s' eqv)
  destruct (equivocator_transition _ _ _) as [sj' om'] eqn: Htj.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
j: index
lj: label (equivocator_IM j)
s: composite_state equivocator_IM
iom: option message
s': composite_state equivocator_IM
oom: option message
sj': equivocator_state (IM j)
om': option message
Htj: equivocator_transition (IM j) lj (s j, iom) =
(sj', om')
Ht: (state_update equivocator_IM s j sj', om') =
(s', oom)
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n (s' eqv)
  apply equivocator_transition_cannot_decrease_state_size in Htj.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
j: index
lj: label (equivocator_IM j)
s: composite_state equivocator_IM
iom: option message
s': composite_state equivocator_IM
oom: option message
sj': equivocator_state (IM j)
om': option message
Htj: equivocator_state_n (s j)
≤ equivocator_state_n sj'
Ht: (state_update equivocator_IM s j sj', om') =
(s', oom)
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n (s' eqv)
  inversion Ht; subst; clear Ht.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
j: index
lj: label (equivocator_IM j)
s: composite_state equivocator_IM
iom, oom: option message
sj': equivocator_state (IM j)
Htj: equivocator_state_n (s j)
≤ equivocator_state_n sj'
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n
    (state_update equivocator_IM s j sj' eqv)
  by destruct (decide (j = eqv)); subst; state_update_simpl.
Qed.

Lemma equivocators_plan_cannot_decrease_state_size
  (s : composite_state equivocator_IM)
  (plan : list (composite_plan_item equivocator_IM))
  (s' := snd (composite_apply_plan equivocator_IM s plan))
  : forall eqv, equivocator_state_n (s eqv) <= equivocator_state_n (s' eqv).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
plan: list (composite_plan_item equivocator_IM)
s':= (composite_apply_plan equivocator_IM s plan).2: state (composite_type equivocator_IM)
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
plan: list (composite_plan_item equivocator_IM)
s':= (composite_apply_plan equivocator_IM s plan).2: state (composite_type equivocator_IM)
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
  intro eqv.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
plan: list (composite_plan_item equivocator_IM)
s':= (composite_apply_plan equivocator_IM s plan).2: state (composite_type equivocator_IM)
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n (s' eqv) subst s'.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
plan: list (composite_plan_item equivocator_IM)
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s plan).2
       eqv)
  induction plan using rev_ind.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s []).2 eqv)
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
x: composite_plan_item equivocator_IM
plan: list (composite_plan_item equivocator_IM)
eqv: index
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s
        plan).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s
        (plan ++ [x])).2 eqv)
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
eqv: index
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s []).2 eqv) by cbn; lia.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
x: composite_plan_item equivocator_IM
plan: list (composite_plan_item equivocator_IM)
eqv: index
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s
        plan).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s
        (plan ++ [x])).2 eqv) rewrite (composite_apply_plan_app equivocator_IM s plan).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
x: composite_plan_item equivocator_IM
plan: list (composite_plan_item equivocator_IM)
eqv: index
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((composite_apply_plan equivocator_IM s
        plan).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((let (aitems, afinal) :=
        composite_apply_plan equivocator_IM s plan in
      let (a'items, a'final) :=
        composite_apply_plan equivocator_IM afinal [x] in
      (aitems ++ a'items, a'final)).2 eqv)
    destruct (composite_apply_plan equivocator_IM s plan) as [junk s1].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
x: composite_plan_item equivocator_IM
plan: list (composite_plan_item equivocator_IM)
eqv: index
junk: list transition_item
s1: state (composite_type equivocator_IM)
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n ((junk, s1).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((let (a'items, a'final) :=
        composite_apply_plan equivocator_IM s1 [x] in
      (junk ++ a'items, a'final)).2 eqv)
    destruct x as [l im].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
l: label (composite_type equivocator_IM)
im: option message
plan: list (composite_plan_item equivocator_IM)
eqv: index
junk: list transition_item
s1: state (composite_type equivocator_IM)
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n ((junk, s1).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((let (a'items, a'final) :=
        composite_apply_plan equivocator_IM s1
          [{| label_a := l; input_a := im |}] in
      (junk ++ a'items, a'final)).2 eqv)
    unfold composite_apply_plan.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
l: label (composite_type equivocator_IM)
im: option message
plan: list (composite_plan_item equivocator_IM)
eqv: index
junk: list transition_item
s1: state (composite_type equivocator_IM)
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n ((junk, s1).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((let (a'items, a'final) :=
        _apply_plan s1
          [{| label_a := l; input_a := im |}] in
      (junk ++ a'items, a'final)).2 eqv)
    unfold _apply_plan.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
l: label (composite_type equivocator_IM)
im: option message
plan: list (composite_plan_item equivocator_IM)
eqv: index
junk: list transition_item
s1: state (composite_type equivocator_IM)
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n ((junk, s1).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((let (a'items, a'final) :=
        let (final, items) :=
          foldr _apply_plan_folder (s1, [])
            (rev [{| label_a := l; input_a := im |}]) in
        (rev items, final) in
      (junk ++ a'items, a'final)).2 eqv)
    cbn -[composite_transition].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
l: label (composite_type equivocator_IM)
im: option message
plan: list (composite_plan_item equivocator_IM)
eqv: index
junk: list transition_item
s1: state (composite_type equivocator_IM)
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n ((junk, s1).2 eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((let (a'items, a'final) :=
        let (final, items) :=
          let (dest, out) :=
            composite_transition equivocator_IM l
              (s1, im) in
          (dest,
           [{|
              l := l;
              input := im;
              destination := dest;
              output := out
            |}]) in
        (rev items, final) in
      (junk ++ a'items, a'final)).2 eqv)
    match goal with
      |- context [composite_transition equivocator_IM l ?som] =>
      destruct (composite_transition equivocator_IM l som) eqn: Htrans
    end.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
l: label (composite_type equivocator_IM)
im: option message
plan: list (composite_plan_item equivocator_IM)
eqv: index
junk: list transition_item
s1: state (composite_type equivocator_IM)
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n ((junk, s1).2 eqv)
c: composite_state equivocator_IM
o: option message
Htrans: composite_transition equivocator_IM l
  (s1, im) = (c, o)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((junk ++
      rev
        [{|
           l := l;
           input := im;
           destination := c;
           output := o
         |}], c).2 eqv)
    apply equivocators_transition_cannot_decrease_state_size with (eqv := eqv) in Htrans.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: composite_state equivocator_IM
l: label (composite_type equivocator_IM)
im: option message
plan: list (composite_plan_item equivocator_IM)
eqv: index
junk: list transition_item
s1: state (composite_type equivocator_IM)
IHplan: equivocator_state_n (s eqv)
≤ equivocator_state_n ((junk, s1).2 eqv)
c: composite_state equivocator_IM
o: option message
Htrans: equivocator_state_n (s1 eqv)
≤ equivocator_state_n (c eqv)
equivocator_state_n (s eqv)
≤ equivocator_state_n
    ((junk ++
      rev
        [{|
           l := l;
           input := im;
           destination := c;
           output := o
         |}], c).2 eqv)
    by cbn in *; lia.
Qed.

Lemma equivocators_pre_trace_cannot_decrease_state_size
  s s' tr
  (Htr : finite_constrained_trace_from_to (free_composite_vlsm equivocator_IM) s s' tr)
  : forall eqv, equivocator_state_n (s eqv) <= equivocator_state_n (s' eqv).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm equivocator_IM) s s' tr
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm equivocator_IM) s s' tr
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
  apply trace_to_plan_to_trace_from_to in Htr.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: apply_plan
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM)) s
  (trace_to_plan
     (preloaded_with_all_messages_vlsm
        (free_composite_vlsm equivocator_IM)) tr) =
(tr, s')
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
  specialize (equivocators_plan_cannot_decrease_state_size s (trace_to_plan _ tr)) as Hmon.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: apply_plan
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM)) s
  (trace_to_plan
     (preloaded_with_all_messages_vlsm
        (free_composite_vlsm equivocator_IM)) tr) =
(tr, s')
Hmon: ∀ (s' :=
   (composite_apply_plan equivocator_IM s
      (trace_to_plan
         (preloaded_with_all_messages_vlsm
            (free_composite_vlsm equivocator_IM))
         tr)).2) (eqv : index),
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
∀ eqv : index,
  equivocator_state_n (s eqv)
  ≤ equivocator_state_n (s' eqv)
  by replace (composite_apply_plan _ _ _) with (tr, s') in Hmon.
Qed.

Lemma equivocators_pre_trace_preserves_equivocating_state
  s s' tr
  (Htr : finite_constrained_trace_from_to (free_composite_vlsm equivocator_IM) s s' tr)
  : forall eqv, is_equivocating_state (IM eqv) (s eqv) -> is_equivocating_state (IM eqv) (s' eqv).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm equivocator_IM) s s' tr
∀ eqv : index,
  is_equivocating_state (IM eqv) (s eqv)
  → is_equivocating_state (IM eqv) (s' eqv)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm equivocator_IM) s s' tr
∀ eqv : index,
  is_equivocating_state (IM eqv) (s eqv)
  → is_equivocating_state (IM eqv) (s' eqv)
  unfold is_equivocating_state, is_singleton_state.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm equivocator_IM) s s' tr
∀ eqv : index,
  equivocator_state_n (s eqv) ≠ 1
  → equivocator_state_n (s' eqv) ≠ 1
  intros eqv Hseqv.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm equivocator_IM) s s' tr
eqv: index
Hseqv: equivocator_state_n (s eqv) ≠ 1
equivocator_state_n (s' eqv) ≠ 1
  apply equivocators_pre_trace_cannot_decrease_state_size  with (eqv := eqv) in Htr.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm equivocator_IM))
tr: list transition_item
eqv: index
Htr: equivocator_state_n (s eqv)
≤ equivocator_state_n (s' eqv)
Hseqv: equivocator_state_n (s eqv) ≠ 1
equivocator_state_n (s' eqv) ≠ 1
  by cbv in *; lia.
Qed.

Context
  (equivocators_free_vlsm := free_composite_vlsm equivocator_IM)
  .

Definition equivocators_no_equivocations_constraint
  :=
  no_equivocations_additional_constraint equivocator_IM (free_constraint equivocator_IM).

Definition equivocators_no_equivocations_vlsm
  : VLSM message
  :=
  composite_vlsm equivocator_IM equivocators_no_equivocations_constraint.

Lemma equivocators_no_equivocations_vlsm_incl_equivocators_free
  : VLSM_incl equivocators_no_equivocations_vlsm equivocators_free_vlsm.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
VLSM_incl equivocators_no_equivocations_vlsm
  equivocators_free_vlsm
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
VLSM_incl equivocators_no_equivocations_vlsm
  equivocators_free_vlsm
  apply basic_VLSM_incl.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
strong_incl_initial_state_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM)
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
weak_incl_initial_message_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM)
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
weak_incl_valid_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM)
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
weak_incl_transition_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM)
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
strong_incl_initial_state_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM) by cbv; intros s Hn n; specialize (Hn n); split_and!; itauto.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
weak_incl_initial_message_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM) by intro; intros; apply initial_message_is_valid.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
weak_incl_valid_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM) by intros l s om Hiv _ _; apply Hiv.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
weak_incl_transition_preservation
  (constrained_vlsm_machine
     (free_composite_vlsm equivocator_IM)
     equivocators_no_equivocations_constraint)
  (free_composite_vlsm_machine equivocator_IM) by destruct 1.
Qed.

Lemma preloaded_equivocators_no_equivocations_vlsm_incl_PreFree :
  VLSM_incl
    (preloaded_with_all_messages_vlsm equivocators_no_equivocations_vlsm)
    (preloaded_with_all_messages_vlsm equivocators_free_vlsm).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
VLSM_incl
  (preloaded_with_all_messages_vlsm
     equivocators_no_equivocations_vlsm)
  (preloaded_with_all_messages_vlsm
     equivocators_free_vlsm)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
VLSM_incl
  (preloaded_with_all_messages_vlsm
     equivocators_no_equivocations_vlsm)
  (preloaded_with_all_messages_vlsm
     equivocators_free_vlsm)
  by apply basic_VLSM_incl_preloaded; [intro | inversion 1 | intro].
Qed.

Lemma equivocators_initial_state_size
  (is : composite_state equivocator_IM)
  (His : composite_initial_state_prop equivocator_IM is)
  (eqv : index)
  : equivocator_state_n (is eqv) = 1.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
is: composite_state equivocator_IM
His: composite_initial_state_prop equivocator_IM is
eqv: index
equivocator_state_n (is eqv) = 1
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
is: composite_state equivocator_IM
His: composite_initial_state_prop equivocator_IM is
eqv: index
equivocator_state_n (is eqv) = 1
  by destruct (His eqv).
Qed.

An indexed set of MachineDescriptors, one for each equivocating machine in the composition.

This will be used to project composite_states and composite_transition_items from the composition of equivocators to the composition of their corresponding components.

Definition equivocator_descriptors : Type := forall (eqv : index), MachineDescriptor (IM eqv).

Generalizes the proper_descriptor definition to equivocator_descriptors. Basically, an indexed set is proper w.r.t. a composite_state one can obtain through it a valid projection of the composite_state to the non-equivocating universe.

Definition proper_equivocator_descriptors
  (eqv_descriptors : equivocator_descriptors)
  (s : state equivocators_free_vlsm)
  : Prop
  := forall
    (eqv : index),
    proper_descriptor (IM eqv) (eqv_descriptors eqv) (s eqv).

Same as above, but disallowing equivocation.

Definition not_equivocating_equivocator_descriptors
  (eqv_descriptors : equivocator_descriptors)
  (s : state equivocators_free_vlsm)
  : Prop
  := forall
    (eqv : index),
    existing_descriptor (IM eqv) (eqv_descriptors eqv) (s eqv).

#[export] Instance not_equivocating_equivocator_descriptors_dec
  : RelDecision not_equivocating_equivocator_descriptors.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
RelDecision not_equivocating_equivocator_descriptors
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
RelDecision not_equivocating_equivocator_descriptors
  intros eqv_descriptors s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
Decision
  (not_equivocating_equivocator_descriptors
     eqv_descriptors s)
  apply @Decision_iff with (P :=
    Forall (fun eqv => existing_descriptor (IM eqv) (eqv_descriptors eqv) (s eqv)) (enum index)).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
Forall
  (λ eqv : index,
     existing_descriptor (IM eqv)
       (eqv_descriptors eqv) (s eqv)) (enum index)
↔ not_equivocating_equivocator_descriptors
    eqv_descriptors s
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
Decision
  (Forall
     (λ eqv : index,
        existing_descriptor 
          (IM eqv) (eqv_descriptors eqv) 
          (s eqv)) (enum index))
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
Forall
  (λ eqv : index,
     existing_descriptor (IM eqv)
       (eqv_descriptors eqv) (s eqv)) (enum index)
↔ not_equivocating_equivocator_descriptors
    eqv_descriptors s rewrite Forall_forall.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
(∀ x : index,
   x ∈ enum index
   → existing_descriptor (IM x) (eqv_descriptors x)
       (s x))
↔ not_equivocating_equivocator_descriptors
    eqv_descriptors s apply forall_proper.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
∀ x : index,
  (x ∈ enum index
   → existing_descriptor (IM x) (eqv_descriptors x)
       (s x))
  ↔ existing_descriptor (IM x) (eqv_descriptors x)
      (s x) intros.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
x: index
(x ∈ enum index
 → existing_descriptor (IM x) (eqv_descriptors x)
     (s x))
↔ existing_descriptor (IM x) (eqv_descriptors x) (s x)
    split; [| done].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
x: index
(x ∈ enum index
 → existing_descriptor (IM x) (eqv_descriptors x)
     (s x))
→ existing_descriptor (IM x) (eqv_descriptors x) (s x)
    by intro Henum; apply Henum, elem_of_enum.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
Decision
  (Forall
     (λ eqv : index,
        existing_descriptor (IM eqv)
          (eqv_descriptors eqv) (s eqv)) (enum index)) apply Forall_dec.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
∀ x : index,
  Decision
    (existing_descriptor (IM x) (eqv_descriptors x)
       (s x)) intro eqv.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
Decision
  (existing_descriptor (IM eqv) (eqv_descriptors eqv)
     (s eqv))
    by apply existing_descriptor_dec.
Qed.

Lemma not_equivocating_equivocator_descriptors_proper
  (eqv_descriptors : equivocator_descriptors)
  (s : state equivocators_free_vlsm)
  (Hne : not_equivocating_equivocator_descriptors eqv_descriptors s)
  : proper_equivocator_descriptors eqv_descriptors s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
Hne: not_equivocating_equivocator_descriptors
  eqv_descriptors s
proper_equivocator_descriptors eqv_descriptors s
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
Hne: not_equivocating_equivocator_descriptors
  eqv_descriptors s
proper_equivocator_descriptors eqv_descriptors s
  by intro eqv; apply existing_descriptor_proper, Hne.
Qed.

Definition zero_descriptor
  (eqv : index)
  : MachineDescriptor (IM eqv)
  := Existing 0.

Lemma zero_descriptor_not_equivocating
  (s : state equivocators_free_vlsm)
  : not_equivocating_equivocator_descriptors zero_descriptor s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state equivocators_free_vlsm
not_equivocating_equivocator_descriptors
  zero_descriptor s
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state equivocators_free_vlsm
not_equivocating_equivocator_descriptors
  zero_descriptor s
  by intro eqv; eexists.
Qed.

Lemma zero_descriptor_proper
  (s : state equivocators_free_vlsm)
  : proper_equivocator_descriptors zero_descriptor s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state equivocators_free_vlsm
proper_equivocator_descriptors zero_descriptor s
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state equivocators_free_vlsm
proper_equivocator_descriptors zero_descriptor s
  apply not_equivocating_equivocator_descriptors_proper.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state equivocators_free_vlsm
not_equivocating_equivocator_descriptors
  zero_descriptor s
  by apply zero_descriptor_not_equivocating.
Qed.

Lemma proper_equivocator_descriptors_state_update_eqv
  (eqv_descriptors : equivocator_descriptors)
  (s : state equivocators_free_vlsm)
  (eqv : index)
  (si : state (equivocator_IM eqv))
  (Hsi_proper : proper_descriptor (IM eqv) (eqv_descriptors eqv) (s eqv))
  (Hproper : proper_equivocator_descriptors eqv_descriptors (state_update equivocator_IM s eqv si))
  : proper_equivocator_descriptors eqv_descriptors s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
si: state (equivocator_IM eqv)
Hsi_proper: proper_descriptor (IM eqv)
  (eqv_descriptors eqv) 
  (s eqv)
Hproper: proper_equivocator_descriptors
  eqv_descriptors
  (state_update equivocator_IM s eqv si)
proper_equivocator_descriptors eqv_descriptors s
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
si: state (equivocator_IM eqv)
Hsi_proper: proper_descriptor (IM eqv)
  (eqv_descriptors eqv) 
  (s eqv)
Hproper: proper_equivocator_descriptors
  eqv_descriptors
  (state_update equivocator_IM s eqv si)
proper_equivocator_descriptors eqv_descriptors s
  intro eqv'.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
si: state (equivocator_IM eqv)
Hsi_proper: proper_descriptor (IM eqv)
  (eqv_descriptors eqv) 
  (s eqv)
Hproper: proper_equivocator_descriptors
  eqv_descriptors
  (state_update equivocator_IM s eqv si)
eqv': index
proper_descriptor (IM eqv') (eqv_descriptors eqv')
  (s eqv')
  specialize (Hproper eqv').message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
si: state (equivocator_IM eqv)
Hsi_proper: proper_descriptor (IM eqv)
  (eqv_descriptors eqv) 
  (s eqv)
eqv': index
Hproper: proper_descriptor (IM eqv')
  (eqv_descriptors eqv')
  (state_update equivocator_IM s eqv si eqv')
proper_descriptor (IM eqv') (eqv_descriptors eqv')
  (s eqv')
  by destruct (decide (eqv = eqv')); subst; state_update_simpl.
Qed.

Definition equivocators_state_project
  (eqv_descriptors : equivocator_descriptors)
  (s : state equivocators_free_vlsm)
  : state Free
  :=
  fun (eqv : index) =>
  equivocator_state_descriptor_project (s eqv) (eqv_descriptors eqv).

Definition lift_to_equivocators_state
  (s : state Free)
  (eqv : index)
  : state (equivocator_IM eqv)
  :=
  mk_singleton_state _ (s eqv).

Lemma lift_initial_to_equivocators_state
  (s : state Free)
  (Hs : initial_state_prop Free s)
  : initial_state_prop equivocators_no_equivocations_vlsm (lift_to_equivocators_state s).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state Free
Hs: initial_state_prop s
initial_state_prop (lift_to_equivocators_state s)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state Free
Hs: initial_state_prop s
initial_state_prop (lift_to_equivocators_state s)
  cbn in Hs |- *; unfold composite_initial_state_prop in Hs |- *.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: state Free
Hs: ∀ n : index, initial_state_prop (s n)
∀ n : index,
  initial_state_prop (lift_to_equivocators_state s n)
  by intro i; specialize (Hs i).
Qed.

Definition newmachine_descriptors_list
  (index_listing : list index)
  (descriptors : equivocator_descriptors)
  : list index
  := @filter _ _ _ (fun i => is_newmachine_descriptor (IM i) (descriptors i))
   (fun i => newmachine_descriptor_dec (IM i) (descriptors i)) index_listing.

A very useful operation on equivocator_descriptorss is updating the state corresponding to a component.

Definition equivocator_descriptors_update
  (s : equivocator_descriptors)
  (i : index)
  (si : MachineDescriptor (IM i))
  (j : index)
  : MachineDescriptor (IM j)
  :=
  match decide (j = i) with
  | left e => eq_rect_r (fun i => MachineDescriptor (IM i)) si e
  | _ => s j
  end.

The next few results describe several properties of the equivocator_descriptors_update operation.

Lemma equivocator_descriptors_update_neq
  (s : equivocator_descriptors)
  (i : index)
  (si : MachineDescriptor (IM i))
  (j : index)
  (Hneq : j <> i)
  : equivocator_descriptors_update s i si j = s j.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
j: index
Hneq: j ≠ i
equivocator_descriptors_update s i si j = s j
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
j: index
Hneq: j ≠ i
equivocator_descriptors_update s i si j = s j
  by unfold equivocator_descriptors_update; case_decide.
Qed.

A generalized version of equivocator_descriptors_update_eq parametric on the hypothesis equating the indices.

Lemma equivocator_descriptors_update_eq_rew
  (s : equivocator_descriptors)
  (i : index)
  (si : MachineDescriptor (IM i))
  (j : index)
  (Heq : j = i)
  : equivocator_descriptors_update s i si j = eq_rect_r (fun i => MachineDescriptor (IM i)) si Heq.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
j: index
Heq: j = i
equivocator_descriptors_update s i si j =
eq_rect_r (λ i : index, MachineDescriptor (IM i)) si
  Heq
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
j: index
Heq: j = i
equivocator_descriptors_update s i si j =
eq_rect_r (λ i : index, MachineDescriptor (IM i)) si
  Heq
  unfold equivocator_descriptors_update.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
j: index
Heq: j = i
match decide (j = i) with
| left e =>
    eq_rect_r (λ i : index, MachineDescriptor (IM i))
      si e
| right _ => s j
end =
eq_rect_r (λ i : index, MachineDescriptor (IM i)) si
  Heq
  case_decide; [| done].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
j: index
Heq, H2: j = i
eq_rect_r (λ i : index, MachineDescriptor (IM i)) si
  H2 =
eq_rect_r (λ i : index, MachineDescriptor (IM i)) si
  Heq
  by f_equal; apply Eqdep_dec.UIP_dec.
Qed.

Lemma equivocator_descriptors_update_eq
  (s : equivocator_descriptors)
  (i : index)
  (si : MachineDescriptor (IM i))
  : equivocator_descriptors_update s i si i = si.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
equivocator_descriptors_update s i si i = si
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
equivocator_descriptors_update s i si i = si
  by rewrite equivocator_descriptors_update_eq_rew with (Heq := eq_refl).
Qed.

Lemma equivocator_descriptors_update_id
  (s : equivocator_descriptors)
  (i : index)
  (si : MachineDescriptor (IM i))
  (Heq : s i = si)
  : equivocator_descriptors_update s i si = s.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
Heq: s i = si
equivocator_descriptors_update s i si = s
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
Heq: s i = si
equivocator_descriptors_update s i si = s
  apply functional_extensionality_dep_good.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
Heq: s i = si
∀ x : index,
  equivocator_descriptors_update s i si x = s x
  intro j.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si: MachineDescriptor (IM i)
Heq: s i = si
j: index
equivocator_descriptors_update s i si j = s j
  destruct (decide (j = i)); subst.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
equivocator_descriptors_update s i (s i) i = s i
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i, j: index
n: j ≠ i
equivocator_descriptors_update s i (s i) j = s j
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
equivocator_descriptors_update s i (s i) i = s i by apply equivocator_descriptors_update_eq.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i, j: index
n: j ≠ i
equivocator_descriptors_update s i (s i) j = s j by apply equivocator_descriptors_update_neq.
Qed.

Lemma equivocator_descriptors_update_twice
  (s : equivocator_descriptors)
  (i : index)
  (si si' : MachineDescriptor (IM i))
  : equivocator_descriptors_update (equivocator_descriptors_update s i si) i si'
  = equivocator_descriptors_update s i si'.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
equivocator_descriptors_update
  (equivocator_descriptors_update s i si) i si' =
equivocator_descriptors_update s i si'
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
equivocator_descriptors_update
  (equivocator_descriptors_update s i si) i si' =
equivocator_descriptors_update s i si'
  apply functional_extensionality_dep_good.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
∀ x : index,
  equivocator_descriptors_update
    (equivocator_descriptors_update s i si) i si' x =
  equivocator_descriptors_update s i si' x
  intro j.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
j: index
equivocator_descriptors_update
  (equivocator_descriptors_update s i si) i si' j =
equivocator_descriptors_update s i si' j
  destruct (decide (j = i)); subst.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
equivocator_descriptors_update
  (equivocator_descriptors_update s i si) i si' i =
equivocator_descriptors_update s i si' i
message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
j: index
n: j ≠ i
equivocator_descriptors_update
  (equivocator_descriptors_update s i si) i si' j =
equivocator_descriptors_update s i si' j
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
equivocator_descriptors_update
  (equivocator_descriptors_update s i si) i si' i =
equivocator_descriptors_update s i si' i by rewrite equivocator_descriptors_update_eq, equivocator_descriptors_update_eq.
  -message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
s: equivocator_descriptors
i: index
si, si': MachineDescriptor (IM i)
j: index
n: j ≠ i
equivocator_descriptors_update
  (equivocator_descriptors_update s i si) i si' j =
equivocator_descriptors_update s i si' j by rewrite !equivocator_descriptors_update_neq.
Qed.

Lemma equivocators_state_project_state_update_eqv
  (eqv_descriptors : equivocator_descriptors)
  (s : state equivocators_free_vlsm)
  (eqv : index)
  (seqv : state (equivocator_IM eqv))
  : let si :=  match eqv_descriptors eqv with
    | NewMachine sn => sn
    | Existing i =>
      match equivocator_state_project seqv i with
      | Some si => si
      | None => equivocator_state_zero seqv
      end
    end in
  equivocators_state_project eqv_descriptors (state_update equivocator_IM s eqv seqv)
  = state_update IM (equivocators_state_project eqv_descriptors s) eqv si.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
seqv: state (equivocator_IM eqv)
let si :=
  match eqv_descriptors eqv with
  | NewMachine sn => sn
  | Existing i =>
      match equivocator_state_project seqv i with
      | Some si => si
      | None => equivocator_state_zero seqv
      end
  end in
equivocators_state_project eqv_descriptors
  (state_update equivocator_IM s eqv seqv) =
state_update IM
  (equivocators_state_project eqv_descriptors s) eqv
  si
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
seqv: state (equivocator_IM eqv)
let si :=
  match eqv_descriptors eqv with
  | NewMachine sn => sn
  | Existing i =>
      match equivocator_state_project seqv i with
      | Some si => si
      | None => equivocator_state_zero seqv
      end
  end in
equivocators_state_project eqv_descriptors
  (state_update equivocator_IM s eqv seqv) =
state_update IM
  (equivocators_state_project eqv_descriptors s) eqv
  si
  cbn; extensionality ieqv.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
seqv: state (equivocator_IM eqv)
ieqv: index
equivocators_state_project eqv_descriptors
  (state_update equivocator_IM s eqv seqv) ieqv =
state_update IM
  (equivocators_state_project eqv_descriptors s) eqv
  match eqv_descriptors eqv with
  | NewMachine sn => sn
  | Existing i =>
      match equivocator_state_project seqv i with
      | Some si => si
      | None => equivocator_state_zero seqv
      end
  end ieqv
  unfold equivocators_state_project, state_update.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
eqv_descriptors: equivocator_descriptors
s: state equivocators_free_vlsm
eqv: index
seqv: state (equivocator_IM eqv)
ieqv: index
equivocator_state_descriptor_project
  match decide (ieqv = eqv) with
  | left e =>
      eq_rect_r
        (λ i : index, state (equivocator_IM i)) seqv e
  | right _ => s ieqv
  end (eqv_descriptors ieqv) =
match decide (ieqv = eqv) with
| left e =>
    eq_rect_r (λ i : index, state (IM i))
      match eqv_descriptors eqv with
      | NewMachine sn => sn
      | Existing i =>
          match equivocator_state_project seqv i with
          | Some si => si
          | None => equivocator_state_zero seqv
          end
      end e
| right _ =>
    equivocator_state_descriptor_project (s ieqv)
      (eqv_descriptors ieqv)
end
  by case_decide; subst.
Qed.

Lemma equivocators_initial_state_project
  (es : state equivocators_free_vlsm)
  (Hes : initial_state_prop equivocators_free_vlsm es)
  (eqv_descriptors : equivocator_descriptors)
  (Heqv : proper_equivocator_descriptors eqv_descriptors es)
  : initial_state_prop Free (equivocators_state_project eqv_descriptors es).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
Hes: initial_state_prop es
eqv_descriptors: equivocator_descriptors
Heqv: proper_equivocator_descriptors eqv_descriptors
  es
initial_state_prop
  (equivocators_state_project eqv_descriptors es)
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
Hes: initial_state_prop es
eqv_descriptors: equivocator_descriptors
Heqv: proper_equivocator_descriptors eqv_descriptors
  es
initial_state_prop
  (equivocators_state_project eqv_descriptors es)
  intro eqv.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
Hes: initial_state_prop es
eqv_descriptors: equivocator_descriptors
Heqv: proper_equivocator_descriptors eqv_descriptors
  es
eqv: index
initial_state_prop
  (equivocators_state_project eqv_descriptors es eqv) specialize (Hes eqv).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
Heqv: proper_equivocator_descriptors eqv_descriptors
  es
initial_state_prop
  (equivocators_state_project eqv_descriptors es eqv)
  unfold equivocator_IM in Hes.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
Heqv: proper_equivocator_descriptors eqv_descriptors
  es
initial_state_prop
  (equivocators_state_project eqv_descriptors es eqv)
  unfold equivocators_state_project.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
Heqv: proper_equivocator_descriptors eqv_descriptors
  es
initial_state_prop
  (equivocator_state_descriptor_project (es eqv)
     (eqv_descriptors eqv))
  specialize (Heqv eqv).message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
Heqv: proper_descriptor (IM eqv)
  (eqv_descriptors eqv) 
  (es eqv)
initial_state_prop
  (equivocator_state_descriptor_project (es eqv)
     (eqv_descriptors eqv))
  destruct (eqv_descriptors eqv) as [sn | i]; [done |].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
i: nat
Heqv: proper_descriptor (IM eqv) 
  (Existing i) (es eqv)
initial_state_prop
  (equivocator_state_descriptor_project (es eqv)
     (Existing i))
  destruct Heqv as [es_eqv_i Hes_eqv_i].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
i: nat
es_eqv_i: state (IM eqv)
Hes_eqv_i: equivocator_state_project (es eqv) i =
Some es_eqv_i
initial_state_prop
  (equivocator_state_descriptor_project (es eqv)
     (Existing i))
  simpl.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
i: nat
es_eqv_i: state (IM eqv)
Hes_eqv_i: equivocator_state_project (es eqv) i =
Some es_eqv_i
initial_state_prop
  (default (equivocator_state_zero (es eqv))
     (equivocator_state_project (es eqv) i)) rewrite Hes_eqv_i.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
i: nat
es_eqv_i: state (IM eqv)
Hes_eqv_i: equivocator_state_project (es eqv) i =
Some es_eqv_i
initial_state_prop
  (default (equivocator_state_zero (es eqv))
     (Some es_eqv_i)) simpl.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
es: state equivocators_free_vlsm
eqv: index
Hes: initial_state_prop (es eqv)
eqv_descriptors: equivocator_descriptors
i: nat
es_eqv_i: state (IM eqv)
Hes_eqv_i: equivocator_state_project (es eqv) i =
Some es_eqv_i
initial_state_prop es_eqv_i
  by eapply equivocator_vlsm_initial_state_preservation_rev.
Qed.

Lemma equivocators_initial_message
  (m : message)
  (Hem : initial_message_prop equivocators_free_vlsm m)
  : initial_message_prop Free m.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
m: message
Hem: initial_message_prop m
initial_message_prop m
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
m: message
Hem: initial_message_prop m
initial_message_prop m
  destruct Hem as [eqv [emi Hem]].message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM i)
H1: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
equivocators_free_vlsm:= free_composite_vlsm
  equivocator_IM: VLSM message
m: message
eqv: index
emi: initial_message (equivocator_IM eqv)
Hem: `emi = m
initial_message_prop m
  by exists eqv, emi.
Qed.

End sec_fully_equivocating_composition.

#[export] Hint Rewrite @equivocator_descriptors_update_eq : state_update.
#[export] Hint Rewrite @equivocator_descriptors_update_id using done : state_update.
#[export] Hint Rewrite @equivocator_descriptors_update_neq using done : state_update.
#[export] Hint Rewrite @equivocators_state_project_state_update_eqv using done : state_update.

Section sec_equivocators_sub_projections.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  `{forall i, HasBeenSentCapability (IM i)}
  (equivocating : list index)
  (sub_equivocator_IM := sub_IM (equivocator_IM IM) equivocating)
  (sub_IM_equivocator := equivocator_IM (sub_IM IM equivocating))
  .

Definition seeded_equivocators_no_equivocation_vlsm
  (seed : message -> Prop)
  : VLSM message :=
  composite_no_equivocation_vlsm_with_preloaded
    sub_equivocator_IM (free_constraint sub_equivocator_IM) seed.

Lemma sub_equivocator_IM_initial_state_commute is :
  composite_initial_state_prop sub_equivocator_IM is <->
  composite_initial_state_prop sub_IM_equivocator is.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
equivocating: list index
sub_equivocator_IM:= sub_IM (equivocator_IM IM)
  equivocating: sub_index equivocating
→ VLSM message
sub_IM_equivocator:= equivocator_IM
  (sub_IM IM equivocating): sub_index equivocating
→ VLSM message
is: composite_state sub_equivocator_IM
composite_initial_state_prop sub_equivocator_IM is
↔ composite_initial_state_prop sub_IM_equivocator is
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
equivocating: list index
sub_equivocator_IM:= sub_IM (equivocator_IM IM)
  equivocating: sub_index equivocating
→ VLSM message
sub_IM_equivocator:= equivocator_IM
  (sub_IM IM equivocating): sub_index equivocating
→ VLSM message
is: composite_state sub_equivocator_IM
composite_initial_state_prop sub_equivocator_IM is
↔ composite_initial_state_prop sub_IM_equivocator is done. Qed.

End sec_equivocators_sub_projections.