Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[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 Reals Lra. From VLSM.Lib Require Import Preamble Measurable RealsExtras FinSetExtras. From VLSM.Core Require Import VLSM VLSMProjections Composition AnnotatedVLSM. From VLSM.Core Require Import Equivocation Equivocation.TraceWiseEquivocation MessageDependencies. From VLSM.Core Require Import Equivocation.NoEquivocation Equivocation.LimitedMessageEquivocation. From VLSM.Core Require Import FixedSetEquivocation MsgDepLimitedEquivocation. From VLSM.Core Require Import Equivocators.Equivocators.
[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
[Loading ML file equations_plugin.cmxs (using legacy method) ... done]
From VLSM.Core Require Import Equivocators.EquivocatorsComposition. From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections. From VLSM.Core Require Import Equivocators.FixedEquivocation.

Core: VLSM Limited Equivocation

Definition composite_constraint
  {index message} (IM : index -> VLSM message) : Type :=
  composite_label IM -> composite_state IM * option message -> Prop.

message: Type
X: VLSM message
es: state (equivocator_vlsm X)
eqv_descriptor: MachineDescriptor X
Heqv: proper_descriptor X eqv_descriptor es
Hes: initial_state_prop es

initial_state_prop (equivocator_state_descriptor_project es eqv_descriptor)
message: Type
X: VLSM message
es: state (equivocator_vlsm X)
eqv_descriptor: MachineDescriptor X
Heqv: proper_descriptor X eqv_descriptor es
Hes: initial_state_prop es

initial_state_prop (equivocator_state_descriptor_project es eqv_descriptor)
message: Type
X: VLSM message
es: state (equivocator_vlsm X)
n: nat
Heqv: proper_descriptor X (Existing n) es
Hes: initial_state_prop es

initial_state_prop (equivocator_state_descriptor_project es (Existing n))
message: Type
X: VLSM message
es: state (equivocator_vlsm X)
n: nat
esn: state X
Hesn: equivocator_state_project es n = Some esn
Hes: initial_state_prop es

initial_state_prop (equivocator_state_descriptor_project es (Existing n))
message: Type
X: VLSM message
es: state (equivocator_vlsm X)
n: nat
esn: state X
Hesn: equivocator_state_project es n = Some esn
Hes: initial_state_prop es

initial_state_prop (default (equivocator_state_zero es) (equivocator_state_project es n))
message: Type
X: VLSM message
es: state (equivocator_vlsm X)
n: nat
esn: state X
Hesn: equivocator_state_project es n = Some esn
Hes: initial_state_prop es

initial_state_prop (default (equivocator_state_zero es) (Some esn))
by eapply equivocator_vlsm_initial_state_preservation_rev. Qed.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
es: composite_state (equivocator_IM IM)
eqv_descriptors: equivocator_descriptors IM
eqv_constraint: composite_constraint (equivocator_IM IM)
constraint: composite_constraint IM
Heqv: proper_equivocator_descriptors IM eqv_descriptors es
Hes: initial_state_prop es

initial_state_prop (equivocators_state_project IM eqv_descriptors es)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
es: composite_state (equivocator_IM IM)
eqv_descriptors: equivocator_descriptors IM
eqv_constraint: composite_constraint (equivocator_IM IM)
constraint: composite_constraint IM
Heqv: proper_equivocator_descriptors IM eqv_descriptors es
Hes: initial_state_prop es

initial_state_prop (equivocators_state_project IM eqv_descriptors es)
refine (fun i => equivocator_initial_state_project _ _ _ (Heqv i) (Hes i)). Qed. Section sec_limited_state_equivocation. Context {message index : Type} (IM : index -> VLSM message) `{forall i : index, HasBeenSentCapability (IM i)} `{forall i : index, HasBeenReceivedCapability (IM i)} (threshold : R) `{ReachableThreshold index Ci threshold} `{!finite.Finite index} (Free := free_composite_vlsm IM) (sender : message -> option index) (HBE : BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold := equivocating_indices_BasicEquivocation IM threshold) (FreeE : VLSM message := free_composite_vlsm (equivocator_IM IM)) . Definition equivocators_limited_equivocations_constraint (l : composite_label (equivocator_IM IM)) (som : composite_state (equivocator_IM IM) * option message) (som' := composite_transition (equivocator_IM IM) l som) : Prop := equivocators_no_equivocations_constraint IM l som /\ not_heavy (1 := HBE) (fst som'). Definition equivocators_limited_equivocations_vlsm : VLSM message := composite_vlsm (equivocator_IM IM) equivocators_limited_equivocations_constraint.
Inclusion in the free composition.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message

VLSM_incl equivocators_limited_equivocations_vlsm FreeE
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message

VLSM_incl equivocators_limited_equivocations_vlsm FreeE
by apply VLSM_incl_constrained_vlsm. Qed.
Inclusion of preloaded machine in the preloaded free composition.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message

VLSM_incl (preloaded_with_all_messages_vlsm equivocators_limited_equivocations_vlsm) (preloaded_with_all_messages_vlsm FreeE)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message

VLSM_incl (preloaded_with_all_messages_vlsm equivocators_limited_equivocations_vlsm) (preloaded_with_all_messages_vlsm FreeE)
by apply basic_VLSM_incl_preloaded; intros ? *; [intro | inversion 1 | intro]. Qed.
Inclusion in the composition of equivocators with no message equivocation (no restriction on state equivocation).
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message

VLSM_incl equivocators_limited_equivocations_vlsm (equivocators_no_equivocations_vlsm IM)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message

VLSM_incl equivocators_limited_equivocations_vlsm (equivocators_no_equivocations_vlsm IM)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message

input_valid_constraint_subsumption (free_composite_vlsm (equivocator_IM IM)) equivocators_limited_equivocations_constraint (equivocators_no_equivocations_constraint IM)
by intros l [s om] (_ & _ & _ & Hc & _). Qed.
A valid state for a VLSM satisfying the limited equivocation assumption has limited equivocation.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
s: composite_state (equivocator_IM IM)
Hs: valid_state_prop equivocators_limited_equivocations_vlsm s

not_heavy s
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
s: composite_state (equivocator_IM IM)
Hs: valid_state_prop equivocators_limited_equivocations_vlsm s

not_heavy s
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
s: composite_state (equivocator_IM IM)
Hs: ( is : initial_state equivocators_limited_equivocations_vlsm, s = `is) ∨ ( (l : label equivocators_limited_equivocations_vlsm) (som : state equivocators_limited_equivocations_vlsm * option message) (om' : option message), input_valid_transition equivocators_limited_equivocations_vlsm l som (s, om'))

not_heavy s
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
s: composite_state (equivocator_IM IM)
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is
Heq_s: s = `(is ↾ His)

not_heavy s
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
s: composite_state (equivocator_IM IM)
l: label equivocators_limited_equivocations_vlsm
s0: state equivocators_limited_equivocations_vlsm
oim, oom': option message
Hlimited: not_heavy (composite_transition (equivocator_IM IM) l ( s0, oim)).1
Ht: transition l (s0, oim) = (s, oom')
not_heavy s
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
s: composite_state (equivocator_IM IM)
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is
Heq_s: s = `(is ↾ His)

not_heavy s
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is

not_heavy (`(is ↾ His))
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is

(sum_weights (equivocating_validators is) <= threshold)%R
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is
Heqv_is: equivocating_validators is ≡ list_to_set (equivocating_indices IM (enum index) is)

(sum_weights (equivocating_validators is) <= threshold)%R
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is
Heqv_is: equivocating_validators is ≡ list_to_set []

(sum_weights (equivocating_validators is) <= threshold)%R
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is
Heqv_is: sum_weights (equivocating_validators is) = 0%R

(sum_weights (equivocating_validators is) <= threshold)%R
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is: state equivocators_limited_equivocations_vlsm
His: initial_state_prop is
Heqv_is: sum_weights (equivocating_validators is) = 0%R
H11: (0 <= threshold)%R

(sum_weights (equivocating_validators is) <= threshold)%R
by cbv in Heqv_is |- *; lra.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
s: composite_state (equivocator_IM IM)
l: label equivocators_limited_equivocations_vlsm
s0: state equivocators_limited_equivocations_vlsm
oim, oom': option message
Hlimited: not_heavy (composite_transition (equivocator_IM IM) l ( s0, oim)).1
Ht: transition l (s0, oim) = (s, oom')

not_heavy s
by replace s with (fst (composite_transition (equivocator_IM IM) l (s0, oim))); [done |] ; cbn in *; rewrite Ht. Qed.
A valid valid trace for the composition of equivocators with limited state-equivocation and no message-equivocation is also a valid valid trace for the composition of equivocators with no message-equivocation and fixed-set state-equivocation, where the fixed set is given by the state-equivocators measured for the final state of the trace.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item

finite_valid_trace_init_to equivocators_limited_equivocations_vlsm is s tr → finite_valid_trace_init_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators s))) is s tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item

finite_valid_trace_init_to equivocators_limited_equivocations_vlsm is s tr → finite_valid_trace_init_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators s))) is s tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm is s tr

