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 RIneq.
From VLSM.Lib Require Import Preamble FinSetExtras.
From VLSM.Lib Require Import RealsExtras Measurable.
From VLSM.Core Require Import VLSM VLSMProjections MessageDependencies Composition Equivocation.
From VLSM.Core Require Import Equivocation.FixedSetEquivocation.
From VLSM.Core Require Import Equivocation.TraceWiseEquivocation.
From VLSM.Core Require Import Equivocation.WitnessedEquivocation.

Core: VLSM Limited Message Equivocation

In this module, we define the notion of limited (message-based) equivocation.

This notion is slightly harder to define than that of fixed-set equivocation, because, while for the latter we fix a set and let only the components belonging to that set to equivocate, in the case of limited equivocation, the set of components equivocating can change dynamically, each component being virtually allowed to equivocate as long as the weight of all components currently equivocating does not pass a certain threshold.

As we need to be able to measure the amount of equivocation in a given state to design a composition constraint preventing equivocation weight from passing the threshold, we need an appropriate measure of equivocation. We here choose is_equivocating_tracewise as this measure.

Moreover, to further limit the amount of equivocation allowed when producing a message, we assume a full-node-like condition to be satisfied by all components. This guarantees that whenever a message not-previously send is received in a state, the amount of equivocation would only grow with the weight of the sender of the message (if that wasn't already known as an equivocator).

Section sec_limited_message_equivocation.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (threshold : R)
  `{ReachableThreshold validator Cv threshold}
  (equivocating : composite_state IM -> validator -> Prop)
  (Hno_initial_equivocation :
    forall s, composite_initial_state_prop IM s ->
    forall v, ~ equivocating s v)
  .

Inductive LimitedEquivocationProp (s : composite_state IM) : Prop :=
| limited_equivocation :
    forall (vs : Cv)
      (Heqv_vs : forall v, equivocating s v -> v ∈ vs)
      (Hlimited : (sum_weights vs <= threshold)%R),
      LimitedEquivocationProp s.

Definition limited_equivocation_constraint
  (l : composite_label IM)
  (som : composite_state IM * option message)
  : Prop :=
  LimitedEquivocationProp (composite_transition IM l som).1.

Definition limited_equivocation_composite_vlsm : VLSM message :=
  composite_vlsm IM limited_equivocation_constraint.

Lemma limited_equivocation_valid_state s
  : valid_state_prop limited_equivocation_composite_vlsm s ->
    LimitedEquivocationProp s.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
s: state limited_equivocation_composite_vlsm
valid_state_prop limited_equivocation_composite_vlsm s
→ LimitedEquivocationProp s
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
s: state limited_equivocation_composite_vlsm
valid_state_prop limited_equivocation_composite_vlsm s
→ LimitedEquivocationProp s
  intros Hs; apply valid_state_prop_iff in Hs
    as [[[is His] ->] | (l & [s' om'] & om & [(_ & _ & _ & Hv) Ht])]; simpl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
is: state limited_equivocation_composite_vlsm
His: initial_state_prop is
LimitedEquivocationProp is
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
s: state limited_equivocation_composite_vlsm
l: label limited_equivocation_composite_vlsm
s': state limited_equivocation_composite_vlsm
om', om: option message
Hv: limited_equivocation_constraint l (s', om')
Ht: transition l (s', om') = (s, om)
LimitedEquivocationProp s
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
is: state limited_equivocation_composite_vlsm
His: initial_state_prop is
LimitedEquivocationProp is exists ∅.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
is: state limited_equivocation_composite_vlsm
His: initial_state_prop is
∀ v : validator, equivocating is v → v ∈ ∅
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
is: state limited_equivocation_composite_vlsm
His: initial_state_prop is
(sum_weights ∅ <= threshold)%R
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
is: state limited_equivocation_composite_vlsm
His: initial_state_prop is
∀ v : validator, equivocating is v → v ∈ ∅ by intros v Hv; contradict Hv; apply Hno_initial_equivocation.
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
is: state limited_equivocation_composite_vlsm
His: initial_state_prop is
(sum_weights ∅ <= threshold)%R rewrite sum_weights_empty; [| done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
is: state limited_equivocation_composite_vlsm
His: initial_state_prop is
(0 <= threshold)%R
      by apply (rt_positive (H6 := H6)).
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
threshold: R
validator, Cv: Type
Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision1: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
equivocating: composite_state IM → validator → Prop
Hno_initial_equivocation: ∀ s : composite_state IM,
  composite_initial_state_prop
    IM s
  → ∀ v : validator,
      ¬ equivocating s v
s: state limited_equivocation_composite_vlsm
l: label limited_equivocation_composite_vlsm
s': state limited_equivocation_composite_vlsm
om', om: option message
Hv: limited_equivocation_constraint l (s', om')
Ht: transition l (s', om') = (s, om)
LimitedEquivocationProp s by cbv in Hv, Ht; rewrite Ht in Hv.
Qed.

End sec_limited_message_equivocation.

Section sec_basic_limited_message_equivocation.

Context
  {message : Type}
  `{EqDecision index}
  `{EqDecision validator}
  (IM : index -> VLSM message)
  `{BasicEquivocation (composite_state IM) validator}
  .

Definition basic_limited_equivocation_constraint :=
  limited_equivocation_constraint IM threshold is_equivocating (Cv := Cv).

Definition basic_limited_equivocation_composite_vlsm : VLSM message :=
  limited_equivocation_composite_vlsm IM threshold is_equivocating (Cv := Cv).

Lemma LimitedEquivocationProp_impl_not_heavy :
  forall s, LimitedEquivocationProp (Cv := Cv) IM threshold is_equivocating s -> not_heavy s.message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
∀ s : composite_state IM,
  LimitedEquivocationProp IM threshold is_equivocating
    s → not_heavy s
Proof.message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
∀ s : composite_state IM,
  LimitedEquivocationProp IM threshold is_equivocating
    s → not_heavy s
  intros s [].message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
vs: Cv
Heqv_vs: ∀ v : validator,
  is_equivocating s v → v ∈ vs
Hlimited: (sum_weights vs <= threshold)%R
not_heavy s
  apply Rle_trans with (sum_weights vs); [| done].message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
vs: Cv
Heqv_vs: ∀ v : validator,
  is_equivocating s v → v ∈ vs
Hlimited: (sum_weights vs <= threshold)%R
(equivocation_fault s <= sum_weights vs)%R
  apply sum_weights_subseteq; intros v Hv.message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
vs: Cv
Heqv_vs: ∀ v : validator,
  is_equivocating s v → v ∈ vs
Hlimited: (sum_weights vs <= threshold)%R
v: validator
Hv: v ∈ equivocating_validators s
v ∈ vs
  apply elem_of_filter in Hv as [Hvsl Hvsr].message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
vs: Cv
Heqv_vs: ∀ v : validator,
  is_equivocating s v → v ∈ vs
Hlimited: (sum_weights vs <= threshold)%R
v: validator
Hvsl: is_equivocating s v
Hvsr: v ∈ state_validators s
v ∈ vs
  by apply Heqv_vs, Hvsl.
Qed.

Definition basic_equivocation_state_validators_comprehensive_prop : Prop :=
  forall s v, is_equivocating s v -> v ∈ state_validators s.

Lemma not_heavy_impl_LimitedEquivocationProp
  (Hcomprehensive : basic_equivocation_state_validators_comprehensive_prop)
  : forall s, not_heavy s -> LimitedEquivocationProp (Cv := Cv) IM threshold is_equivocating s.message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
Hcomprehensive: basic_equivocation_state_validators_comprehensive_prop
∀ s : composite_state IM,
  not_heavy s
  → LimitedEquivocationProp IM threshold
      is_equivocating s
Proof.message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
Hcomprehensive: basic_equivocation_state_validators_comprehensive_prop
∀ s : composite_state IM,
  not_heavy s
  → LimitedEquivocationProp IM threshold
      is_equivocating s
  intros s Hs.message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
Hcomprehensive: basic_equivocation_state_validators_comprehensive_prop
s: composite_state IM
Hs: not_heavy s
LimitedEquivocationProp IM threshold is_equivocating s
  exists (equivocating_validators s); [| done].message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
Hcomprehensive: basic_equivocation_state_validators_comprehensive_prop
s: composite_state IM
Hs: not_heavy s
∀ v : validator,
  is_equivocating s v → v ∈ equivocating_validators s
  intros v Hv; apply elem_of_filter.message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
Hcomprehensive: basic_equivocation_state_validators_comprehensive_prop
s: composite_state IM
Hs: not_heavy s
v: validator
Hv: is_equivocating s v
is_equivocating s v ∧ v ∈ state_validators s
  split; [done |].message, index: Type
EqDecision0: EqDecision index
validator: Type
EqDecision1: EqDecision validator
IM: index → VLSM message
Cv: Type
threshold: R
measurable_V, Hm: Measurable validator
H: ElemOf validator Cv
H0: Empty Cv
H1: Singleton validator Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements validator Cv
EqDecision2: EqDecision validator
H6: FinSet validator Cv
H7: ReachableThreshold validator Cv threshold
H8: BasicEquivocation (composite_state IM) validator
  Cv threshold
Hcomprehensive: basic_equivocation_state_validators_comprehensive_prop
s: composite_state IM
Hs: not_heavy s
v: validator
Hv: is_equivocating s v
v ∈ state_validators s
  by apply Hcomprehensive.
Qed.

End sec_basic_limited_message_equivocation.

Section sec_tracewise_limited_message_equivocation.

Context
  {message index : Type}
  (IM : index -> VLSM message)
  (threshold : R)
  `{EqDecision index}
  `{forall i, HasBeenSentCapability (IM i)}
  `{forall i, HasBeenReceivedCapability (IM i)}
  (Free := free_composite_vlsm IM)
  `{finite.Finite validator}
  `{ReachableThreshold validator Cv threshold}
  (A : validator -> index)
  (sender : message -> option validator)
  `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)}
  (HBE : BasicEquivocation (composite_state IM) validator Cv threshold
    := equivocation_dec_tracewise IM threshold A sender)
  .

