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.
From Coq Require Import FinFun Reals.
From VLSM.Lib Require Import StdppListSet RealsExtras Measurable FinSetExtras.
From VLSM.Core Require Import VLSM VLSMProjections Composition AnnotatedVLSM.
From VLSM.Core Require Import Equivocation MessageDependencies.
From VLSM.Core Require Import Equivocation.TraceWiseEquivocation.
From VLSM.Core Require Import Equivocation.LimitedMessageEquivocation.
From VLSM.Core Require Import Equivocation.WitnessedEquivocation.
From VLSM.Core Require Import Equivocation.MsgDepLimitedEquivocation.
From VLSM.Core Require Import Equivocation.FixedSetEquivocation.
From VLSM.Core Require Import Equivocators.EquivocatorsComposition.[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 Equivocators.EquivocatorsCompositionProjections.
From VLSM.Core Require Import Equivocators.LimitedStateEquivocation.
From VLSM.Core Require Import
  Equivocators.FixedEquivocationSimulation.
From VLSM.Core Require Import Equivocators.FixedEquivocation.

Core: VLSM Equivocators Simulating Limited Message Equivocation Traces

In this module, we show that the composition of equivocators with no-message equivocation and limited state-equivocation can simulate all traces with the fixed_limited_equivocation_property.

As a corollary we show that any state which is valid for the composition of regular components using a limited_equivocation_constraint can be obtained as the projection of a valid state for the composition of equivocators with no message equivocation and limited state equivocation.

Section sec_fixed_limited_state_equivocation.

Context
  {message index : Type}
  (IM : index -> VLSM message)
  `{forall i, HasBeenSentCapability (IM i)}
  `{forall i, HasBeenReceivedCapability (IM i)}
  (threshold : R)
  `{ReachableThreshold index Ci threshold}
  `{!finite.Finite index}
  (Limited : VLSM message := equivocators_limited_equivocations_vlsm (Ci := Ci) IM threshold)
  (equivocating : Ci)
  (Fixed : VLSM message := equivocators_fixed_equivocations_vlsm IM (elements equivocating))
  .

If the total weight of the equivocators allowed to state-equivocate is less than the threshold, then traces of equivocators which are valid w.r.t the fixed state-equivocation constraint are also valid w.r.t. the limited state-equivocation constraint.

Lemma equivocators_Fixed_incl_Limited
  (Hlimited : (sum_weights (equivocating) <= threshold)%R)
  : VLSM_incl Fixed Limited.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
VLSM_incl Fixed Limited
Proof.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
VLSM_incl Fixed Limited
  apply constraint_subsumption_incl.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
input_valid_constraint_subsumption
  (free_composite_vlsm (equivocator_IM IM))
  (equivocators_fixed_equivocations_constraint IM
     (elements equivocating))
  (equivocators_limited_equivocations_constraint IM
     threshold)
  apply preloaded_constraint_subsumption_stronger.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
preloaded_constraint_subsumption
  (free_composite_vlsm (equivocator_IM IM))
  (equivocators_fixed_equivocations_constraint IM
     (elements equivocating))
  (equivocators_limited_equivocations_constraint IM
     threshold)
  apply strong_constraint_subsumption_strongest.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
strong_constraint_subsumption
  (free_composite_vlsm (equivocator_IM IM))
  (equivocators_fixed_equivocations_constraint IM
     (elements equivocating))
  (equivocators_limited_equivocations_constraint IM
     threshold)
  intros l (s, om) [Hno_equiv Hfixed].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
Hfixed: state_has_fixed_equivocation IM
  (elements equivocating)
  (composite_transition 
     (equivocator_IM IM) l (
     s, om)).1
equivocators_limited_equivocations_constraint IM
  threshold l (s, om)
  split; [done |].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
Hfixed: state_has_fixed_equivocation IM
  (elements equivocating)
  (composite_transition 
     (equivocator_IM IM) l (
     s, om)).1
not_heavy
  (composite_transition (equivocator_IM IM) l (s, om)).1
  unfold not_heavy.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
Hfixed: state_has_fixed_equivocation IM
  (elements equivocating)
  (composite_transition 
     (equivocator_IM IM) l (
     s, om)).1
(equivocation_fault
   (composite_transition (equivocator_IM IM) l (s, om)).1 <=
 threshold)%R
  transitivity (sum_weights (equivocating)); [| done].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
Hfixed: state_has_fixed_equivocation IM
  (elements equivocating)
  (composite_transition 
     (equivocator_IM IM) l (
     s, om)).1
(equivocation_fault
   (composite_transition (equivocator_IM IM) l (s, om)).1 <=
 sum_weights equivocating)%R
  remember (composite_transition _ _ _).1.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Heqc: c =
(composite_transition (equivocator_IM IM) l
   (s, om)).1
Hfixed: state_has_fixed_equivocation IM
  (elements equivocating) c
(equivocation_fault c <= sum_weights equivocating)%R clear Heqc.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Hfixed: state_has_fixed_equivocation IM
  (elements equivocating) c
(equivocation_fault c <= sum_weights equivocating)%R
  unfold state_has_fixed_equivocation in Hfixed.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Hfixed: equivocating_indices IM (finite.enum index) c
⊆ elements equivocating
(equivocation_fault c <= sum_weights equivocating)%R
  unfold equivocation_fault.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Hfixed: equivocating_indices IM (finite.enum index) c
⊆ elements equivocating
(sum_weights (equivocating_validators c) <=
 sum_weights equivocating)%R
  apply sum_weights_subseteq.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Hfixed: equivocating_indices IM (finite.enum index) c
⊆ elements equivocating
equivocating_validators c ⊆ equivocating
  intros i Hi.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Hfixed: equivocating_indices IM (finite.enum index) c
⊆ elements equivocating
i: index
Hi: i ∈ equivocating_validators c
i ∈ equivocating
  apply elem_of_elements, Hfixed.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Hfixed: equivocating_indices IM (finite.enum index) c
⊆ elements equivocating
i: index
Hi: i ∈ equivocating_validators c
i ∈ equivocating_indices IM (finite.enum index) c
  rewrite <- @elem_of_list_to_set with (C := Ci) by typeclasses eauto.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Limited:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
equivocating: Ci
Fixed:= equivocators_fixed_equivocations_vlsm IM
  (elements equivocating): VLSM message
Hlimited: (sum_weights equivocating <= threshold)%R
l: label (free_composite_vlsm (equivocator_IM IM))
s: state (free_composite_vlsm (equivocator_IM IM))
om: option message
Hno_equiv: equivocators_no_equivocations_constraint
  IM l (s, om)
c: composite_state (equivocator_IM IM)
Hfixed: equivocating_indices IM (finite.enum index) c
⊆ elements equivocating
i: index
Hi: i ∈ equivocating_validators c
i
∈ list_to_set
    (equivocating_indices IM (finite.enum index) c)
  by eapply equivocating_indices_equivocating_validators.
Qed.

End sec_fixed_limited_state_equivocation.

Section sec_limited_equivocation_simulation.

Context
  {message index : Type}
  (IM : index -> VLSM message)
  `{forall i, HasBeenSentCapability (IM i)}
  `{forall i, HasBeenReceivedCapability (IM i)}
  (threshold : R)
  `{ReachableThreshold index Ci threshold}
  `{!finite.Finite index}
  (XE : VLSM message := equivocators_limited_equivocations_vlsm (Ci := Ci) IM threshold)
  .

If a trace has the fixed_limited_equivocation_property, then it can be simulated by the composition of equivocators with no message-equivocation and limited state-equivocation.

Lemma limited_equivocators_finite_valid_trace_init_to_rev
  (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM)
  isX trX
  (HtrX : fixed_limited_equivocation_prop (Ci := Ci) (Cv := Ci) IM threshold Datatypes.id isX trX)
  : exists is s tr,
      equivocators_total_state_project IM is = isX /\
      equivocators_total_state_project IM s = finite_trace_last isX trX /\
      equivocators_total_trace_project IM tr = trX /\
      finite_valid_trace_init_to XE is s tr /\
      finite_trace_last_output trX = finite_trace_last_output tr.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
HtrX: fixed_limited_equivocation_prop IM threshold
  Datatypes.id isX trX
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is = isX
  ∧ equivocators_total_state_project IM s =
    finite_trace_last isX trX
    ∧ equivocators_total_trace_project IM tr = trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
Proof.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
HtrX: fixed_limited_equivocation_prop IM threshold
  Datatypes.id isX trX
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is = isX
  ∧ equivocators_total_state_project IM s =
    finite_trace_last isX trX
    ∧ equivocators_total_trace_project IM tr = trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  destruct HtrX as (equivocating & Hlimited & HtrX).message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
equivocating: Ci
Hlimited: (sum_weights equivocating <= threshold)%R
HtrX: finite_valid_trace
  (fixed_equivocation_vlsm_composition IM
     (fin_sets.set_map Datatypes.id
        equivocating)) isX trX
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is = isX
  ∧ equivocators_total_state_project IM s =
    finite_trace_last isX trX
    ∧ equivocators_total_trace_project IM tr = trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  eapply VLSM_incl_finite_valid_trace, valid_trace_add_default_last in HtrX
  ; [| by eapply Fixed_eq_StrongFixed].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
equivocating: Ci
Hlimited: (sum_weights equivocating <= threshold)%R
HtrX: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      {|
        vlsm_type :=
          fixed_equivocation_vlsm_composition
            IM
            (fin_sets.set_map Datatypes.id
               equivocating);
        vlsm_machine :=
          strong_fixed_equivocation_vlsm_composition
            IM
            (fin_sets.set_map Datatypes.id
               equivocating)
      |}
  |} isX (finite_trace_last isX trX) trX
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is = isX
  ∧ equivocators_total_state_project IM s =
    finite_trace_last isX trX
    ∧ equivocators_total_trace_project IM tr = trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  eapply fixed_equivocators_finite_valid_trace_init_to_rev in HtrX
    as (is & s & tr & His & Hs & Htr & Hptr & Houtput); [| done].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