finite_valid_trace_init_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators s))) is s tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm is s tr

finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators s))) is s tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
is, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm is s tr

equivocating : list index, elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) is s tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si: state equivocators_limited_equivocations_vlsm
Hsi: initial_state_prop si
equivocating: list index
Hincl: elements (equivocating_validators si) ⊆ equivocating

finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si si []
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
IHHtr: equivocating : list index, elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si: state equivocators_limited_equivocations_vlsm
Hsi: initial_state_prop si
equivocating: list index
Hincl: elements (equivocating_validators si) ⊆ equivocating

finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si si []
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si: state equivocators_limited_equivocations_vlsm
Hsi: initial_state_prop si
equivocating: list index
Hincl: elements (equivocating_validators si) ⊆ equivocating

valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) si
by apply initial_state_is_valid.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
IHHtr: equivocating : list index, elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating

finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
IHHtr: elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
Hincl: elements (equivocating_validators sf) ⊆ equivocating

finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
IHHtr: elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
Hincl: elements (equivocating_validators sf) ⊆ equivocating

elements (equivocating_validators s) ⊆ equivocating
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
IHHtr: elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
Hincl: elements (equivocating_validators sf) ⊆ equivocating

elements (equivocating_validators s) ⊆ equivocating
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
IHHtr: elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
Hincl: elements (equivocating_validators sf) ⊆ equivocating