Existing Instance HBE.

Lemma tracewise_basic_equivocation_state_validators_comprehensive_prop :
  basic_equivocation_state_validators_comprehensive_prop IM.message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
basic_equivocation_state_validators_comprehensive_prop
  IM
Proof.message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
basic_equivocation_state_validators_comprehensive_prop
  IM by intros s v _; cbn; apply elem_of_list_to_set, elem_of_enum. Qed.

Definition tracewise_limited_equivocation_constraint :=
  basic_limited_equivocation_constraint IM.

Definition tracewise_limited_equivocation_vlsm_composition : VLSM message :=
  basic_limited_equivocation_composite_vlsm IM.

Lemma full_node_limited_equivocation_valid_state_weight s
  : valid_state_prop tracewise_limited_equivocation_vlsm_composition s ->
    LimitedEquivocationProp (Cv := Cv) IM threshold is_equivocating s.message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state
  tracewise_limited_equivocation_vlsm_composition
valid_state_prop
  tracewise_limited_equivocation_vlsm_composition s
→ LimitedEquivocationProp IM threshold is_equivocating
    s
Proof.message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state
  tracewise_limited_equivocation_vlsm_composition
valid_state_prop
  tracewise_limited_equivocation_vlsm_composition s
→ LimitedEquivocationProp IM threshold is_equivocating
    s
  eapply limited_equivocation_valid_state; [done |].message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state
  tracewise_limited_equivocation_vlsm_composition