equivocating: Ci
Hlimited: (sum_weights equivocating <= threshold)%R
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His: equivocators_total_state_project IM is = isX
Hs: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: equivocators_total_trace_project IM tr = trX
Hptr: finite_valid_trace_init_to
  (equivocators_fixed_equivocations_vlsm IM
     (elements
        (fin_sets.set_map Datatypes.id
           equivocating))) is s tr
Houtput: finite_trace_last_output trX =
finite_trace_last_output tr
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is = isX
  ∧ equivocators_total_state_project IM s =
    finite_trace_last isX trX
    ∧ equivocators_total_trace_project IM tr = trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  exists is, s, tr; split_and?; try itauto.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
equivocating: Ci
Hlimited: (sum_weights equivocating <= threshold)%R
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His: equivocators_total_state_project IM is = isX
Hs: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: equivocators_total_trace_project IM tr = trX
Hptr: finite_valid_trace_init_to
  (equivocators_fixed_equivocations_vlsm IM
     (elements
        (fin_sets.set_map Datatypes.id
           equivocating))) is s tr
Houtput: finite_trace_last_output trX =
finite_trace_last_output tr
finite_valid_trace_init_to XE is s tr
  revert Hptr; apply VLSM_incl_finite_valid_trace_init_to.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
equivocating: Ci
Hlimited: (sum_weights equivocating <= threshold)%R
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His: equivocators_total_state_project IM is = isX
Hs: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: equivocators_total_trace_project IM tr = trX
Houtput: finite_trace_last_output trX =
finite_trace_last_output tr
VLSM_incl_part
  (constrained_vlsm_machine
     (free_composite_vlsm (equivocator_IM IM))
     (equivocators_fixed_equivocations_constraint IM
        (elements
           (fin_sets.set_map Datatypes.id equivocating))))
  (constrained_vlsm_machine
     (free_composite_vlsm (equivocator_IM IM))
     (equivocators_limited_equivocations_constraint IM
        threshold))
  eapply VLSM_incl_trans; [| by apply equivocators_Fixed_incl_Limited].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