elements (equivocating_validators s) ⊆ equivocating
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
IHHtr: elements (equivocating_validators s) ⊆ equivocating → finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr
Hincl: elements (equivocating_validators sf) ⊆ equivocating
Hincl': equivocating_indices IM (enum index) s ⊆ equivocating_indices IM (enum index) sf

elements (equivocating_validators s) ⊆ equivocating
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
s, sf: state equivocators_limited_equivocations_vlsm
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
Hincl': equivocating_indices IM (enum index) s ⊆ equivocating_indices IM (enum index) sf

elements (equivocating_validators s) ⊆ equivocating
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
s, sf: state equivocators_limited_equivocations_vlsm
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
Hincl': equivocating_indices IM (enum index) s ⊆ equivocating_indices IM (enum index) sf

elements (equivocating_validators s) ⊆ elements (equivocating_validators sf)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
s, sf: state equivocators_limited_equivocations_vlsm
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
Hincl': equivocating_indices IM (enum index) s ⊆ equivocating_indices IM (enum index) sf
x: index
Hx: x ∈ equivocating_validators s

x ∈ equivocating_validators sf
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
s, sf: state equivocators_limited_equivocations_vlsm
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
Hincl': equivocating_indices IM (enum index) s ⊆ equivocating_indices IM (enum index) sf
x: index
Hx: x ∈ equivocating_validators s

x ∈ equivocating_indices IM (enum index) s
by apply equivocating_indices_equivocating_validators, elem_of_list_to_set in Hx.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr

finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr

finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) s sf [{| l := l; input := iom; destination := sf; output := oom |}]
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr

finite_valid_trace_from (equivocators_fixed_equivocations_vlsm IM equivocating) s [{| l := l; input := iom; destination := sf; output := oom |}]
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: finite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si s tr

input_valid_transition (equivocators_fixed_equivocations_vlsm IM equivocating) l (s, iom) (sf, oom)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Ht: input_valid_transition equivocators_limited_equivocations_vlsm l (s, iom) (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

input_valid_transition (equivocators_fixed_equivocations_vlsm IM equivocating) l (s, iom) (sf, oom)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

input_valid_transition (equivocators_fixed_equivocations_vlsm IM equivocating) l (s, iom) (sf, oom)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

option_valid_message_prop (equivocators_fixed_equivocations_vlsm IM equivocating) iom
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s
state_has_fixed_equivocation IM equivocating (composite_transition (equivocator_IM IM) l (s, iom)).1
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

option_valid_message_prop (equivocators_fixed_equivocations_vlsm IM equivocating) iom
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
m: message
oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, Some m)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, Some m)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, Some m)).1
Ht: transition l (s, Some m) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

option_valid_message_prop (equivocators_fixed_equivocations_vlsm IM equivocating) (Some m)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
m: message
oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, Some m)
Hsent: composite_has_been_sent (equivocator_IM IM) ( s, Some m).1 m
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, Some m)).1
Ht: transition l (s, Some m) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

option_valid_message_prop (equivocators_fixed_equivocations_vlsm IM equivocating) (Some m)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
m: message
oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, Some m)
Hsent: composite_has_been_sent (equivocator_IM IM) s m
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, Some m)).1
Ht: transition l (s, Some m) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

option_valid_message_prop (equivocators_fixed_equivocations_vlsm IM equivocating) (Some m)
by eapply sent_valid.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

state_has_fixed_equivocation IM equivocating (composite_transition (equivocator_IM IM) l (s, iom)).1
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

state_has_fixed_equivocation IM equivocating (sf, oom).1
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