∀ s : composite_state IM,
  composite_initial_state_prop IM s
  → ∀ v : validator, ¬ is_equivocating s v
  by intros; apply initial_state_not_is_equivocating_tracewise.
Qed.

Lemma tracewise_not_heavy_LimitedEquivocationProp_iff :
  forall s, not_heavy s <-> LimitedEquivocationProp (Cv := Cv) IM threshold is_equivocating s.message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
∀ s : composite_state IM,
  not_heavy s
  ↔ LimitedEquivocationProp IM threshold
      is_equivocating s
Proof.message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
∀ s : composite_state IM,
  not_heavy s
  ↔ LimitedEquivocationProp IM threshold
      is_equivocating s
  intros; split.message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
not_heavy s
→ LimitedEquivocationProp IM threshold is_equivocating
    s
message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
LimitedEquivocationProp IM threshold is_equivocating s
→ not_heavy s
  -message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
not_heavy s
→ LimitedEquivocationProp IM threshold is_equivocating
    s by apply not_heavy_impl_LimitedEquivocationProp,
      tracewise_basic_equivocation_state_validators_comprehensive_prop.
  -message, index: Type
IM: index → VLSM message
threshold: R
EqDecision0: EqDecision index
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H1: finite.Finite validator
Cv: Type
Hm: Measurable validator
H2: ElemOf validator Cv
H3: Empty Cv
H4: Singleton validator Cv
H5: Union Cv
H6: Intersection Cv
H7: Difference Cv
H8: Elements validator Cv
EqDecision2: EqDecision validator
H9: FinSet validator Cv
H10: ReachableThreshold validator Cv threshold
A: validator → index
sender: message → option validator
H11: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: composite_state IM
LimitedEquivocationProp IM threshold is_equivocating s
→ not_heavy s by apply LimitedEquivocationProp_impl_not_heavy.
Qed.

End sec_tracewise_limited_message_equivocation.

Section sec_fixed_limited_message_equivocation.

Fixed Message Equivocation implies Limited Message Equivocation

In this section we show that if the set of allowed equivocators for a fixed equivocation constraint is of weight smaller than the threshold accepted for limited message equivocation, then any valid trace for the fixed equivocation constraint is also a trace under the limited equivocation constraint.

Context
  {message index : Type}
  (IM : index -> VLSM message)
  (threshold : R)
  `{FinSet index Ci}
  `{!finite.Finite index}
  `{forall i, HasBeenSentCapability (IM i)}
  `{forall i, HasBeenReceivedCapability (IM i)}
  (Free := free_composite_vlsm IM)
  `{finite.Finite validator}
  `{ReachableThreshold validator Cv threshold}
  (A : validator -> index)
  `{! Inj (=) (=) A}
  (sender : message -> option validator)
  (eqv_validators : Cv)
  (equivocators := fin_sets.set_map A eqv_validators : Ci)
  (Hlimited : (sum_weights eqv_validators <= threshold)%R )
  (Hsender_safety : sender_safety_alt_prop IM A sender)
  `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)}
  (Fixed := fixed_equivocation_vlsm_composition IM equivocators)
  (StrongFixed := strong_fixed_equivocation_vlsm_composition IM equivocators)
  (Limited : VLSM message := tracewise_limited_equivocation_vlsm_composition (Cv := Cv) IM threshold A sender)
  (HBE : BasicEquivocation (composite_state IM) validator Cv threshold :=
    equivocation_dec_tracewise IM threshold A sender)
  .

Lemma StrongFixed_valid_state_not_heavy s
  (Hs : valid_state_prop StrongFixed s)
  : not_heavy (1 := HBE) s.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state StrongFixed
Hs: valid_state_prop StrongFixed s
not_heavy s
Proof.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state StrongFixed
Hs: valid_state_prop StrongFixed s
not_heavy s
  cut (equivocating_validators (1 := HBE) s ⊆ eqv_validators).message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state StrongFixed
Hs: valid_state_prop StrongFixed s
equivocating_validators s ⊆ eqv_validators
→ not_heavy s
message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state StrongFixed
Hs: valid_state_prop StrongFixed s
equivocating_validators s ⊆ eqv_validators
  {message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state StrongFixed
Hs: valid_state_prop StrongFixed s
equivocating_validators s ⊆ eqv_validators
→ not_heavy s
    intro Hincl; unfold not_heavy.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state StrongFixed
Hs: valid_state_prop StrongFixed s
Hincl: equivocating_validators s ⊆ eqv_validators
(equivocation_fault s <= threshold)%R
    by etransitivity; [apply sum_weights_subseteq |].
  }message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s: state StrongFixed
Hs: valid_state_prop StrongFixed s
equivocating_validators s ⊆ eqv_validators
  apply valid_state_has_trace in Hs as [is [tr Htr]].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr: list transition_item
Htr: finite_valid_trace_init_to StrongFixed is s tr
equivocating_validators s ⊆ eqv_validators
  eapply VLSM_incl_finite_valid_trace_init_to in Htr as Hpre_tr;
    [| by apply constrained_preloaded_incl].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr: list transition_item
Htr: finite_valid_trace_init_to StrongFixed is s tr
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
equivocating_validators s ⊆ eqv_validators
  intros v Hv.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr: list transition_item
