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.From VLSM.Core Require Import Equivocators.EquivocatorsComposition. From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections. From VLSM.Core Require Import Equivocators.FixedEquivocation.
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 esinitial_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 esinitial_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 esinitial_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 esinitial_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 esinitial_state_prop (default (equivocator_state_zero es) (equivocator_state_project es n))by eapply equivocator_vlsm_initial_state_preservation_rev. Qed.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 esinitial_state_prop (default (equivocator_state_zero es) (Some esn))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 esinitial_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.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 esinitial_state_prop (equivocators_state_project IM eqv_descriptors es)
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 messageVLSM_incl equivocators_limited_equivocations_vlsm FreeEby apply VLSM_incl_constrained_vlsm. Qed.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 messageVLSM_incl equivocators_limited_equivocations_vlsm FreeE
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 messageVLSM_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.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 messageVLSM_incl (preloaded_with_all_messages_vlsm equivocators_limited_equivocations_vlsm) (preloaded_with_all_messages_vlsm FreeE)
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 messageVLSM_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 messageVLSM_incl equivocators_limited_equivocations_vlsm (equivocators_no_equivocations_vlsm IM)by intros l [s om] (_ & _ & _ & Hc & _). Qed.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 messageinput_valid_constraint_subsumption (free_composite_vlsm (equivocator_IM IM)) equivocators_limited_equivocations_constraint (equivocators_no_equivocations_constraint IM)
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 snot_heavy smessage, 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 snot_heavy smessage, 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 smessage, 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 smessage, 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 smessage, 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 smessage, 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 isnot_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)%Rmessage, 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)%Rmessage, 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)%Rmessage, 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)%Rby 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
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)%Rby replace s with (fst (composite_transition (equivocator_IM IM) l (s0, oim))); [done |] ; cbn in *; rewrite Ht. Qed.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
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_itemfinite_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 trmessage, 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_itemfinite_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 trmessage, 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 trfinite_valid_trace_init_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators s))) is s trmessage, 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 trfinite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators s))) is s trmessage, 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 trmessage, 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) ⊆ equivocatingfinite_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) ⊆ equivocatingfinite_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) ⊆ equivocatingfinite_valid_trace_from_to (equivocators_fixed_equivocations_vlsm IM equivocating) si 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: state equivocators_limited_equivocations_vlsm
Hsi: initial_state_prop si
equivocating: list index
Hincl: elements (equivocating_validators si) ⊆ equivocatingvalid_state_prop (equivocators_fixed_equivocations_vlsm IM equivocating) simessage, 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) ⊆ equivocatingfinite_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) ⊆ equivocatingfinite_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) ⊆ equivocatingelements (equivocating_validators s) ⊆ equivocatingmessage, 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 trfinite_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) ⊆ equivocatingelements (equivocating_validators s) ⊆ equivocatingmessage, 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) ⊆ equivocatingelements (equivocating_validators s) ⊆ equivocatingmessage, 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) sfelements (equivocating_validators s) ⊆ equivocatingmessage, 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) sfelements (equivocating_validators s) ⊆ equivocatingmessage, 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) sfelements (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 sx ∈ equivocating_validators sfby 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)
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 sx ∈ equivocating_indices IM (enum index) smessage, 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 trfinite_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 trfinite_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 trfinite_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 trinput_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) sinput_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) sinput_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) soption_valid_message_prop (equivocators_fixed_equivocations_vlsm IM equivocating) iommessage, 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) sstate_has_fixed_equivocation IM equivocating (composite_transition (equivocator_IM IM) l (s, iom)).1message, 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) soption_valid_message_prop (equivocators_fixed_equivocations_vlsm IM equivocating) iommessage, 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) soption_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) soption_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
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) soption_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
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) sstate_has_fixed_equivocation IM equivocating (composite_transition (equivocator_IM IM) l (s, iom)).1message, 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) sstate_has_fixed_equivocation IM equivocating (sf, oom).1message, 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) sequivocating_indices IM (enum index) (sf, oom).1 ⊆ equivocatingby intros x Hx; apply elem_of_elements, equivocating_indices_equivocating_validators, elem_of_list_to_set. Qed.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) sequivocating_indices IM (enum index) (sf, oom).1 ⊆ elements (equivocating_validators sf)
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 trXmessage, 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 trXmessage, 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 trXmessage, 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 trXmessage, 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 trXmessage, 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 trXmessage, 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 trmessage, 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 trXby 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)proper_fixed_equivocator_descriptors IM (equivocating_validators (finite_trace_last is tr)) final_descriptors (finite_trace_last 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)finite_valid_trace (equivocators_fixed_equivocations_vlsm IM (elements (equivocating_validators (finite_trace_last is tr)))) is trmessage, 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 trXmessage, 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) trXlet 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 trXmessage, 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) trXfixed_limited_equivocation_prop IM threshold Datatypes.id (equivocators_state_project IM initial_descriptors is) trXmessage, 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) trXmessage, 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)%Rmessage, 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) trXfinite_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) trXmessage, 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)%Rmessage, 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)%Rby 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: 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))%Rmessage, 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) trXfinite_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) trXmessage, 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) trXfinite_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) trXmessage, 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) trXinput_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) trXstrong_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: messagefixed_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 mmessage, 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) mfixed_equivocation IM (set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))) s mmessage, 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: messagecan_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) mmessage, 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: messageelements (equivocating_validators (finite_trace_last is tr)) ⊆ elements (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) .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: messageequivocating_validators (finite_trace_last is tr) ⊆ set_map Datatypes.id (equivocating_validators (finite_trace_last is tr))
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) trXlet 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)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) .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) trXfinite_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)
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 trXmessage, 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 trXmessage, 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 trXmessage, 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) trXlet 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 trXmessage, 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) trXfinite_valid_trace_from Limited (equivocators_state_project IM initial_descriptors is) trXmessage, 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) trXinitial_state_prop (equivocators_state_project IM initial_descriptors is)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) trXfinite_valid_trace_from Limited (equivocators_state_project IM initial_descriptors is) trXby destruct Hpr_limited as [equivs Hpr_limited]; apply Hpr_limited. Qed.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) trXinitial_state_prop (equivocators_state_project IM initial_descriptors is)
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 IMVLSM_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 IMVLSM_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 = sYmessage, 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 trYmessage, 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 = sYmessage, 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 = sXmessage, 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 = sXmessage, 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)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)VLSM_incl_part (constrained_vlsm_machine (free_composite_vlsm (equivocator_IM IM)) equivocators_limited_equivocations_constraint) (preloaded_vlsm_machine FreeE (λ _ : message, True))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 = sXmessage, 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 = sXby 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∀ (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 = sXmessage, 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 trYmessage, 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 trfinite_valid_trace Limited sX trXmessage, 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 = sXfinite_valid_trace Limited sX trXmessage, 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) _trXfinite_valid_trace Limited sX trXby inversion _Htr_project; subst. Qed.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) _trXfinite_valid_trace Limited sX trX
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_dependenciesVLSM_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_dependenciesVLSM_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_itemfinite_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_itemfinite_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_itemfinite_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 trXequivocators_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 trXfinite_valid_trace_from (preloaded_with_all_messages_vlsm (free_composite_vlsm (equivocator_IM IM))) sX trXmessage, 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_itemfinite_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 trXby 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_itemVLSM_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))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_itemfinite_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 trXfinite_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 trXfinite_constrained_trace FreeE sX trXmessage, 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 trXfinite_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 trXfinite_constrained_trace FreeE sX trXby 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 trXVLSM_incl_part (constrained_vlsm_machine (free_composite_vlsm (equivocator_IM IM)) equivocators_limited_equivocations_constraint) (preloaded_vlsm_machine FreeE (λ _ : message, True))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 trXfinite_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)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: 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)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) trXfinite_valid_trace Limited (equivocators_total_state_project IM sX) trmessage, 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) trXequivocators_total_trace_project IM trX = trmessage, 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) trXby apply (equivocators_total_VLSM_projection_finite_trace_project IM (proj1 Hpre_tr)). Qed. End sec_equivocators_projection_constrained_limited. End sec_limited_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
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