equivocating_indices IM (enum index) (sf, oom).1 ⊆ equivocating
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
si, s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
Htr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm si s tr
sf: state equivocators_limited_equivocations_vlsm
iom, oom: option message
l: label equivocators_limited_equivocations_vlsm
Hv: valid l (s, iom)
Hno_equiv: composite_no_equivocations (equivocator_IM IM) l ( s, iom)
Hno_heavy: not_heavy (composite_transition (equivocator_IM IM) l ( s, iom)).1
Ht: transition l (s, iom) = (sf, oom)
equivocating: list index
Hincl: elements (equivocating_validators sf) ⊆ equivocating
IHHtr: valid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) s

equivocating_indices IM (enum index) (sf, oom).1 ⊆ elements (equivocating_validators sf)
by intros x Hx; apply elem_of_elements, equivocating_indices_equivocating_validators, elem_of_list_to_set. Qed.
Projections of valid traces for the composition of equivocators with limited state-equivocation and no message-equivocation have the fixed_limited_equivocation_property.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace_init_to equivocators_limited_equivocations_vlsm is (finite_trace_last is tr) tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace_init_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is (finite_trace_last is tr) tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace_init_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is (finite_trace_last is tr) tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)

proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) final_descriptors (finite_trace_last is tr)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX
(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)

proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) final_descriptors (finite_trace_last is tr)
by eapply not_equivocating_equivocator_descriptors_proper_fixed.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)

finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
done.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ fixed_limited_equivocation_prop IM threshold Datatypes.id isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

(sum_weights (equivocating_validators (finite_trace_last is tr)) <= threshold)%R ∧ finite_valid_trace (fixed_equivocation_vlsm_composition IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr)))) (equivocators_state_project IM initial_descriptors is) trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

(sum_weights (equivocating_validators (finite_trace_last is tr)) <= threshold)%R
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX
finite_valid_trace (fixed_equivocation_vlsm_composition IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr)))) (equivocators_state_project IM initial_descriptors is) trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

(sum_weights (equivocating_validators (finite_trace_last is tr)) <= threshold)%R
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: not_heavy (finite_trace_last is tr)
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

(sum_weights (equivocating_validators (finite_trace_last is tr)) <= threshold)%R
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: not_heavy (finite_trace_last is tr)
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

(sum_weights (equivocating_validators (finite_trace_last is tr)) <= equivocation_fault (finite_trace_last is tr))%R
by unfold equivocation_fault; apply sum_weights_subseteq.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_fixed: finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX

finite_valid_trace (fixed_equivocation_vlsm_composition IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr)))) (equivocators_state_project IM initial_descriptors is) trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX

finite_valid_trace (fixed_equivocation_vlsm_composition IM (equivocating_validators (finite_trace_last is tr))) (equivocators_state_project IM initial_descriptors is) trX → finite_valid_trace (fixed_equivocation_vlsm_composition IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr)))) (equivocators_state_project IM initial_descriptors is) trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX

input_valid_constraint_subsumption (free_composite_vlsm IM) (fixed_equivocation_constraint IM (equivocating_validators (finite_trace_last is tr))) (fixed_equivocation_constraint IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))))
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX

strong_constraint_subsumption (free_composite_vlsm IM) (fixed_equivocation_constraint IM (equivocating_validators (finite_trace_last is tr))) (fixed_equivocation_constraint IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))))
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
l: label (free_composite_vlsm IM)
s: state (free_composite_vlsm IM)
m: message

fixed_equivocation IM (equivocating_validators (finite_trace_last is tr)) s m → fixed_equivocation IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))) s m
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
l: label (free_composite_vlsm IM)
s: state (free_composite_vlsm IM)
m: message
Hemit: can_emit (equivocators_composition_for_directly_observed IM (equivocating_validators (finite_trace_last is tr)) s) m

fixed_equivocation IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))) s m
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
l: label (free_composite_vlsm IM)
s: state (free_composite_vlsm IM)
m: message

can_emit (equivocators_composition_for_directly_observed IM (equivocating_validators (finite_trace_last is tr)) s) m → can_emit (equivocators_composition_for_directly_observed IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))) s) m
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
l: label (free_composite_vlsm IM)
s: state (free_composite_vlsm IM)
m: message

elements (equivocating_validators (finite_trace_last is tr)) ⊆ elements (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr)))
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
Hfixed_tr: finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is tr
Hfixed_last: valid_state_prop (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) (finite_trace_last is tr)
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
l: label (free_composite_vlsm IM)
s: state (free_composite_vlsm IM)
m: message