Htr: finite_valid_trace_init_to StrongFixed is s tr
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
v ∈ eqv_validators
  apply equivocating_validators_is_equivocating_tracewise_iff in Hv as Hvs'.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr: list transition_item
Htr: finite_valid_trace_init_to StrongFixed is s tr
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
Hvs': is_equivocating_tracewise_no_has_been_sent IM A
  sender s v
v ∈ eqv_validators
  specialize (Hvs' _ _ Hpre_tr).message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr: list transition_item
Htr: finite_valid_trace_init_to StrongFixed is s tr
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
Hvs': ∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) m tr
v ∈ eqv_validators
  destruct Hvs' as [m0 [Hsender0 [pre [item [suf [Heqtr [Hm0 Heqv]]]]]]].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr: list transition_item
Htr: finite_valid_trace_init_to StrongFixed is s tr
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
pre: list transition_item
item: transition_item
suf: list transition_item
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
v ∈ eqv_validators
  rewrite Heqtr in Htr.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Htr: finite_valid_trace_init_to StrongFixed is s
  (pre ++ item :: suf)
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
v ∈ eqv_validators
  destruct Htr as [Htr Hinit].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Htr: finite_valid_trace_from_to StrongFixed is s
  (pre ++ item :: suf)
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
v ∈ eqv_validators
  change (pre ++ item :: suf) with (pre ++ [item] ++ suf) in Htr.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Htr: finite_valid_trace_from_to StrongFixed is s
  (pre ++ [item] ++ suf)
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
v ∈ eqv_validators
  apply (finite_valid_trace_from_to_app_split StrongFixed) in Htr.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Htr: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
∧ finite_valid_trace_from_to StrongFixed
    (finite_trace_last is pre) s 
    ([item] ++ suf)
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
v ∈ eqv_validators
  destruct Htr as [Hpre Hitem].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
Hitem: finite_valid_trace_from_to StrongFixed
  (finite_trace_last is pre) s 
  ([item] ++ suf)
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
v ∈ eqv_validators
  eapply VLSM_incl_finite_valid_trace_from_to in Hpre as Hpre_pre;
    [| by apply constrained_preloaded_incl].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
Hitem: finite_valid_trace_from_to StrongFixed
  (finite_trace_last is pre) s 
  ([item] ++ suf)
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
v ∈ eqv_validators
  apply valid_trace_last_pstate in Hpre_pre as Hs_pre.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
Hitem: finite_valid_trace_from_to StrongFixed
  (finite_trace_last is pre) s 
  ([item] ++ suf)
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
v ∈ eqv_validators
  apply (finite_valid_trace_from_to_app_split StrongFixed), proj1 in Hitem.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
tr, pre: list transition_item
item: transition_item
suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
Hitem: finite_valid_trace_from_to StrongFixed
  (finite_trace_last is pre)
  (finite_trace_last
     (finite_trace_last is pre) [item]) [item]
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s tr
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Heqtr: tr = pre ++ item :: suf
Hm0: input item = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
v ∈ eqv_validators
  inversion Hitem; subst; clear Htl Hitem.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
iom, oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := iom;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Hm0: input
  {|
    l := l;
    input := iom;
    destination := s0;
    output := oom
  |} = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
Ht: input_valid_transition StrongFixed l
  (finite_trace_last is pre, iom) (
  s0, oom)
v ∈ eqv_validators simpl in Hm0.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
iom, oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := iom;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
m0: message
Hsender0: sender m0 = Some v
Hm0: iom = Some m0
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
Ht: input_valid_transition StrongFixed l
  (finite_trace_last is pre, iom) (
  s0, oom)
v ∈ eqv_validators subst.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
Ht: input_valid_transition StrongFixed l
  (finite_trace_last is pre, Some m0) (
  s0, oom)
v ∈ eqv_validators
  destruct Ht as [(_ & _ & _ & Hc) _].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
Hc: strong_fixed_equivocation_constraint IM
  equivocators l
  (finite_trace_last is pre, Some m0)
v ∈ eqv_validators
  destruct Hc as [(i & Hi & Hsenti) | Hemit].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
i: index
Hi: i ∉ elements equivocators
Hsenti: has_been_sent (IM i)
  (finite_trace_last is pre i) m0
v ∈ eqv_validators
message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
Hemit: can_emit
  (equivocators_composition_for_sent IM
     equivocators (finite_trace_last is pre))
  m0
v ∈ eqv_validators
  -message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
i: index
Hi: i ∉ elements equivocators
Hsenti: has_been_sent (IM i)
  (finite_trace_last is pre i) m0
v ∈ eqv_validators assert (Hsent : composite_has_been_sent IM (finite_trace_last is pre) m0)
      by (exists i; done).message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
i: index
Hi: i ∉ elements equivocators
Hsenti: has_been_sent (IM i)
  (finite_trace_last is pre i) m0
Hsent: composite_has_been_sent IM
  (finite_trace_last is pre) m0
v ∈ eqv_validators
    apply (composite_proper_sent IM) in Hsent; [| done].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
i: index
Hi: i ∉ elements equivocators
Hsenti: has_been_sent (IM i)
  (finite_trace_last is pre i) m0
Hsent: selected_message_exists_in_all_preloaded_traces
  (free_composite_vlsm IM)
  (field_selector output)
  (finite_trace_last is pre) m0
v ∈ eqv_validators
    by specialize (Hsent _ _ (conj Hpre_pre Hinit)).
  -message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
Hemit: can_emit
  (equivocators_composition_for_sent IM
     equivocators (finite_trace_last is pre))
  m0
v ∈ eqv_validators apply (SubProjectionTraces.sub_can_emit_sender IM (elements equivocators)
      A sender Hsender_safety _ _ v), elem_of_elements in Hemit; [| done].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
s, is: state StrongFixed
pre, suf: list transition_item
Hpre: finite_valid_trace_from_to StrongFixed is
  (finite_trace_last is pre) pre
s0: state StrongFixed
oom: option message
l: label StrongFixed
Hinit: initial_state_prop is
m0: message
Hpre_tr: finite_valid_trace_init_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is s
  (pre ++
   {|
     l := l;
     input := Some m0;
     destination := s0;
     output := oom
   |} :: suf)
v: validator
Hv: v ∈ equivocating_validators s
Hsender0: sender m0 = Some v
Heqv: ¬ trace_has_message (field_selector output) m0
    pre
Hpre_pre: finite_valid_trace_from_to
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} is (finite_trace_last is pre) pre
Hs_pre: valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      preloaded_with_all_messages_vlsm
        (free_composite_vlsm IM)
  |} (finite_trace_last is pre)