equivocating: Ci
Hlimited: (sum_weights equivocating <= threshold)%R
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His: equivocators_total_state_project IM is = isX
Hs: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: equivocators_total_trace_project IM tr = trX
Houtput: finite_trace_last_output trX =
finite_trace_last_output tr
VLSM_incl
  {|
    vlsm_type :=
      free_composite_vlsm (equivocator_IM IM);
    vlsm_machine :=
      {|
        initial_state_prop := initial_state_prop;
        s0 :=
          s0 (free_composite_vlsm (equivocator_IM IM))
            (free_composite_vlsm (equivocator_IM IM));
        initial_message_prop := initial_message_prop;
        transition := transition;
        valid :=
          λ (l : label
                   (free_composite_vlsm
                      (equivocator_IM IM))) (som : 
                                             state
                                               (free_composite_vlsm
                                                 (equivocator_IM
                                                 IM)) *
                                             option
                                               message),
            valid l som
            ∧ equivocators_fixed_equivocations_constraint
                IM
                (elements
                   (fin_sets.set_map Datatypes.id
                      equivocating)) l som
      |}
  |}
  {|
    vlsm_type :=
      free_composite_vlsm (equivocator_IM IM);
    vlsm_machine :=
      constrained_vlsm_machine
        (free_composite_vlsm (equivocator_IM IM))
        (equivocators_fixed_equivocations_constraint
           IM (elements equivocating))
  |}
  apply equivocators_fixed_equivocations_vlsm_subset_incl.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