equivocating_validators (finite_trace_last is tr) ⊆ set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))
by intros v Hv; apply elem_of_map; eexists. Qed. Section sec_equivocators_projection_annotated_limited. Context `{FinSet message Cm} (message_dependencies : message -> Cm) (full_message_dependencies : message -> Cm) (HFullMsgDep : FullMessageDependencies message_dependencies full_message_dependencies) (HMsgDep : forall i, MessageDependencies (IM i) message_dependencies) (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM) (Hchannel : channel_authentication_prop IM Datatypes.id sender) .
Projections of valid traces for the composition of equivocators with limited state-equivocation and no message-equivocation can be annotated with equivocators to obtain a limited-message equivocation trace.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
HFullMsgDep: FullMessageDependencies message_dependencies full_message_dependencies
HMsgDep: i : index, MessageDependencies (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop IM
Hchannel: channel_authentication_prop IM Datatypes.id sender
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace (msg_dep_limited_equivocation_vlsm IM threshold full_message_dependencies sender) {| original_state := isX; state_annotation := `inhabitant |} (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender isX trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
HFullMsgDep: FullMessageDependencies message_dependencies full_message_dependencies
HMsgDep: i : index, MessageDependencies (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop IM
Hchannel: channel_authentication_prop IM Datatypes.id sender
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace (msg_dep_limited_equivocation_vlsm IM threshold full_message_dependencies sender) {| original_state := isX; state_annotation := `inhabitant |} (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender isX trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
HFullMsgDep: FullMessageDependencies message_dependencies full_message_dependencies
HMsgDep: i : index, MessageDependencies (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop IM
Hchannel: channel_authentication_prop IM Datatypes.id sender
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace (msg_dep_limited_equivocation_vlsm IM threshold full_message_dependencies sender) {| original_state := isX; state_annotation := `inhabitant |} (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender isX trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
HFullMsgDep: FullMessageDependencies message_dependencies full_message_dependencies
HMsgDep: i : index, MessageDependencies (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop IM
Hchannel: channel_authentication_prop IM Datatypes.id sender
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace (msg_dep_limited_equivocation_vlsm IM threshold full_message_dependencies sender) {| original_state := isX; state_annotation := `inhabitant |} (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender isX trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
HFullMsgDep: FullMessageDependencies message_dependencies full_message_dependencies
HMsgDep: i : index, MessageDependencies (IM i) message_dependencies
no_initial_messages_in_IM: no_initial_messages_in_IM_prop IM
Hchannel: channel_authentication_prop IM Datatypes.id sender
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

finite_valid_trace (msg_dep_limited_equivocation_vlsm IM threshold full_message_dependencies sender) {| original_state := equivocators_state_project IM initial_descriptors is; state_annotation := ∅ |} (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender (equivocators_state_project IM initial_descriptors is) trX)
by eapply @msg_dep_limited_fixed_equivocation; [| | | typeclasses eauto |..]. Qed. End sec_equivocators_projection_annotated_limited. Section sec_equivocators_projection_constrained_limited. Context `{FinSet message Cm} `{RelDecision _ _ (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)} (Limited : VLSM message := tracewise_limited_equivocation_vlsm_composition IM (Cv := Ci) threshold Datatypes.id sender) (Hsender_safety : sender_safety_alt_prop IM Datatypes.id sender) (message_dependencies : message -> Cm) (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies) .
If each of the components satisfy the message_dependencies_full_node_condition_property, then projections of valid traces for the composition of equivocators with limited state-equivocation and no message-equivocation are also valid traces for the composition of regular components with limited message-equivocation.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace Limited isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace Limited isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

(trX : list (composite_transition_item IM)) (initial_descriptors : equivocator_descriptors IM), let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace Limited isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

let isX := equivocators_state_project IM initial_descriptors is in let final_stateX := finite_trace_last isX trX in proper_equivocator_descriptors IM initial_descriptors is ∧ equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) ∧ equivocators_state_project IM final_descriptors final_state = final_stateX ∧ finite_valid_trace Limited isX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

finite_valid_trace_from Limited (equivocators_state_project IM initial_descriptors is) trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX
initial_state_prop (equivocators_state_project IM initial_descriptors is)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

finite_valid_trace_from Limited (equivocators_state_project IM initial_descriptors is) trX
by eapply @traces_exhibiting_limited_equivocation_are_valid; [| | typeclasses eauto | |].
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
is: composite_state (equivocator_IM IM)
tr: list (composite_transition_item (equivocator_IM IM))
final_state:= finite_trace_last is tr: state (composite_type (equivocator_IM IM))
Hproper: not_equivocating_equivocator_descriptors IM final_descriptors final_state
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm is tr
trX: list (composite_transition_item IM)
initial_descriptors: equivocator_descriptors IM
Hinitial_descriptors: proper_equivocator_descriptors IM initial_descriptors is
Hpr: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hlst_pr: equivocators_state_project IM final_descriptors (finite_trace_last is tr) = finite_trace_last (equivocators_state_project IM initial_descriptors is) trX
Hpr_limited: fixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trX

initial_state_prop (equivocators_state_project IM initial_descriptors is)
by destruct Hpr_limited as [equivs Hpr_limited]; apply Hpr_limited. Qed.
The above result formalized as a relation between the corresponding composite VLSMs. It yields a VLSM_partial_projection because for invalid equivocator_descriptors one might not be able to obtain a trace projection.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM

VLSM_partial_projection equivocators_limited_equivocations_vlsm Limited (equivocators_partial_trace_project IM final_descriptors)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM

VLSM_partial_projection equivocators_limited_equivocations_vlsm Limited (equivocators_partial_trace_project IM final_descriptors)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM

(sX : state equivocators_limited_equivocations_vlsm) (trX : list transition_item) (sY : state Limited) (trY : list transition_item), equivocators_partial_trace_project IM final_descriptors (sX, trX) = Some (sY, trY) → (s'X : state equivocators_limited_equivocations_vlsm) (preX : list transition_item), finite_trace_last s'X preX = sX → finite_valid_trace_from equivocators_limited_equivocations_vlsm s'X (preX ++ trX) → (s'Y : state Limited) (preY : list transition_item), equivocators_partial_trace_project IM final_descriptors (s'X, preX ++ trX) = Some (s'Y, preY ++ trY) ∧ finite_trace_last s'Y preY = sY
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
(sX : state equivocators_limited_equivocations_vlsm) (trX : list transition_item) (sY : state Limited) (trY : list transition_item), equivocators_partial_trace_project IM final_descriptors ( sX, trX) = Some (sY, trY) → finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited sY trY
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM

(sX : state equivocators_limited_equivocations_vlsm) (trX : list transition_item) (sY : state Limited) (trY : list transition_item), equivocators_partial_trace_project IM final_descriptors (sX, trX) = Some (sY, trY) → (s'X : state equivocators_limited_equivocations_vlsm) (preX : list transition_item), finite_trace_last s'X preX = sX → finite_valid_trace_from equivocators_limited_equivocations_vlsm s'X (preX ++ trX) → (s'Y : state Limited) (preY : list transition_item), equivocators_partial_trace_project IM final_descriptors (s'X, preX ++ trX) = Some (s'Y, preY ++ trY) ∧ finite_trace_last s'Y preY = sY
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
s_pre: state equivocators_limited_equivocations_vlsm
pre: list transition_item
Hs_lst: finite_trace_last s_pre pre = s
Hpre_tr: finite_valid_trace_from equivocators_limited_equivocations_vlsm s_pre (pre ++ tr)

(s'Y : state Limited) (preY : list transition_item), equivocators_partial_trace_project IM final_descriptors (s_pre, pre ++ tr) = Some (s'Y, preY ++ trX) ∧ finite_trace_last s'Y preY = sX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
s_pre: state equivocators_limited_equivocations_vlsm
pre: list transition_item
Hs_lst: finite_trace_last s_pre pre = s
Hpre_tr: finite_valid_trace_from equivocators_limited_equivocations_vlsm s_pre (pre ++ tr)

finite_constrained_trace_from FreeE s_pre (pre ++ tr)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
s_pre: state equivocators_limited_equivocations_vlsm
pre: list transition_item
Hs_lst: finite_trace_last s_pre pre = s
Hpre_tr: finite_valid_trace_from equivocators_limited_equivocations_vlsm s_pre (pre ++ tr)
HPreFree_pre_tr: finite_constrained_trace_from FreeE s_pre (pre ++ tr)
(s'Y : state Limited) (preY : list transition_item), equivocators_partial_trace_project IM final_descriptors ( s_pre, pre ++ tr) = Some (s'Y, preY ++ trX) ∧ finite_trace_last s'Y preY = sX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
s_pre: state equivocators_limited_equivocations_vlsm
pre: list transition_item
Hs_lst: finite_trace_last s_pre pre = s
Hpre_tr: finite_valid_trace_from equivocators_limited_equivocations_vlsm s_pre (pre ++ tr)

finite_constrained_trace_from FreeE s_pre (pre ++ tr)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
s_pre: state equivocators_limited_equivocations_vlsm
pre: list transition_item
Hs_lst: finite_trace_last s_pre pre = s
Hpre_tr: finite_valid_trace_from equivocators_limited_equivocations_vlsm s_pre (pre ++ tr)

VLSM_incl_part (constrained_vlsm_machine (free_composite_vlsm (equivocator_IM IM)) equivocators_limited_equivocations_constraint) (preloaded_vlsm_machine FreeE (λ _ : message, True))
by apply constrained_preloaded_incl.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
s_pre: state equivocators_limited_equivocations_vlsm
pre: list transition_item
Hs_lst: finite_trace_last s_pre pre = s
Hpre_tr: finite_valid_trace_from equivocators_limited_equivocations_vlsm s_pre (pre ++ tr)
HPreFree_pre_tr: finite_constrained_trace_from FreeE s_pre (pre ++ tr)

(s'Y : state Limited) (preY : list transition_item), equivocators_partial_trace_project IM final_descriptors (s_pre, pre ++ tr) = Some (s'Y, preY ++ trX) ∧ finite_trace_last s'Y preY = sX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
s_pre: state equivocators_limited_equivocations_vlsm
pre: list transition_item
Hs_lst: finite_trace_last s_pre pre = s
HPreFree_pre_tr: finite_constrained_trace_from FreeE s_pre (pre ++ tr)

(s'Y : state Limited) (preY : list transition_item), equivocators_partial_trace_project IM final_descriptors (s_pre, pre ++ tr) = Some (s'Y, preY ++ trX) ∧ finite_trace_last s'Y preY = sX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM

(s : state equivocators_limited_equivocations_vlsm) (tr : list transition_item) (sX : state Limited) (trX : list transition_item), equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX) → (s_pre : state equivocators_limited_equivocations_vlsm) (pre : list transition_item), finite_trace_last s_pre pre = s → finite_constrained_trace_from FreeE s_pre (pre ++ tr) → (s'Y : state Limited) (preY : list transition_item), equivocators_partial_trace_project IM final_descriptors (s_pre, pre ++ tr) = Some (s'Y, preY ++ trX) ∧ finite_trace_last s'Y preY = sX
by apply equivocators_partial_trace_project_extends_left.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM

(sX : state equivocators_limited_equivocations_vlsm) (trX : list transition_item) (sY : state Limited) (trY : list transition_item), equivocators_partial_trace_project IM final_descriptors (sX, trX) = Some (sY, trY) → finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited sY trY
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm s tr

finite_valid_trace Limited sX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm s tr
Hnot_equiv: not_equivocating_equivocator_descriptors IM final_descriptors (finite_trace_last s tr)
initial_descriptors: equivocator_descriptors IM
Htr_project: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hs_project: equivocators_state_project IM initial_descriptors s = sX

finite_valid_trace Limited sX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm s tr
Hnot_equiv: not_equivocating_equivocator_descriptors IM final_descriptors (finite_trace_last s tr)
initial_descriptors: equivocator_descriptors IM
Htr_project: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hs_project: equivocators_state_project IM initial_descriptors s = sX
_trX: list (composite_transition_item IM)
_initial_descriptors: equivocator_descriptors IM
_Htr_project: equivocators_trace_project IM final_descriptors tr = Some (_trX, _initial_descriptors)
HtrX: finite_valid_trace Limited (equivocators_state_project IM _initial_descriptors s) _trX

finite_valid_trace Limited sX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
final_descriptors: equivocator_descriptors IM
s: state equivocators_limited_equivocations_vlsm
tr: list transition_item
sX: state Limited
trX: list transition_item
Hpr_tr: equivocators_partial_trace_project IM final_descriptors (s, tr) = Some (sX, trX)
Htr: finite_valid_trace equivocators_limited_equivocations_vlsm s tr
Hnot_equiv: not_equivocating_equivocator_descriptors IM final_descriptors (finite_trace_last s tr)
initial_descriptors: equivocator_descriptors IM
Htr_project: equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors)
Hs_project: equivocators_state_project IM initial_descriptors s = sX
_trX: list (composite_transition_item IM)
_initial_descriptors: equivocator_descriptors IM
_Htr_project: Some (trX, initial_descriptors) = Some (_trX, _initial_descriptors)
HtrX: finite_valid_trace Limited (equivocators_state_project IM _initial_descriptors s) _trX

finite_valid_trace Limited sX trX
by inversion _Htr_project; subst. Qed.
In the case of using the original machine copy for projecting each component, we are guaranteed to obtain a trace projection for each trace, hence the relation above strengthens to a VLSM_projection.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies

VLSM_projection equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies

VLSM_projection equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item

finite_valid_trace_from equivocators_limited_equivocations_vlsm sX trX → equivocators_total_state_project IM (finite_trace_last sX trX) = finite_trace_last (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item

finite_valid_trace_from equivocators_limited_equivocations_vlsm sX trX → equivocators_total_state_project IM (finite_trace_last sX trX) = finite_trace_last (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace_from equivocators_limited_equivocations_vlsm sX trX

equivocators_total_state_project IM (finite_trace_last sX trX) = finite_trace_last (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace_from equivocators_limited_equivocations_vlsm sX trX

finite_valid_trace_from (preloaded_with_all_messages_vlsm (free_composite_vlsm (equivocator_IM IM))) sX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item

finite_valid_trace_from equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace_from (preloaded_with_all_messages_vlsm (free_composite_vlsm (equivocator_IM IM))) sX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item

VLSM_incl_part (constrained_vlsm_machine (free_composite_vlsm (equivocator_IM IM)) equivocators_limited_equivocations_constraint) (preloaded_vlsm_machine (free_composite_vlsm (equivocator_IM IM)) (λ _ : message, True))
by apply constrained_preloaded_incl.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item

finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX

finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX

finite_constrained_trace FreeE sX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX

finite_constrained_trace FreeE sX trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX

VLSM_incl_part (constrained_vlsm_machine (free_composite_vlsm (equivocator_IM IM)) equivocators_limited_equivocations_constraint) (preloaded_vlsm_machine FreeE (λ _ : message, True))
by apply constrained_preloaded_incl.
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX

finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: equivocators_partial_trace_project IM (zero_descriptor IM) ( sX, trX) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX) → finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: equivocators_partial_trace_project IM (zero_descriptor IM) ( sX, trX) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX) → finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

equivocators_partial_trace_project IM (zero_descriptor IM) (sX, trX) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: equivocators_partial_trace_project IM (zero_descriptor IM) ( sX, trX) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX) → finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

equivocators_partial_trace_project IM (zero_descriptor IM) (sX, trX) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: equivocators_partial_trace_project IM (zero_descriptor IM) ( sX, trX) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX) → finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

(if decide (not_equivocating_equivocator_descriptors IM (zero_descriptor IM) (finite_trace_last sX trX)) then match equivocators_trace_project IM (zero_descriptor IM) trX with | Some (trX, initial_descriptors) => Some (equivocators_state_project IM initial_descriptors sX, trX) | None => None end else None) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: equivocators_partial_trace_project IM (zero_descriptor IM) ( sX, trX) = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX) → finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

match equivocators_trace_project IM (zero_descriptor IM) trX with | Some (trX, initial_descriptors) => Some (equivocators_state_project IM initial_descriptors sX, trX) | None => None end = Some (equivocators_state_project IM (zero_descriptor IM) sX, equivocators_total_trace_project IM trX)
by rewrite (equivocators_total_trace_project_characterization IM (proj1 Hpre_tr)).
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

finite_valid_trace Limited (equivocators_total_state_project IM sX) (pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX)
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
tr: list transition_item
Heqtr: tr = pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX

finite_valid_trace Limited (equivocators_total_state_project IM sX) tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
tr: list transition_item
Heqtr: tr = pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX

equivocators_total_trace_project IM trX = tr
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

equivocators_total_trace_project IM trX = pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX
message, index: Type
IM: index → VLSM message
H: i : index, HasBeenSentCapability (IM i)
H0: i : index, HasBeenReceivedCapability (IM i)
threshold: R
Ci: Type
Hm: Measurable index
H1: ElemOf index Ci
H2: Empty Ci
H3: Singleton index Ci
H4: Union Ci
H5: Intersection Ci
H6: Difference Ci
H7: Elements index Ci
EqDecision0: EqDecision index
H8: FinSet index Ci
H9: ReachableThreshold index Ci threshold
H10: finite.Finite index
Free:= free_composite_vlsm IM: VLSM message
sender: message → option index
HBE:= equivocating_indices_BasicEquivocation IM threshold: BasicEquivocation (composite_state (equivocator_IM IM)) index Ci threshold
FreeE:= free_composite_vlsm (equivocator_IM IM): VLSM message
Cm: Type
H11: ElemOf message Cm
H12: Empty Cm
H13: Singleton message Cm
H14: Union Cm
H15: Intersection Cm
H16: Difference Cm
H17: Elements message Cm
EqDecision1: EqDecision message
H18: FinSet message Cm
H19: RelDecision (is_equivocating_tracewise_no_has_been_sent IM Datatypes.id sender)
Limited:= tracewise_limited_equivocation_vlsm_composition IM threshold Datatypes.id sender: VLSM message
Hsender_safety: sender_safety_alt_prop IM Datatypes.id sender
message_dependencies: message → Cm
Hfull: i : index, message_dependencies_full_node_condition_prop (IM i) message_dependencies
sX: state equivocators_limited_equivocations_vlsm
trX: list transition_item
HtrX: finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)
Hpre_tr: finite_constrained_trace FreeE sX trX
Hsim: finite_valid_trace equivocators_limited_equivocations_vlsm sX trX → finite_valid_trace Limited (equivocators_state_project IM (zero_descriptor IM) sX) (equivocators_total_trace_project IM trX)

pre_VLSM_projection_finite_trace_project equivocators_limited_equivocations_vlsm Limited (equivocators_total_label_project IM) (equivocators_total_state_project IM) trX = equivocators_total_trace_project IM trX
by apply (equivocators_total_VLSM_projection_finite_trace_project IM (proj1 Hpre_tr)). Qed. End sec_equivocators_projection_constrained_limited. End sec_limited_state_equivocation.