Hemit: A v ∈ equivocators
v ∈ eqv_validators
    by revert Hemit; apply elem_of_set_map_inj.
Qed.

Lemma StrongFixed_incl_Limited : VLSM_incl StrongFixed Limited.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
VLSM_incl StrongFixed Limited
Proof.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
VLSM_incl StrongFixed Limited
  apply constraint_subsumption_incl.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
input_valid_constraint_subsumption
  (free_composite_vlsm IM)
  (strong_fixed_equivocation_constraint IM
     equivocators)
  (limited_equivocation_constraint IM threshold
     is_equivocating)
  intros [i li] [s om] Hpv.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
i: index
li: label (IM i)
s: state (free_composite_vlsm IM)
om: option message
Hpv: input_valid
  (constrained_vlsm (free_composite_vlsm IM)
     (strong_fixed_equivocation_constraint IM
        equivocators)) 
  (existT i li) (s, om)
limited_equivocation_constraint IM threshold
  is_equivocating (existT i li) (s, om)
  unfold limited_equivocation_constraint.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
i: index
li: label (IM i)
s: state (free_composite_vlsm IM)
om: option message
Hpv: input_valid
  (constrained_vlsm (free_composite_vlsm IM)
     (strong_fixed_equivocation_constraint IM
        equivocators)) 
  (existT i li) (s, om)
LimitedEquivocationProp IM threshold is_equivocating
  (composite_transition IM (existT i li) (s, om)).1
  destruct (composite_transition _ _ _) as [s' om'] eqn: Ht.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
i: index
li: label (IM i)
s: state (free_composite_vlsm IM)
om: option message
Hpv: input_valid
  (constrained_vlsm (free_composite_vlsm IM)
     (strong_fixed_equivocation_constraint IM
        equivocators)) 
  (existT i li) (s, om)
s': composite_state IM
om': option message
Ht: composite_transition IM (existT i li) (s, om) =
(s', om')
LimitedEquivocationProp IM threshold is_equivocating
  (s', om').1
  by eapply tracewise_not_heavy_LimitedEquivocationProp_iff,
    StrongFixed_valid_state_not_heavy, input_valid_transition_destination.
Qed.

Lemma Fixed_incl_Limited : VLSM_incl Fixed Limited.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
VLSM_incl Fixed Limited
Proof.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
VLSM_incl Fixed Limited
  destruct (Fixed_eq_StrongFixed IM equivocators) as [Heq _].message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
Heq: VLSM_incl
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      fixed_equivocation_vlsm_composition IM
        equivocators
  |}
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      strong_fixed_equivocation_vlsm_composition
        IM equivocators
  |}
VLSM_incl Fixed Limited
  apply VLSM_incl_trans with StrongFixed.message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
Heq: VLSM_incl
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      fixed_equivocation_vlsm_composition IM
        equivocators
  |}
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      strong_fixed_equivocation_vlsm_composition
        IM equivocators
  |}
VLSM_incl
  {|
    vlsm_type := StrongFixed;
    vlsm_machine :=
      constrained_vlsm_machine
        (free_composite_vlsm IM)
        (fixed_equivocation_constraint IM equivocators)
  |}
  {|
    vlsm_type := StrongFixed;
    vlsm_machine := StrongFixed
  |}
message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
Heq: VLSM_incl
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      fixed_equivocation_vlsm_composition IM
        equivocators
  |}
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      strong_fixed_equivocation_vlsm_composition
        IM equivocators
  |}
VLSM_incl
  {|
    vlsm_type := StrongFixed;
    vlsm_machine := StrongFixed
  |}
  {|
    vlsm_type := StrongFixed;
    vlsm_machine :=
      constrained_vlsm_machine
        (free_composite_vlsm IM)
        (limited_equivocation_constraint IM threshold
           is_equivocating)
  |}
  -message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
Heq: VLSM_incl
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      fixed_equivocation_vlsm_composition IM
        equivocators
  |}
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      strong_fixed_equivocation_vlsm_composition
        IM equivocators
  |}
VLSM_incl
  {|
    vlsm_type := StrongFixed;
    vlsm_machine :=
      constrained_vlsm_machine
        (free_composite_vlsm IM)
        (fixed_equivocation_constraint IM equivocators)
  |}
  {|
    vlsm_type := StrongFixed;
    vlsm_machine := StrongFixed
  |} by apply Heq.
  -message, index: Type