isX: composite_state IM
trX: list (composite_transition_item IM)
equivocating: Ci
Hlimited: (sum_weights equivocating <= threshold)%R
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His: equivocators_total_state_project IM is = isX
Hs: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: equivocators_total_trace_project IM tr = trX
Houtput: finite_trace_last_output trX =
finite_trace_last_output tr
elements (fin_sets.set_map Datatypes.id equivocating)
⊆ elements equivocating
  by set_solver.
Qed.

Section sec_equivocators_simulating_annotated_limited.

Context
  `{FinSet message Cm}
  (message_dependencies : message -> Cm)
  (full_message_dependencies : message -> Cm)
  `{!FullMessageDependencies message_dependencies full_message_dependencies}
  `{forall i, MessageDependencies (IM i) message_dependencies}
  (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM)
  (sender : message -> option index)
  (Hchannel : channel_authentication_prop IM Datatypes.id sender)
  .

Lemma equivocators_limited_valid_trace_projects_to_annotated_limited_equivocation_rev
  isX sX trX
  (HtrX : finite_valid_trace_init_to (msg_dep_limited_equivocation_vlsm (Cv := Ci) IM threshold
            full_message_dependencies sender) isX sX trX)
  : exists is s tr,
      equivocators_total_state_project IM is = original_state isX /\
      equivocators_total_state_project IM s = original_state sX /\
      equivocators_total_trace_project IM tr =
        pre_VLSM_embedding_finite_trace_project
          (annotated_type (free_composite_vlsm IM) Ci) (composite_type IM)
            Datatypes.id original_state trX /\
      finite_valid_trace_init_to XE is s tr /\
      finite_trace_last_output trX = finite_trace_last_output tr.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX, sX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
HtrX: finite_valid_trace_init_to
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
  isX sX trX
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is =
  original_state isX
  ∧ equivocators_total_state_project IM s =
    original_state sX
    ∧ equivocators_total_trace_project IM tr =
      pre_VLSM_embedding_finite_trace_project
        (annotated_type (free_composite_vlsm IM) Ci)
        (composite_type IM) Datatypes.id
        original_state trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
Proof.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX, sX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
HtrX: finite_valid_trace_init_to
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
  isX sX trX
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is =
  original_state isX
  ∧ equivocators_total_state_project IM s =
    original_state sX
    ∧ equivocators_total_trace_project IM tr =
      pre_VLSM_embedding_finite_trace_project
        (annotated_type (free_composite_vlsm IM) Ci)
        (composite_type IM) Datatypes.id
        original_state trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  apply valid_trace_get_last in HtrX as HeqsX.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX, sX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
HtrX: finite_valid_trace_init_to
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
  isX sX trX
HeqsX: finite_trace_last isX trX = sX
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is =
  original_state isX
  ∧ equivocators_total_state_project IM s =
    original_state sX
    ∧ equivocators_total_trace_project IM tr =
      pre_VLSM_embedding_finite_trace_project
        (annotated_type (free_composite_vlsm IM) Ci)
        (composite_type IM) Datatypes.id
        original_state trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  eapply valid_trace_forget_last, @msg_dep_fixed_limited_equivocation in HtrX; [| done..].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX, sX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
HeqsX: finite_trace_last isX trX = sX
HtrX: fixed_limited_equivocation_prop IM threshold
  Datatypes.id (original_state isX)
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX)
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is =
  original_state isX
  ∧ equivocators_total_state_project IM s =
    original_state sX
    ∧ equivocators_total_trace_project IM tr =
      pre_VLSM_embedding_finite_trace_project
        (annotated_type (free_composite_vlsm IM) Ci)
        (composite_type IM) Datatypes.id
        original_state trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  apply limited_equivocators_finite_valid_trace_init_to_rev in HtrX
     as (is & s & tr & His_pr & Hpr_s & Htr_pr & Htr & Houtput); [| done].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX, sX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
HeqsX: finite_trace_last isX trX = sX
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His_pr: equivocators_total_state_project IM is =
original_state isX
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last (original_state isX)
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX)
Htr_pr: equivocators_total_trace_project IM tr =
pre_VLSM_embedding_finite_trace_project
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies
     sender) (composite_type IM) Datatypes.id
  original_state trX
Htr: finite_valid_trace_init_to XE is s tr
Houtput: finite_trace_last_output
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX) =
finite_trace_last_output tr
∃ (is
   s : state (free_composite_vlsm (equivocator_IM IM))) 
  (tr : list
          (composite_transition_item
             (equivocator_IM IM))),
  equivocators_total_state_project IM is =
  original_state isX
  ∧ equivocators_total_state_project IM s =
    original_state sX
    ∧ equivocators_total_trace_project IM tr =
      pre_VLSM_embedding_finite_trace_project
        (annotated_type (free_composite_vlsm IM) Ci)
        (composite_type IM) Datatypes.id
        original_state trX
      ∧ finite_valid_trace_init_to XE is s tr
        ∧ finite_trace_last_output trX =
          finite_trace_last_output tr
  exists is, s, tr; subst; split_and!; [done | | done | done |].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His_pr: equivocators_total_state_project IM is =
original_state isX
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last (original_state isX)
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX)
Htr_pr: equivocators_total_trace_project IM tr =
pre_VLSM_embedding_finite_trace_project
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies
     sender) (composite_type IM) Datatypes.id
  original_state trX
Htr: finite_valid_trace_init_to XE is s tr
Houtput: finite_trace_last_output
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX) =
finite_trace_last_output tr
equivocators_total_state_project IM s =
original_state (finite_trace_last isX trX)
message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His_pr: equivocators_total_state_project IM is =
original_state isX
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last (original_state isX)
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX)
Htr_pr: equivocators_total_trace_project IM tr =
pre_VLSM_embedding_finite_trace_project
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies
     sender) (composite_type IM) Datatypes.id
  original_state trX
Htr: finite_valid_trace_init_to XE is s tr
Houtput: finite_trace_last_output
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX) =
finite_trace_last_output tr
finite_trace_last_output trX =
finite_trace_last_output tr
  -message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His_pr: equivocators_total_state_project IM is =
original_state isX
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last (original_state isX)
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX)
Htr_pr: equivocators_total_trace_project IM tr =
pre_VLSM_embedding_finite_trace_project
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies
     sender) (composite_type IM) Datatypes.id
  original_state trX
Htr: finite_valid_trace_init_to XE is s tr
Houtput: finite_trace_last_output
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX) =
finite_trace_last_output tr
equivocators_total_state_project IM s =
original_state (finite_trace_last isX trX) by erewrite Hpr_s, <- pre_VLSM_embedding_finite_trace_last.
  -message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H19: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
sender: message → option index
Hchannel: channel_authentication_prop IM Datatypes.id
  sender
isX: state
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies sender)
trX: list transition_item
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
His_pr: equivocators_total_state_project IM is =
original_state isX
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last (original_state isX)
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX)
Htr_pr: equivocators_total_trace_project IM tr =
pre_VLSM_embedding_finite_trace_project
  (msg_dep_limited_equivocation_vlsm IM
     threshold full_message_dependencies
     sender) (composite_type IM) Datatypes.id
  original_state trX
Htr: finite_valid_trace_init_to XE is s tr
Houtput: finite_trace_last_output
  (pre_VLSM_embedding_finite_trace_project
     (msg_dep_limited_equivocation_vlsm IM
        threshold full_message_dependencies
        sender) (composite_type IM)
     Datatypes.id original_state trX) =
finite_trace_last_output tr
finite_trace_last_output trX =
finite_trace_last_output tr by rewrite <- Houtput; apply pre_VLSM_embedding_finite_trace_last_output.
Qed.

End sec_equivocators_simulating_annotated_limited.

Context
  `{FinSet message Cm}
  (sender : message -> option index)
  `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM (fun i => i) sender)}
  (Limited : VLSM message := tracewise_limited_equivocation_vlsm_composition IM (Cv := Ci) threshold Datatypes.id sender)
  (message_dependencies : message -> Cm)
  .

Any valid state for the composition of regular components under a limited message-equivocation constraint is the projection of a valid state of the composition of equivocators under a no message-equivocation and limited state-equivocation constraint.

Lemma limited_equivocators_valid_state_rev
  (Hwitnessed_equivocation : WitnessedEquivocationCapability IM threshold Datatypes.id sender (Cv := Ci))
  `{!Irreflexive (msg_dep_happens_before message_dependencies)}
  `{forall i, MessageDependencies (IM i) message_dependencies}
  (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies)
  (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM)
  (can_emit_signed : channel_authentication_prop IM Datatypes.id sender)
  : forall sX, valid_state_prop Limited sX ->
    exists s, equivocators_total_state_project IM s = sX /\
    valid_state_prop XE s.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
∀ sX : state Limited,
  valid_state_prop Limited sX
  → ∃ s : state
            (free_composite_vlsm (equivocator_IM IM)),
      equivocators_total_state_project IM s = sX
      ∧ valid_state_prop XE s
Proof.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
∀ sX : state Limited,
  valid_state_prop Limited sX
  → ∃ s : state
            (free_composite_vlsm (equivocator_IM IM)),
      equivocators_total_state_project IM s = sX
      ∧ valid_state_prop XE s
  intros sX HsX.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
sX: state Limited
HsX: valid_state_prop Limited sX
∃ s : state (free_composite_vlsm (equivocator_IM IM)),
  equivocators_total_state_project IM s = sX
  ∧ valid_state_prop XE s
  apply
    (limited_valid_state_has_trace_exhibiting_limited_equivocation (Ci := Ci) IM threshold
      Datatypes.id sender message_dependencies Hwitnessed_equivocation Hfull
      no_initial_messages_in_IM can_emit_signed)
    in HsX as (isX & trX & HsX & HtrX).message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
sX: state Limited
isX: state
  (tracewise_limited_equivocation_vlsm_composition
     IM threshold Datatypes.id sender)
trX: list transition_item
HsX: finite_trace_last isX trX = sX
HtrX: fixed_limited_equivocation_prop IM threshold
  Datatypes.id isX trX
∃ s : state (free_composite_vlsm (equivocator_IM IM)),
  equivocators_total_state_project IM s = sX
  ∧ valid_state_prop XE s
  apply limited_equivocators_finite_valid_trace_init_to_rev in HtrX
    as (is & s & tr & _ & Hpr_s & _ & Htr & _)
  ; [| done].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
sX: state Limited
isX: state
  (tracewise_limited_equivocation_vlsm_composition
     IM threshold Datatypes.id sender)
trX: list transition_item
HsX: finite_trace_last isX trX = sX
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: finite_valid_trace_init_to XE is s tr
∃ s : state (free_composite_vlsm (equivocator_IM IM)),
  equivocators_total_state_project IM s = sX
  ∧ valid_state_prop XE s
  exists s.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
sX: state Limited
isX: state
  (tracewise_limited_equivocation_vlsm_composition
     IM threshold Datatypes.id sender)
trX: list transition_item
HsX: finite_trace_last isX trX = sX
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: finite_valid_trace_init_to XE is s tr
equivocators_total_state_project IM s = sX
∧ valid_state_prop XE s
  subst.message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
isX: state
  (tracewise_limited_equivocation_vlsm_composition
     IM threshold Datatypes.id sender)
trX: list transition_item
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: finite_valid_trace_init_to XE is s tr
equivocators_total_state_project IM s =
finite_trace_last isX trX ∧ valid_state_prop XE s split; [done |].message, index: Type
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
XE:= equivocators_limited_equivocations_vlsm IM
  threshold: VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
sender: message → option index
H19: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     (λ i : index, i) sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold Datatypes.id sender: VLSM message
message_dependencies: message → Cm
Hwitnessed_equivocation: WitnessedEquivocationCapability
  IM threshold Datatypes.id
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H20: ∀ i : index,
  MessageDependencies (IM i)
    message_dependencies
Hfull: ∀ i : index,
  message_dependencies_full_node_condition_prop
    (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop
  IM
can_emit_signed: channel_authentication_prop IM
  Datatypes.id sender
isX: state
  (tracewise_limited_equivocation_vlsm_composition
     IM threshold Datatypes.id sender)
trX: list transition_item
is, s: state (free_composite_vlsm (equivocator_IM IM))
tr: list
  (composite_transition_item (equivocator_IM IM))
Hpr_s: equivocators_total_state_project IM s =
finite_trace_last isX trX
Htr: finite_valid_trace_init_to XE is s tr
valid_state_prop XE s
  by apply valid_trace_last_pstate in Htr.
Qed.

End sec_limited_equivocation_simulation.