IM: index → VLSM message
threshold: R
Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
H8: ∀ i : index, HasBeenSentCapability (IM i)
H9: ∀ i : index, HasBeenReceivedCapability (IM i)
Free:= free_composite_vlsm IM: VLSM message
validator: Type
EqDecision1: EqDecision validator
H10: finite.Finite validator
Cv: Type
Hm: Measurable validator
H11: ElemOf validator Cv
H12: Empty Cv
H13: Singleton validator Cv
H14: Union Cv
H15: Intersection Cv
H16: Difference Cv
H17: Elements validator Cv
EqDecision2: EqDecision validator
H18: FinSet validator Cv
H19: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
eqv_validators: Cv
equivocators:= set_map A eqv_validators: Ci
Hlimited: (sum_weights eqv_validators <= threshold)%R
Hsender_safety: sender_safety_alt_prop IM A sender
H20: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Fixed:= fixed_equivocation_vlsm_composition IM
  equivocators: VLSM message
StrongFixed:= strong_fixed_equivocation_vlsm_composition
  IM equivocators: VLSM message
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
HBE:= equivocation_dec_tracewise IM threshold A sender: BasicEquivocation (composite_state IM) validator
  Cv threshold
Heq: VLSM_incl
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      fixed_equivocation_vlsm_composition IM
        equivocators
  |}
  {|
    vlsm_type :=
      fixed_equivocation_vlsm_composition IM
        equivocators;
    vlsm_machine :=
      strong_fixed_equivocation_vlsm_composition
        IM equivocators
  |}
VLSM_incl
  {|
    vlsm_type := StrongFixed;
    vlsm_machine := StrongFixed
  |}
  {|
    vlsm_type := StrongFixed;
    vlsm_machine :=
      constrained_vlsm_machine
        (free_composite_vlsm IM)
        (limited_equivocation_constraint IM threshold
           is_equivocating)
  |} by apply StrongFixed_incl_Limited.
Qed.

End sec_fixed_limited_message_equivocation.

Section sec_has_limited_equivocation.

Limited Equivocation derived from Fixed Equivocation

We say that a trace has the fixed_limited_equivocation_property if it is valid for the composition using a generalized_fixed_equivocation_constraint induced by a subset of indices whose weight is less than the allowed ReachableThreshold.

Context
  {message}
  `{FinSet index Ci}
  `{!finite.Finite index}
  (IM : index -> VLSM message)
  (threshold : R)
  `{finite.Finite validator}
  `{ReachableThreshold validator Cv threshold}
  (A : validator -> index)
  `{!Inj (=) (=) A}
  (sender : message -> option validator)
  `{forall i, HasBeenSentCapability (IM i)}
  `{forall i, HasBeenReceivedCapability (IM i)}
  .

Definition fixed_limited_equivocation_prop
  (s : composite_state IM)
  (tr : list (composite_transition_item IM))
  : Prop
  :=
    exists equivocators : Cv,
      (sum_weights equivocators <= threshold)%R /\
      finite_valid_trace (fixed_equivocation_vlsm_composition (Ci := Ci) IM (fin_sets.set_map A equivocators)) s tr.

Context
  `{FinSet message Cm}
  (message_dependencies : message -> Cm)
  `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM A sender)}
  (Limited : VLSM message :=
    tracewise_limited_equivocation_vlsm_composition (Cv := Cv) IM threshold A sender)
  .

Traces with the fixed_limited_equivocation_property are valid for the composition using a limited_equivocation_constraint.

Lemma traces_exhibiting_limited_equivocation_are_valid
  (Hsender_safety : sender_safety_alt_prop IM A sender)
  : forall s tr, fixed_limited_equivocation_prop s tr -> finite_valid_trace Limited s tr.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM A sender
∀ (s : composite_state IM) (tr : list
                                   (composite_transition_item
                                      IM)),
  fixed_limited_equivocation_prop s tr
  → finite_valid_trace Limited s tr
Proof.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM A sender
∀ (s : composite_state IM) (tr : list
                                   (composite_transition_item
                                      IM)),
  fixed_limited_equivocation_prop s tr
  → finite_valid_trace Limited s tr
  intros s tr [equivocators [Hlimited Htr]].message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
tr: list (composite_transition_item IM)
equivocators: Cv
Hlimited: (sum_weights equivocators <= threshold)%R
Htr: finite_valid_trace
  (fixed_equivocation_vlsm_composition IM
     (set_map A equivocators)) s tr
finite_valid_trace Limited s tr
  eapply VLSM_incl_finite_valid_trace; [| done].message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
tr: list (composite_transition_item IM)
equivocators: Cv
Hlimited: (sum_weights equivocators <= threshold)%R
Htr: finite_valid_trace
  (fixed_equivocation_vlsm_composition IM
     (set_map A equivocators)) s tr
VLSM_incl_part
  (constrained_vlsm_machine (free_composite_vlsm IM)
     (fixed_equivocation_constraint IM
        (set_map A equivocators)))
  (constrained_vlsm_machine (free_composite_vlsm IM)
     (limited_equivocation_constraint IM threshold
        is_equivocating))
  by eapply Fixed_incl_Limited.
Qed.

Traces having the strong_trace_witnessing_equivocation_property, which are valid for the free composition and whose final state is not_heavy have the fixed_limited_equivocation_property.

Lemma traces_exhibiting_limited_equivocation_are_valid_rev
  (Hke : WitnessedEquivocationCapability IM threshold A sender (Cv := Cv))
  `{!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 A sender)
  (Htracewise_basic_equivocation : BasicEquivocation (composite_state IM) validator Cv threshold
    := equivocation_dec_tracewise IM threshold A sender)
  (tracewise_not_heavy := not_heavy (1 := Htracewise_basic_equivocation) (Cv := Cv))
  : forall is s tr, strong_trace_witnessing_equivocation_prop IM threshold A sender is tr (Cv := Cv) ->
    finite_valid_trace_init_to (free_composite_vlsm IM) is s tr ->
    tracewise_not_heavy s ->
    fixed_limited_equivocation_prop is tr.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
∀ (is : state (composite_type IM)) (s : state
                                          (free_composite_vlsm
                                             IM)) 
  (tr : list transition_item),
  strong_trace_witnessing_equivocation_prop IM
    threshold A sender is tr
  → finite_valid_trace_init_to
      (free_composite_vlsm IM) is s tr
    → tracewise_not_heavy s
      → fixed_limited_equivocation_prop is tr
Proof.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
∀ (is : state (composite_type IM)) (s : state
                                          (free_composite_vlsm
                                             IM)) 
  (tr : list transition_item),
  strong_trace_witnessing_equivocation_prop IM
    threshold A sender is tr
  → finite_valid_trace_init_to
      (free_composite_vlsm IM) is s tr
    → tracewise_not_heavy s
      → fixed_limited_equivocation_prop is tr
  intros is s tr Hstrong Htr Hnot_heavy.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
is: state (composite_type IM)
s: state (free_composite_vlsm IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Hnot_heavy: tracewise_not_heavy s
fixed_limited_equivocation_prop is tr
  exists (equivocating_validators s).message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
is: state (composite_type IM)
s: state (free_composite_vlsm IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Hnot_heavy: tracewise_not_heavy s
(sum_weights (equivocating_validators s) <= threshold)%R
∧ finite_valid_trace
    (fixed_equivocation_vlsm_composition IM
       (set_map A (equivocating_validators s))) is tr
  split; cycle 1.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
is: state (composite_type IM)
s: state (free_composite_vlsm IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Hnot_heavy: tracewise_not_heavy s
finite_valid_trace
  (fixed_equivocation_vlsm_composition IM
     (set_map A (equivocating_validators s))) is tr
message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
is: state (composite_type IM)
s: state (free_composite_vlsm IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Hnot_heavy: tracewise_not_heavy s
(sum_weights (equivocating_validators s) <= threshold)%R
  -message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
is: state (composite_type IM)
s: state (free_composite_vlsm IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Hnot_heavy: tracewise_not_heavy s
finite_valid_trace
  (fixed_equivocation_vlsm_composition IM
     (set_map A (equivocating_validators s))) is tr by eapply valid_trace_forget_last, strong_witness_has_fixed_equivocation.
  -message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
Htracewise_basic_equivocation:= equivocation_dec_tracewise
  IM threshold A sender: BasicEquivocation
  (composite_state IM)
  validator Cv
  threshold
tracewise_not_heavy:= not_heavy: composite_state IM → Prop
is: state (composite_type IM)
s: state (free_composite_vlsm IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Hnot_heavy: tracewise_not_heavy s
(sum_weights (equivocating_validators s) <= threshold)%R by replace (sum_weights _) with (equivocation_fault s).
Qed.

Traces with the strong_trace_witnessing_equivocation_property, which are valid for the composition using a limited_equivocation_constraint have the fixed_limited_equivocation_property.

Lemma limited_traces_exhibiting_limited_equivocation_are_valid_rev
  (Hke : WitnessedEquivocationCapability IM threshold A sender (Cv := Cv))
  `{!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 A sender)
  : forall s tr, strong_trace_witnessing_equivocation_prop IM threshold A sender s tr (Cv := Cv) ->
    finite_valid_trace Limited s tr -> fixed_limited_equivocation_prop s tr.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
∀ (s : state (composite_type IM)) (tr : list
                                          transition_item),
  strong_trace_witnessing_equivocation_prop IM
    threshold A sender s tr
  → finite_valid_trace Limited s tr
    → fixed_limited_equivocation_prop s tr
Proof.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
∀ (s : state (composite_type IM)) (tr : list
                                          transition_item),
  strong_trace_witnessing_equivocation_prop IM
    threshold A sender s tr
  → finite_valid_trace Limited s tr
    → fixed_limited_equivocation_prop s tr
  intros s tr Hstrong Htr.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state (composite_type IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender s tr
Htr: finite_valid_trace Limited s tr
fixed_limited_equivocation_prop s tr
  eapply traces_exhibiting_limited_equivocation_are_valid_rev; [done.. | |].message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state (composite_type IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender s tr
Htr: finite_valid_trace Limited s tr
finite_valid_trace_init_to (free_composite_vlsm IM) s
  ?s tr
message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state (composite_type IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender s tr
Htr: finite_valid_trace Limited s tr
not_heavy ?s
  -message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state (composite_type IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender s tr
Htr: finite_valid_trace Limited s tr
finite_valid_trace_init_to (free_composite_vlsm IM) s
  ?s tr apply valid_trace_add_default_last.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state (composite_type IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender s tr
Htr: finite_valid_trace Limited s tr
finite_valid_trace (free_composite_vlsm IM) s tr
    eapply VLSM_incl_finite_valid_trace; [| done].message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state (composite_type IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender s tr
Htr: finite_valid_trace Limited s tr
VLSM_incl_part
  (constrained_vlsm_machine (free_composite_vlsm IM)
     (limited_equivocation_constraint IM threshold
        is_equivocating))
  (free_composite_vlsm_machine IM)
    by apply (VLSM_incl_constrained_vlsm (free_composite_vlsm IM)).
  -message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state (composite_type IM)
tr: list transition_item
Hstrong: strong_trace_witnessing_equivocation_prop IM
  threshold A sender s tr
Htr: finite_valid_trace Limited s tr
not_heavy (finite_trace_last s tr) by apply tracewise_not_heavy_LimitedEquivocationProp_iff,
      full_node_limited_equivocation_valid_state_weight,
      finite_valid_trace_last_pstate with (X := Limited), Htr.
Qed.

Any state which is valid for limited equivocation can be produced by a trace having the fixed_limited_equivocation_property.

Lemma limited_valid_state_has_trace_exhibiting_limited_equivocation
  (Hke : WitnessedEquivocationCapability IM threshold A sender (Cv := Cv))
  `{!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 A sender)
  : forall s, valid_state_prop Limited s ->
    exists is tr, finite_trace_last is tr = s /\ fixed_limited_equivocation_prop is tr.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
∀ s : state Limited,
  valid_state_prop Limited s
  → ∃ (is : state Limited) (tr : list transition_item),
      finite_trace_last is tr = s
      ∧ fixed_limited_equivocation_prop is tr
Proof.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
∀ s : state Limited,
  valid_state_prop Limited s
  → ∃ (is : state Limited) (tr : list transition_item),
      finite_trace_last is tr = s
      ∧ fixed_limited_equivocation_prop is tr
  intros s Hs.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
∃ (is : state Limited) (tr : list transition_item),
  finite_trace_last is tr = s
  ∧ fixed_limited_equivocation_prop is tr
  assert (Hfree_s : valid_state_prop (free_composite_vlsm IM) s).message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
valid_state_prop (free_composite_vlsm IM) s
message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
Hfree_s: valid_state_prop (free_composite_vlsm IM) s
∃ (is : state Limited) (tr : list transition_item),
  finite_trace_last is tr = s
  ∧ fixed_limited_equivocation_prop is tr
  {message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
valid_state_prop (free_composite_vlsm IM) s
    apply VLSM_incl_valid_state; [| done].message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
VLSM_incl_part
  (constrained_vlsm_machine (free_composite_vlsm IM)
     (limited_equivocation_constraint IM threshold
        is_equivocating))
  (free_composite_vlsm_machine IM)
    by apply (VLSM_incl_constrained_vlsm (free_composite_vlsm IM)).
  }message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
Hfree_s: valid_state_prop (free_composite_vlsm IM) s
∃ (is : state Limited) (tr : list transition_item),
  finite_trace_last is tr = s
  ∧ fixed_limited_equivocation_prop is tr
  destruct
    (free_has_strong_trace_witnessing_equivocation_prop IM threshold A sender _ s Hfree_s)
    as (is & tr & Htr & Heqv).message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
Hfree_s: valid_state_prop (free_composite_vlsm IM) s
is: state (free_composite_vlsm IM)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Heqv: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
∃ (is : state Limited) (tr : list transition_item),
  finite_trace_last is tr = s
  ∧ fixed_limited_equivocation_prop is tr
  exists is, tr.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
Hfree_s: valid_state_prop (free_composite_vlsm IM) s
is: state (free_composite_vlsm IM)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Heqv: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
finite_trace_last is tr = s
∧ fixed_limited_equivocation_prop is tr
  apply valid_trace_get_last in Htr as Hlst.message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
Hfree_s: valid_state_prop (free_composite_vlsm IM) s
is: state (free_composite_vlsm IM)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Heqv: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Hlst: finite_trace_last is tr = s
finite_trace_last is tr = s
∧ fixed_limited_equivocation_prop is tr
  split; [done |].message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
Hfree_s: valid_state_prop (free_composite_vlsm IM) s
is: state (free_composite_vlsm IM)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Heqv: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Hlst: finite_trace_last is tr = s
fixed_limited_equivocation_prop is tr
  eapply traces_exhibiting_limited_equivocation_are_valid_rev; [done.. |].message, index, Ci: Type
H: ElemOf index Ci
H0: Empty Ci
H1: Singleton index Ci
H2: Union Ci
H3: Intersection Ci
H4: Difference Ci
H5: Elements index Ci
EqDecision0: EqDecision index
H6: FinSet index Ci
H7: finite.Finite index
IM: index → VLSM message
threshold: R
validator: Type
EqDecision1: EqDecision validator
H8: finite.Finite validator
Cv: Type
Hm: Measurable validator
H9: ElemOf validator Cv
H10: Empty Cv
H11: Singleton validator Cv
H12: Union Cv
H13: Intersection Cv
H14: Difference Cv
H15: Elements validator Cv
EqDecision2: EqDecision validator
H16: FinSet validator Cv
H17: ReachableThreshold validator Cv threshold
A: validator → index
Inj0: Inj eq eq A
sender: message → option validator
H18: ∀ i : index, HasBeenSentCapability (IM i)
H19: ∀ i : index, HasBeenReceivedCapability (IM i)
Cm: Type
H20: ElemOf message Cm
H21: Empty Cm
H22: Singleton message Cm
H23: Union Cm
H24: Intersection Cm
H25: Difference Cm
H26: Elements message Cm
EqDecision3: EqDecision message
H27: FinSet message Cm
message_dependencies: message → Cm
H28: RelDecision
  (is_equivocating_tracewise_no_has_been_sent IM
     A sender)
Limited:= tracewise_limited_equivocation_vlsm_composition
  IM threshold A sender: VLSM message
Hke: WitnessedEquivocationCapability IM threshold A
  sender
Irreflexive0: Irreflexive
  (msg_dep_happens_before
     message_dependencies)
H29: ∀ 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 A
  sender
s: state Limited
Hs: valid_state_prop Limited s
Hfree_s: valid_state_prop (free_composite_vlsm IM) s
is: state (free_composite_vlsm IM)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (free_composite_vlsm IM) is s tr
Heqv: strong_trace_witnessing_equivocation_prop IM
  threshold A sender is tr
Hlst: finite_trace_last is tr = s
not_heavy s
  by apply tracewise_not_heavy_LimitedEquivocationProp_iff,
    full_node_limited_equivocation_valid_state_weight.
Qed.

End sec_has_limited_equivocation.