From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude finite.
From Coq Require Import FinFun Rdefinitions.
From VLSM.Lib Require Import Preamble ListExtras StdppListSet Measurable.
From VLSM.Core Require Import VLSM Composition ProjectionTraces.
From VLSM.Core Require Import Equivocation.
From VLSM.Lib Require Import Preamble StdppExtras.

Core: VLSM Trace-Wise Equivocation

In this module, we define a more precise notion of message equivocation, based on analyzing (all) traces leading to a state. Although in some cases we might be able to actually compute this, its purpose is more to identify the ideal notion of detectable equivocation which would be used to establish the connection between limited (observed) message equivocation and limited state equivocation.

Section sec_tracewise_equivocation.

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

An item is equivocating in a trace containing it if it receives a message which has not been previously sent in that trace.

Definition item_equivocating_in_trace
  (item : composite_transition_item IM)
  (tr : list (composite_transition_item IM))
  : Prop
  := from_option (fun m => ~ trace_has_message (field_selector output) m tr) False (input item).

#[local] Instance item_equivocating_in_trace_dec : RelDecision item_equivocating_in_trace.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
RelDecision item_equivocating_in_trace
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
RelDecision item_equivocating_in_trace
  intros item tr.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
item: composite_transition_item IM
tr: list (composite_transition_item IM)
Decision (item_equivocating_in_trace item tr)
  destruct item.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label (composite_type IM)
input: option message
destination: state (composite_type IM)
output: option message
tr: list (composite_transition_item IM)
Decision
  (item_equivocating_in_trace
     {|
       l := l;
       input := input;
       destination := destination;
       output := output
     |} tr) destruct input as [m |]; [| by right; itauto].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label (composite_type IM)
m: message
destination: state (composite_type IM)
output: option message
tr: list (composite_transition_item IM)
Decision
  (item_equivocating_in_trace
     {|
       l := l;
       input := Some m;
       destination := destination;
       output := output
     |} tr)
  unfold item_equivocating_in_trace, trace_has_message, field_selector; cbn.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label (composite_type IM)
m: message
destination: state (composite_type IM)
output: option message
tr: list (composite_transition_item IM)
Decision
  (¬ Exists
       (λ item : transition_item,
          VLSM.output item = Some m) tr)
  by typeclasses eauto.
Qed.

Given a trace, we can precisely identify the validators equivocating in that trace based on identifying every item_equivocating_in_trace.

Definition equivocating_senders_in_trace
  (tr : list (composite_transition_item IM))
  : set validator
  :=
  let decompositions := one_element_decompositions tr in
  let test := (fun d => match d with (pre, item, _) =>
      item_equivocating_in_trace item pre
    end) in
  let equivocating_items :=
    map (fun d => match d with (_, item, _) => item end)
      (filter test decompositions) in
  let equivocating_messages := omap input equivocating_items in
  let equivocating_senders := omap sender equivocating_messages in
  remove_dups equivocating_senders.

Lemma no_input_no_equivocating_senders_in_trace tr
  (Hinput_none : forall item, item ∈ tr -> input item = None)
  : equivocating_senders_in_trace tr = [].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
equivocating_senders_in_trace tr = []
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
equivocating_senders_in_trace tr = []
  apply elem_of_nil_inv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
∀ x : validator, x ∉ equivocating_senders_in_trace tr
  intros v Hv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
v: validator
Hv: v ∈ equivocating_senders_in_trace tr
False
  unfold equivocating_senders_in_trace in Hv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
v: validator
Hv: v
∈ remove_dups
    (omap sender
       (omap input
          (map
             (λ d : list
                      (composite_transition_item
                      IM) *
                    composite_transition_item IM *
                    list
                      (composite_transition_item
                      IM),
                let (y, _) := d in
                let (_, item) := y in item)
             (filter
                (λ d : 
                    list
                      (composite_transition_item
                      IM) *
                    composite_transition_item IM *
                    list
                      (composite_transition_item
                      IM),
                   let (y, _) := d in
                   let (pre, item) := y in
                   item_equivocating_in_trace
                     item pre)
                (one_element_decompositions tr)))))
False
  rewrite elem_of_remove_dups in Hv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
v: validator
Hv: v
∈ omap sender
    (omap input
       (map
          (λ d : list
                   (composite_transition_item IM) *
                 composite_transition_item IM *
                 list
                   (composite_transition_item IM),
             let (y, _) := d in
             let (_, item) := y in item)
          (filter
             (λ d : list
                      (composite_transition_item
                      IM) *
                    composite_transition_item IM *
                    list
                      (composite_transition_item
                      IM),
                let (y, _) := d in
                let (pre, item) := y in
                item_equivocating_in_trace item
                  pre)
             (one_element_decompositions tr))))
False
  apply elem_of_list_omap in Hv as [msg [Hmsg Hv]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
v: validator
msg: message
Hmsg: msg
∈ omap input
    (map
       (λ d : list
                (composite_transition_item IM) *
              composite_transition_item IM *
              list
                (composite_transition_item IM),
          let (y, _) := d in
          let (_, item) := y in item)
       (filter
          (λ d : list
                   (composite_transition_item
                      IM) *
                 composite_transition_item IM *
                 list
                   (composite_transition_item
                      IM),
             let (y, _) := d in
             let (pre, item) := y in
             item_equivocating_in_trace item
               pre)
          (one_element_decompositions tr)))
Hv: sender msg = Some v
False
  apply elem_of_list_omap in Hmsg as [item [Hitem Hmsg]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
v: validator
msg: message
item: transition_item
Hitem: item
∈ map
    (λ d : list (composite_transition_item IM) *
           composite_transition_item IM *
           list (composite_transition_item IM),
       let (y, _) := d in
       let (_, item) := y in item)
    (filter
       (λ d : list
                (composite_transition_item IM) *
              composite_transition_item IM *
              list
                (composite_transition_item IM),
          let (y, _) := d in
          let (pre, item) := y in
          item_equivocating_in_trace item pre)
       (one_element_decompositions tr))
Hmsg: input item = Some msg
Hv: sender msg = Some v
False
  apply elem_of_list_fmap in Hitem as [((pre, _item), _suf) [Heq_item Hitem]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
v: validator
msg: message
item: transition_item
pre: list (composite_transition_item IM)
_item: composite_transition_item IM
_suf: list (composite_transition_item IM)
Heq_item: item = _item
Hitem: (pre, _item, _suf)
∈ filter
    (λ d : list (composite_transition_item IM) *
           composite_transition_item IM *
           list (composite_transition_item IM),
       let (y, _) := d in
       let (pre, item) := y in
       item_equivocating_in_trace item pre)
    (one_element_decompositions tr)
Hmsg: input item = Some msg
Hv: sender msg = Some v
False
  apply elem_of_list_filter, proj2, elem_of_one_element_decompositions in Hitem.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
Hinput_none: ∀ item : transition_item,
  item ∈ tr → input item = None
v: validator
msg: message
item: transition_item
pre: list (composite_transition_item IM)
_item: composite_transition_item IM
_suf: list (composite_transition_item IM)
Heq_item: item = _item
Hitem: pre ++ [_item] ++ _suf = tr
Hmsg: input item = Some msg
Hv: sender msg = Some v
False
  subst tr _item.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
pre, _suf: list (composite_transition_item IM)
item: transition_item
Hinput_none: ∀ item0 : transition_item,
  item0 ∈ pre ++ [item] ++ _suf
  → input item0 = None
v: validator
msg: message
Hmsg: input item = Some msg
Hv: sender msg = Some v
False
  specialize (Hinput_none item).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
pre, _suf: list (composite_transition_item IM)
item: transition_item
Hinput_none: item ∈ pre ++ [item] ++ _suf
→ input item = None
v: validator
msg: message
Hmsg: input item = Some msg
Hv: sender msg = Some v
False
  spec Hinput_none; [| by congruence].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
pre, _suf: list (composite_transition_item IM)
item: transition_item
Hinput_none: item ∈ pre ++ [item] ++ _suf
→ input item = None
v: validator
msg: message
Hmsg: input item = Some msg
Hv: sender msg = Some v
item ∈ pre ++ [item] ++ _suf
  by apply elem_of_app; right; apply elem_of_app; do 2 left.
Qed.

Lemma elem_of_equivocating_senders_in_trace
  (tr : list (composite_transition_item IM))
  (v : validator)
  : v ∈ equivocating_senders_in_trace tr <->
    exists (m : message),
    (sender m = Some v) /\
    equivocation_in_trace (free_composite_vlsm IM) m tr.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
v ∈ equivocating_senders_in_trace tr
↔ (∃ m : message,
     sender m = Some v
     ∧ equivocation_in_trace (free_composite_vlsm IM)
         m tr)
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
v ∈ equivocating_senders_in_trace tr
↔ (∃ m : message,
     sender m = Some v
     ∧ equivocation_in_trace (free_composite_vlsm IM)
         m tr)
  unfold equivocating_senders_in_trace.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
v
∈ remove_dups
    (omap sender
       (omap input
          (map
             (λ d : list
                      (composite_transition_item IM) *
                    composite_transition_item IM *
                    list
                      (composite_transition_item IM),
                let (y, _) := d in
                let (_, item) := y in item)
             (filter
                (λ d : list
                         (composite_transition_item IM) *
                       composite_transition_item IM *
                       list
                         (composite_transition_item IM),
                   let (y, _) := d in
                   let (pre, item) := y in
                   item_equivocating_in_trace item pre)
                (one_element_decompositions tr)))))
↔ (∃ m : message,
     sender m = Some v
     ∧ equivocation_in_trace (free_composite_vlsm IM)
         m tr)
  rewrite elem_of_remove_dups, elem_of_list_omap.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
(∃ x : message,
   x
   ∈ omap input
       (map
          (λ d : list (composite_transition_item IM) *
                 composite_transition_item IM *
                 list (composite_transition_item IM),
             let (y, _) := d in
             let (_, item) := y in item)
          (filter
             (λ d : list
                      (composite_transition_item IM) *
                    composite_transition_item IM *
                    list
                      (composite_transition_item IM),
                let (y, _) := d in
                let (pre, item) := y in
                item_equivocating_in_trace item pre)
             (one_element_decompositions tr)))
   ∧ sender x = Some v)
↔ (∃ m : message,
     sender m = Some v
     ∧ equivocation_in_trace (free_composite_vlsm IM)
         m tr)
  setoid_rewrite elem_of_list_omap.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
(∃ x : message,
   (∃ x0 : transition_item,
      x0
      ∈ map
          (λ d : list (composite_transition_item IM) *
                 composite_transition_item IM *
                 list (composite_transition_item IM),
             let (y, _) := d in
             let (_, item) := y in item)
          (filter
             (λ d : list
                      (composite_transition_item IM) *
                    composite_transition_item IM *
                    list
                      (composite_transition_item IM),
                let (y, _) := d in
                let (pre, item) := y in
                item_equivocating_in_trace item pre)
             (one_element_decompositions tr))
      ∧ input x0 = Some x) ∧ sender x = Some v)
↔ (∃ m : message,
     sender m = Some v
     ∧ equivocation_in_trace (free_composite_vlsm IM)
         m tr)
  setoid_rewrite elem_of_list_fmap.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
(∃ x : message,
   (∃ x0 : transition_item,
      (∃ y : list (composite_transition_item IM) *
             composite_transition_item IM *
             list (composite_transition_item IM),
         x0 =
         (let (y0, _) := y in
          let (_, item) := y0 in item)
         ∧ y
           ∈ filter
               (λ d : list
                        (composite_transition_item IM) *
                      composite_transition_item IM *
                      list
                        (composite_transition_item IM),
                  let (y0, _) := d in
                  let (pre, item) := y0 in
                  item_equivocating_in_trace item pre)
               (one_element_decompositions tr))
      ∧ input x0 = Some x) ∧ sender x = Some v)
↔ (∃ m : message,
     sender m = Some v
     ∧ equivocation_in_trace (free_composite_vlsm IM)
         m tr)
  split.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
(∃ x : message,
   (∃ x0 : transition_item,
      (∃ y : list (composite_transition_item IM) *
             composite_transition_item IM *
             list (composite_transition_item IM),
         x0 =
         (let (y0, _) := y in
          let (_, item) := y0 in item)
         ∧ y
           ∈ filter
               (λ d : list
                        (composite_transition_item IM) *
                      composite_transition_item IM *
                      list
                        (composite_transition_item IM),
                  let (y0, _) := d in
                  let (pre, item) := y0 in
                  item_equivocating_in_trace item pre)
               (one_element_decompositions tr))
      ∧ input x0 = Some x) ∧ sender x = Some v)
→ ∃ m : message,
    sender m = Some v
    ∧ equivocation_in_trace (free_composite_vlsm IM) m
        tr
message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
(∃ m : message,
   sender m = Some v
   ∧ equivocation_in_trace 
       (free_composite_vlsm IM) m tr)
→ ∃ x : message,
    (∃ x0 : transition_item,
       (∃ y : list (composite_transition_item IM) *
              composite_transition_item IM *
              list (composite_transition_item IM),
          x0 =
          (let (y0, _) := y in
           let (_, item) := y0 in item)
          ∧ y
            ∈ filter
                (λ d : 
                    list
                      (composite_transition_item IM) *
                    composite_transition_item IM *
                    list
                      (composite_transition_item IM),
                   let (y0, _) := d in
                   let (pre, item) := y0 in
                   item_equivocating_in_trace item pre)
                (one_element_decompositions tr))
       ∧ input x0 = Some x) ∧ 
    sender x = Some v
  -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
(∃ x : message,
   (∃ x0 : transition_item,
      (∃ y : list (composite_transition_item IM) *
             composite_transition_item IM *
             list (composite_transition_item IM),
         x0 =
         (let (y0, _) := y in
          let (_, item) := y0 in item)
         ∧ y
           ∈ filter
               (λ d : list
                        (composite_transition_item IM) *
                      composite_transition_item IM *
                      list
                        (composite_transition_item IM),
                  let (y0, _) := d in
                  let (pre, item) := y0 in
                  item_equivocating_in_trace item pre)
               (one_element_decompositions tr))
      ∧ input x0 = Some x) ∧ sender x = Some v)
→ ∃ m : message,
    sender m = Some v
    ∧ equivocation_in_trace (free_composite_vlsm IM) m
        tr intros [im [[item [[((prefix, _item), suffix) [Heq_item Hfilter]] Hinput]] Hsender]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix: list (composite_transition_item IM)
_item: composite_transition_item IM
suffix: list (composite_transition_item IM)
Heq_item: item = _item
Hfilter: (prefix, _item, suffix)
∈ filter
    (λ d : list
             (composite_transition_item IM) *
           composite_transition_item IM *
           list
             (composite_transition_item IM),
       let (y, _) := d in
       let (pre, item) := y in
       item_equivocating_in_trace item pre)
    (one_element_decompositions tr)
Hinput: input item = Some im
Hsender: sender im = Some v
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace (free_composite_vlsm IM) m
      tr
    apply elem_of_list_filter in Hfilter.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix: list (composite_transition_item IM)
_item: composite_transition_item IM
suffix: list (composite_transition_item IM)
Heq_item: item = _item
Hfilter: item_equivocating_in_trace _item prefix
∧ (prefix, _item, suffix)
  ∈ one_element_decompositions tr
Hinput: input item = Some im
Hsender: sender im = Some v
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace (free_composite_vlsm IM) m
      tr
    destruct Hfilter as [Heqv Hdec].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix: list (composite_transition_item IM)
_item: composite_transition_item IM
suffix: list (composite_transition_item IM)
Heq_item: item = _item
Heqv: item_equivocating_in_trace _item prefix
Hdec: (prefix, _item, suffix)
∈ one_element_decompositions tr
Hinput: input item = Some im
Hsender: sender im = Some v
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace (free_composite_vlsm IM) m
      tr
    subst _item.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: (prefix, item, suffix)
∈ one_element_decompositions tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace (free_composite_vlsm IM) m
      tr
    exists im.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: (prefix, item, suffix)
∈ one_element_decompositions tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
sender im = Some v
∧ equivocation_in_trace (free_composite_vlsm IM) im tr split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: (prefix, item, suffix)
∈ one_element_decompositions tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
equivocation_in_trace (free_composite_vlsm IM) im tr
    exists prefix, item, suffix.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: (prefix, item, suffix)
∈ one_element_decompositions tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
tr = prefix ++ item :: suffix
∧ input item = Some im
  ∧ ¬ trace_has_message (field_selector output) im
        prefix
    apply elem_of_one_element_decompositions in Hdec.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: prefix ++ [item] ++ suffix = tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
tr = prefix ++ item :: suffix
∧ input item = Some im
  ∧ ¬ trace_has_message (field_selector output) im
        prefix simpl in Hdec.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: prefix ++ item :: suffix = tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
tr = prefix ++ item :: suffix
∧ input item = Some im
  ∧ ¬ trace_has_message (field_selector output) im
        prefix
    split; [by subst |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: prefix ++ item :: suffix = tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
input item = Some im
∧ ¬ trace_has_message (field_selector output) im
      prefix
    split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
item: transition_item
prefix, suffix: list (composite_transition_item IM)
Hdec: prefix ++ item :: suffix = tr
Heqv: item_equivocating_in_trace item prefix
Hinput: input item = Some im
Hsender: sender im = Some v
¬ trace_has_message (field_selector output) im prefix
    by unfold item_equivocating_in_trace in Heqv; rewrite Hinput in Heqv.
  -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
(∃ m : message,
   sender m = Some v
   ∧ equivocation_in_trace (free_composite_vlsm IM) m
       tr)
→ ∃ x : message,
    (∃ x0 : transition_item,
       (∃ y : list (composite_transition_item IM) *
              composite_transition_item IM *
              list (composite_transition_item IM),
          x0 =
          (let (y0, _) := y in
           let (_, item) := y0 in item)
          ∧ y
            ∈ filter
                (λ d : list
                         (composite_transition_item IM) *
                       composite_transition_item IM *
                       list
                         (composite_transition_item IM),
                   let (y0, _) := d in
                   let (pre, item) := y0 in
                   item_equivocating_in_trace item pre)
                (one_element_decompositions tr))
       ∧ input x0 = Some x) ∧ sender x = Some v intros [im [Hsender [prefix [item [suffix [Heq_tr [Hinput Heqv]]]]]]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
∃ x : message,
  (∃ x0 : transition_item,
     (∃ y : list (composite_transition_item IM) *
            composite_transition_item IM *
            list (composite_transition_item IM),
        x0 =
        (let (y0, _) := y in
         let (_, item) := y0 in item)
        ∧ y
          ∈ filter
              (λ d : list
                       (composite_transition_item IM) *
                     composite_transition_item IM *
                     list
                       (composite_transition_item IM),
                 let (y0, _) := d in
                 let (pre, item) := y0 in
                 item_equivocating_in_trace item pre)
              (one_element_decompositions tr))
     ∧ input x0 = Some x) ∧ sender x = Some v
    exists im.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
(∃ x : transition_item,
   (∃ y : list (composite_transition_item IM) *
          composite_transition_item IM *
          list (composite_transition_item IM),
      x =
      (let (y0, _) := y in let (_, item) := y0 in item)
      ∧ y
        ∈ filter
            (λ d : list (composite_transition_item IM) *
                   composite_transition_item IM *
                   list (composite_transition_item IM),
               let (y0, _) := d in
               let (pre, item) := y0 in
               item_equivocating_in_trace item pre)
            (one_element_decompositions tr))
   ∧ input x = Some im) ∧ sender im = Some v split; [| done].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
∃ x : transition_item,
  (∃ y : list (composite_transition_item IM) *
         composite_transition_item IM *
         list (composite_transition_item IM),
     x =
     (let (y0, _) := y in let (_, item) := y0 in item)
     ∧ y
       ∈ filter
           (λ d : list (composite_transition_item IM) *
                  composite_transition_item IM *
                  list (composite_transition_item IM),
              let (y0, _) := d in
              let (pre, item) := y0 in
              item_equivocating_in_trace item pre)
           (one_element_decompositions tr))
  ∧ input x = Some im exists item.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
(∃ y : list (composite_transition_item IM) *
       composite_transition_item IM *
       list (composite_transition_item IM),
   item =
   (let (y0, _) := y in let (_, item) := y0 in item)
   ∧ y
     ∈ filter
         (λ d : list (composite_transition_item IM) *
                composite_transition_item IM *
                list (composite_transition_item IM),
            let (y0, _) := d in
            let (pre, item) := y0 in
            item_equivocating_in_trace item pre)
         (one_element_decompositions tr))
∧ input item = Some im
    split; [| done].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
∃ y : list (composite_transition_item IM) *
      composite_transition_item IM *
      list (composite_transition_item IM),
  item =
  (let (y0, _) := y in let (_, item) := y0 in item)
  ∧ y
    ∈ filter
        (λ d : list (composite_transition_item IM) *
               composite_transition_item IM *
               list (composite_transition_item IM),
           let (y0, _) := d in
           let (pre, item) := y0 in
           item_equivocating_in_trace item pre)
        (one_element_decompositions tr) exists ((prefix, item), suffix).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
item = item
∧ (prefix, item, suffix)
  ∈ filter
      (λ d : list (composite_transition_item IM) *
             composite_transition_item IM *
             list (composite_transition_item IM),
         let (y, _) := d in
         let (pre, item) := y in
         item_equivocating_in_trace item pre)
      (one_element_decompositions tr)
    split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
(prefix, item, suffix)
∈ filter
    (λ d : list (composite_transition_item IM) *
           composite_transition_item IM *
           list (composite_transition_item IM),
       let (y, _) := d in
       let (pre, item) := y in
       item_equivocating_in_trace item pre)
    (one_element_decompositions tr)
    apply elem_of_list_filter.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
item_equivocating_in_trace item prefix
∧ (prefix, item, suffix)
  ∈ one_element_decompositions tr
    unfold item_equivocating_in_trace.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
from_option
  (λ m : message,
     ¬ trace_has_message (field_selector output) m
         prefix) False (input item)
∧ (prefix, item, suffix)
  ∈ one_element_decompositions tr
    simpl in *.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
from_option
  (λ m : message,
     ¬ trace_has_message (field_selector output) m
         prefix) False (input item)
∧ (prefix, item, suffix)
  ∈ one_element_decompositions tr  rewrite Hinput.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
from_option
  (λ m : message,
     ¬ trace_has_message (field_selector output) m
         prefix) False (Some im)
∧ (prefix, item, suffix)
  ∈ one_element_decompositions tr
    split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
tr: list (composite_transition_item IM)
v: validator
im: message
Hsender: sender im = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some im
Heqv: ¬ trace_has_message (field_selector output) im
    prefix
(prefix, item, suffix) ∈ one_element_decompositions tr
    by apply elem_of_one_element_decompositions.
Qed.

Lemma equivocating_senders_in_trace_prefix prefix suffix
  : equivocating_senders_in_trace prefix ⊆ equivocating_senders_in_trace (prefix ++ suffix).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
prefix, suffix: list (composite_transition_item IM)
equivocating_senders_in_trace prefix
⊆ equivocating_senders_in_trace (prefix ++ suffix)
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
prefix, suffix: list (composite_transition_item IM)
equivocating_senders_in_trace prefix
⊆ equivocating_senders_in_trace (prefix ++ suffix)
  intros v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
prefix, suffix: list (composite_transition_item IM)
v: validator
v ∈ equivocating_senders_in_trace prefix
→ v ∈ equivocating_senders_in_trace (prefix ++ suffix) rewrite !elem_of_equivocating_senders_in_trace.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
prefix, suffix: list (composite_transition_item IM)
v: validator
(∃ m : message,
   sender m = Some v
   ∧ equivocation_in_trace (free_composite_vlsm IM) m
       prefix)
→ ∃ m : message,
    sender m = Some v
    ∧ equivocation_in_trace (free_composite_vlsm IM) m
        (prefix ++ suffix)
  intros [m [Hm Heqv]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
prefix, suffix: list (composite_transition_item IM)
v: validator
m: message
Hm: sender m = Some v
Heqv: equivocation_in_trace (free_composite_vlsm IM)
  m prefix
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace (free_composite_vlsm IM) m
      (prefix ++ suffix)
  exists m.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
prefix, suffix: list (composite_transition_item IM)
v: validator
m: message
Hm: sender m = Some v
Heqv: equivocation_in_trace (free_composite_vlsm IM)
  m prefix
sender m = Some v
∧ equivocation_in_trace (free_composite_vlsm IM) m
    (prefix ++ suffix) split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
prefix, suffix: list (composite_transition_item IM)
v: validator
m: message
Hm: sender m = Some v
Heqv: equivocation_in_trace (free_composite_vlsm IM)
  m prefix
equivocation_in_trace (free_composite_vlsm IM) m
  (prefix ++ suffix)
  by apply equivocation_in_trace_prefix.
Qed.

An alternative definition for detecting equivocation in a certain state, which checks that for every valid trace (using any messages) reaching that state there exists an equivocation involving the given validator.

Notably, this definition is not generally equivalent to is_equivocating_statewise, which does not verify the order in which receiving and sending occurred.

Definition is_equivocating_tracewise
  (s : composite_state IM)
  (v : validator)
  (j := A v)
  : Prop
  :=
  forall is tr
  (Hpr : finite_constrained_trace_init_to (free_composite_vlsm IM) is s tr),
  exists (m : message),
  (sender m = Some v) /\
  exists prefix elem suffix (lprefix := finite_trace_last is prefix),
  tr = prefix ++ elem :: suffix
  /\ input elem = Some m
  /\ ~ has_been_sent (IM j) (lprefix j) m.

A possibly friendlier version using a previously defined primitive. Note that this definition does not require the HasBeenSentCapability.

Definition is_equivocating_tracewise_no_has_been_sent
  (s : composite_state IM)
  (v : validator)
  (j := A v)
  : Prop
  :=
  forall is tr
  (Htr : finite_constrained_trace_init_to (free_composite_vlsm IM) is s tr),
  exists (m : message),
  (sender m = Some v) /\
  equivocation_in_trace (preloaded_with_all_messages_vlsm (free_composite_vlsm IM)) m tr.

Lemma is_equivocating_tracewise_no_has_been_sent_equivocating_senders_in_trace
  (s : composite_state IM)
  (v : validator)
  : is_equivocating_tracewise_no_has_been_sent s v <->
    forall is tr
    (Htr : finite_constrained_trace_init_to (free_composite_vlsm IM) is s tr),
    v ∈ equivocating_senders_in_trace tr.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
is_equivocating_tracewise_no_has_been_sent s v
↔ (∀ (is : state
             (preloaded_with_all_messages_vlsm
                (free_composite_vlsm IM))) (tr : list
                                                 transition_item),
     finite_constrained_trace_init_to
       (free_composite_vlsm IM) is s tr
     → v ∈ equivocating_senders_in_trace tr)
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
is_equivocating_tracewise_no_has_been_sent s v
↔ (∀ (is : state
             (preloaded_with_all_messages_vlsm
                (free_composite_vlsm IM))) (tr : list
                                                 transition_item),
     finite_constrained_trace_init_to
       (free_composite_vlsm IM) is s tr
     → v ∈ equivocating_senders_in_trace tr)
  by split; intros Heqv is tr Htr; specialize (Heqv _ _ Htr)
  ; apply elem_of_equivocating_senders_in_trace.
Qed.

If any message can only be emitted by a component corresponding to its sender (sender_safety_alt_prop), then is_equivocating_tracewise is equivalent to is_equivocating_tracewise_no_has_been_sent.

Lemma is_equivocating_tracewise_no_has_been_sent_iff
  (Hsender_safety : sender_safety_alt_prop IM A sender)
  s v
  : is_equivocating_tracewise_no_has_been_sent s v <-> is_equivocating_tracewise s v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is_equivocating_tracewise_no_has_been_sent s v
↔ is_equivocating_tracewise s v
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is_equivocating_tracewise_no_has_been_sent s v
↔ is_equivocating_tracewise s v
  unfold is_equivocating_tracewise, equivocation_in_trace,
    is_equivocating_tracewise_no_has_been_sent.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
(∀ (is : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM))) (tr : list
                                                 transition_item),
   finite_constrained_trace_init_to
     (free_composite_vlsm IM) is s tr
   → ∃ m : message,
       sender m = Some v
       ∧ equivocation_in_trace
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)) m tr)
↔ (∀ (is : state
             (preloaded_with_all_messages_vlsm
                (free_composite_vlsm IM))) (tr : list
                                                 transition_item),
     finite_constrained_trace_init_to
       (free_composite_vlsm IM) is s tr
     → ∃ m : message,
         sender m = Some v
         ∧ (∃ (prefix : list transition_item) (elem : transition_item) 
              (suffix : list transition_item),
              tr = prefix ++ elem :: suffix
              ∧ input elem = Some m
                ∧ ¬ has_been_sent (IM (A v))
                      (finite_trace_last is prefix
                         (A v)) m))
  apply forall_proper; intros is.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
(∀ tr : list transition_item,
   finite_constrained_trace_init_to
     (free_composite_vlsm IM) is s tr
   → ∃ m : message,
       sender m = Some v
       ∧ equivocation_in_trace
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)) m tr)
↔ (∀ tr : list transition_item,
     finite_constrained_trace_init_to
       (free_composite_vlsm IM) is s tr
     → ∃ m : message,
         sender m = Some v
         ∧ (∃ (prefix : list transition_item) (elem : transition_item) 
              (suffix : list transition_item),
              tr = prefix ++ elem :: suffix
              ∧ input elem = Some m
                ∧ ¬ has_been_sent (IM (A v))
                      (finite_trace_last is prefix
                         (A v)) m))
  apply forall_proper; intros.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
x: list transition_item
(finite_constrained_trace_init_to
   (free_composite_vlsm IM) is s x
 → ∃ m : message,
     sender m = Some v
     ∧ equivocation_in_trace
         (preloaded_with_all_messages_vlsm
            (free_composite_vlsm IM)) m x)
↔ (finite_constrained_trace_init_to
     (free_composite_vlsm IM) is s x
   → ∃ m : message,
       sender m = Some v
       ∧ (∃ (prefix : list transition_item) (elem : transition_item) 
            (suffix : list transition_item),
            x = prefix ++ elem :: suffix
            ∧ input elem = Some m
              ∧ ¬ has_been_sent (IM (A v))
                    (finite_trace_last is prefix (A v))
                    m))
  apply forall_proper; intros [].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
x: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s x
H11: initial_state_prop is
(∃ m : message,
   sender m = Some v
   ∧ equivocation_in_trace
       (preloaded_with_all_messages_vlsm
          (free_composite_vlsm IM)) m x)
↔ (∃ m : message,
     sender m = Some v
     ∧ (∃ (prefix : list transition_item) (elem : transition_item) 
          (suffix : list transition_item),
          x = prefix ++ elem :: suffix
          ∧ input elem = Some m
            ∧ ¬ has_been_sent (IM (A v))
                  (finite_trace_last is prefix (A v))
                  m))
  apply exist_proper; intros.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
x: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s x
H11: initial_state_prop is
x0: message
sender x0 = Some v
∧ equivocation_in_trace
    (preloaded_with_all_messages_vlsm
       (free_composite_vlsm IM)) x0 x
↔ sender x0 = Some v
  ∧ (∃ (prefix : list transition_item) (elem : transition_item) 
       (suffix : list transition_item),
       x = prefix ++ elem :: suffix
       ∧ input elem = Some x0
         ∧ ¬ has_been_sent (IM (A v))
               (finite_trace_last is prefix (A v)) x0)
  apply and_proper_l; intro.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
x: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s x
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
equivocation_in_trace
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) x0 x
↔ (∃ (prefix : list transition_item) (elem : transition_item) 
     (suffix : list transition_item),
     x = prefix ++ elem :: suffix
     ∧ input elem = Some x0
       ∧ ¬ has_been_sent (IM (A v))
             (finite_trace_last is prefix (A v)) x0)
  apply exist_proper; intro prefix.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
x: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s x
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
prefix: list transition_item
(∃ (item : transition_item) (suffix : list
                                        transition_item),
   x = prefix ++ item :: suffix
   ∧ input item = Some x0
     ∧ ¬ trace_has_message (field_selector output) x0
           prefix)
↔ (∃ (elem : transition_item) (suffix : list
                                          transition_item),
     x = prefix ++ elem :: suffix
     ∧ input elem = Some x0
       ∧ ¬ has_been_sent (IM (A v))
             (finite_trace_last is prefix (A v)) x0)
  apply exist_proper; intro.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
x: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s x
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
prefix: list transition_item
x1: transition_item
(∃ suffix : list transition_item,
   x = prefix ++ x1 :: suffix
   ∧ input x1 = Some x0
     ∧ ¬ trace_has_message (field_selector output) x0
           prefix)
↔ (∃ suffix : list transition_item,
     x = prefix ++ x1 :: suffix
     ∧ input x1 = Some x0
       ∧ ¬ has_been_sent (IM (A v))
             (finite_trace_last is prefix (A v)) x0)
  apply exist_proper; intro.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
x: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s x
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
prefix: list transition_item
x1: transition_item
x2: list transition_item
x = prefix ++ x1 :: x2
∧ input x1 = Some x0
  ∧ ¬ trace_has_message (field_selector output) x0
        prefix
↔ x = prefix ++ x1 :: x2
  ∧ input x1 = Some x0
    ∧ ¬ has_been_sent (IM (A v))
          (finite_trace_last is prefix (A v)) x0
  apply and_proper_l; intros ->.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
input x1 = Some x0
∧ ¬ trace_has_message (field_selector output) x0
      prefix
↔ input x1 = Some x0
  ∧ ¬ has_been_sent (IM (A v))
        (finite_trace_last is prefix (A v)) x0
  apply and_iff_compat_l, not_iff_compat; cbn.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
trace_has_message (field_selector output) x0 prefix
↔ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) x0
  cut (finite_constrained_trace_init_to (free_composite_vlsm IM) is
    (finite_trace_last is prefix) prefix).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
→ trace_has_message (field_selector output) x0 prefix
  ↔ has_been_sent (IM (A v))
      (finite_trace_last is prefix (A v)) x0
message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
  {message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
→ trace_has_message (field_selector output) x0 prefix
  ↔ has_been_sent (IM (A v))
      (finite_trace_last is prefix (A v)) x0
    intros.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
H13: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
trace_has_message (field_selector output) x0 prefix
↔ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) x0
    erewrite <- oracle_initial_trace_update
      with (vlsm := free_composite_vlsm IM); cycle 1.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
H13: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
oracle_stepwise_props (field_selector output) ?Goal1
message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
H13: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
finite_constrained_trace_init_to
  (free_composite_vlsm IM) 
  ?Goal4 ?Goal3 prefix
message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
H13: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
?Goal1 ?Goal3 x0
↔ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) x0
    -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
H13: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
oracle_stepwise_props (field_selector output) ?Goal1 by apply free_composite_has_been_sent_stepwise_props.
    -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
H13: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
finite_constrained_trace_init_to
  (free_composite_vlsm IM) ?Goal2 ?Goal1 prefix done.
    -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
H13: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
composite_has_been_sent IM
  (finite_trace_last is prefix) x0
↔ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) x0 by eapply has_been_sent_iff_by_sender.
  }message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
finite_constrained_trace_init_to
  (free_composite_vlsm IM) is
  (finite_trace_last is prefix) prefix
  split; [| done].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
s: composite_state IM
v: validator
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
prefix: list transition_item
x1: transition_item
x2: list transition_item
H10: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s
  (prefix ++ x1 :: x2)
H11: initial_state_prop is
x0: message
H12: sender x0 = Some v
finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is
  (finite_trace_last is prefix) prefix
  by eapply  finite_valid_trace_from_to_app_split.
Qed.

Lemma transition_is_equivocating_tracewise_char
  l s om s' om'
  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
  (v : validator)
  : is_equivocating_tracewise_no_has_been_sent s' v ->
    is_equivocating_tracewise_no_has_been_sent s v \/
    om ≫= sender = Some v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
is_equivocating_tracewise_no_has_been_sent s' v
→ is_equivocating_tracewise_no_has_been_sent s v
  ∨ om ≫= sender = Some v
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
is_equivocating_tracewise_no_has_been_sent s' v
→ is_equivocating_tracewise_no_has_been_sent s v
  ∨ om ≫= sender = Some v
  destruct (decide (om ≫= sender = Some v))
  ; [by intro; right |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
is_equivocating_tracewise_no_has_been_sent s' v
→ is_equivocating_tracewise_no_has_been_sent s v
  ∨ om ≫= sender = Some v
  intros Heqv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
Heqv: is_equivocating_tracewise_no_has_been_sent s' v
is_equivocating_tracewise_no_has_been_sent s v
∨ om ≫= sender = Some v left.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
Heqv: is_equivocating_tracewise_no_has_been_sent s' v
is_equivocating_tracewise_no_has_been_sent s v intros is tr [Htr Hinit].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
Heqv: is_equivocating_tracewise_no_has_been_sent s' v
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) m tr
  specialize (extend_right_finite_trace_from_to _ Htr Ht) as Htr'.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
Heqv: is_equivocating_tracewise_no_has_been_sent s' v
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) m tr
  specialize (Heqv _ _ (conj Htr' Hinit)).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
Heqv: ∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) m
      (tr ++
       [{|
          l := l;
          input := om;
          destination := s';
          output := om'
        |}])
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) m tr
  destruct Heqv as [m [Hv [prefix [item [suffix [Heq Heqv]]]]]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) m tr
  exists m.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
sender m = Some v
∧ equivocation_in_trace
    (preloaded_with_all_messages_vlsm
       (free_composite_vlsm IM)) m tr split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
equivocation_in_trace
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) m tr exists prefix.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
∃ (item : transition_item) (suffix : list
                                       transition_item),
  tr = prefix ++ item :: suffix
  ∧ input item = Some m
    ∧ ¬ trace_has_message (field_selector output) m
          prefix
  destruct_list_last suffix suffix' item' Heqsuffix.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ [item]
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = []
∃ (item : transition_item) (suffix : list
                                       transition_item),
  tr = prefix ++ item :: suffix
  ∧ input item = Some m
    ∧ ¬ trace_has_message (field_selector output) m
          prefix
message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix' ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
∃ (item : transition_item) 
  (suffix : list transition_item),
  tr = prefix ++ item :: suffix
  ∧ input item = Some m
    ∧ ¬ trace_has_message 
          (field_selector output) m prefix
  {message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ [item]
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = []
∃ (item : transition_item) (suffix : list
                                       transition_item),
  tr = prefix ++ item :: suffix
  ∧ input item = Some m
    ∧ ¬ trace_has_message (field_selector output) m
          prefix exfalso.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix: list transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ [item]
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = []
False subst.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ [item]
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
False apply app_inj_tail, proj2 in Heq.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
Heq: {|
  l := l;
  input := om;
  destination := s';
  output := om'
|} = item
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
False subst item.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
Heqv: input
  {|
    l := l;
    input := om;
    destination := s';
    output := om'
  |} = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
False apply proj1 in Heqv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
Heqv: input
  {|
    l := l;
    input := om;
    destination := s';
    output := om'
  |} = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
False simpl in Heqv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
Heqv: om = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
False
    subst om.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
m: message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, Some m) (s', om')
v: validator
n: Some m ≫= sender ≠ Some v
tr: list transition_item
Hv: sender m = Some v
prefix: list transition_item
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := Some m;
      destination := s';
      output := om'
    |}])
False simpl in n.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s, s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
m: message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, Some m) (s', om')
v: validator
n: sender m ≠ Some v
tr: list transition_item
Hv: sender m = Some v
prefix: list transition_item
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := Some m;
      destination := s';
      output := om'
    |}])
False congruence. }message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix' ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
∃ (item : transition_item) (suffix : list
                                       transition_item),
  tr = prefix ++ item :: suffix
  ∧ input item = Some m
    ∧ ¬ trace_has_message (field_selector output) m
          prefix
  exists item, suffix'.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix' ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
tr = prefix ++ item :: suffix'
∧ input item = Some m
  ∧ ¬ trace_has_message (field_selector output) m
        prefix split; [| done].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix' ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
tr = prefix ++ item :: suffix'
  replace (prefix ++ item :: suffix' ++ [item']) with ((prefix ++ item :: suffix') ++ [item']) in Heq.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = (prefix ++ item :: suffix') ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
tr = prefix ++ item :: suffix'
message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix' ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
(prefix ++ item :: suffix') ++ [item'] =
prefix ++ item :: suffix' ++ [item']
  -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = (prefix ++ item :: suffix') ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
tr = prefix ++ item :: suffix' apply app_inj_tail in Heq.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr = prefix ++ item :: suffix'
∧ {|
    l := l;
    input := om;
    destination := s';
    output := om'
  |} = item'
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
tr = prefix ++ item :: suffix' apply Heq.
  -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
v: validator
n: om ≫= sender ≠ Some v
tr: list transition_item
m: message
Hv: sender m = Some v
prefix: list transition_item
item: transition_item
suffix, suffix': list transition_item
item': transition_item
Heq: tr ++
[{|
   l := l;
   input := om;
   destination := s';
   output := om'
 |}] = prefix ++ item :: suffix' ++ [item']
Heqv: input item = Some m
∧ ¬ trace_has_message (field_selector output) m
      prefix
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s tr
Hinit: initial_state_prop is
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) is s'
  (tr ++
   [{|
      l := l;
      input := om;
      destination := s';
      output := om'
    |}])
Heqsuffix: suffix = suffix' ++ [item']
(prefix ++ item :: suffix') ++ [item'] =
prefix ++ item :: suffix' ++ [item'] by rewrite <- app_assoc.
Qed.

Lemma transition_receiving_no_sender_reflects_is_equivocating_tracewise
  l s om s' om'
  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
  (Hno_sender : om ≫= sender = None)
  (v : validator)
  : is_equivocating_tracewise_no_has_been_sent s' v -> is_equivocating_tracewise_no_has_been_sent s v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
v: validator
is_equivocating_tracewise_no_has_been_sent s' v
→ is_equivocating_tracewise_no_has_been_sent s v
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
v: validator
is_equivocating_tracewise_no_has_been_sent s' v
→ is_equivocating_tracewise_no_has_been_sent s v
  intro Hs'.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
v: validator
Hs': is_equivocating_tracewise_no_has_been_sent s' v
is_equivocating_tracewise_no_has_been_sent s v
  by destruct (transition_is_equivocating_tracewise_char _ _ _ _ _ Ht v Hs'); [| congruence].
Qed.

Lemma is_equivocating_statewise_implies_is_equivocating_tracewise s v
  : is_equivocating_statewise IM A sender s v -> is_equivocating_tracewise s v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
is_equivocating_statewise IM A sender s v
→ is_equivocating_tracewise s v
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
is_equivocating_statewise IM A sender s v
→ is_equivocating_tracewise s v
  intros [j [m [Hm [Hnbs_m Hbr_m]]]] is tr Htr.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
Hbr_m: has_been_received (IM j) (s j) m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
∃ m : message,
  sender m = Some v
  ∧ (∃ (prefix : list transition_item) (elem : transition_item) 
       (suffix : list transition_item),
       let lprefix := finite_trace_last is prefix in
       tr = prefix ++ elem :: suffix
       ∧ input elem = Some m
         ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v))
               m)
  exists m.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
Hbr_m: has_been_received (IM j) (s j) m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
sender m = Some v
∧ (∃ (prefix : list transition_item) (elem : transition_item) 
     (suffix : list transition_item),
     let lprefix := finite_trace_last is prefix in
     tr = prefix ++ elem :: suffix
     ∧ input elem = Some m
       ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m) split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
Hbr_m: has_been_received (IM j) (s j) m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  apply (preloaded_finite_valid_trace_init_to_projection _ j) in Htr as Htrj.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
Hbr_m: has_been_received (IM j) (s j) m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  apply proj1 in Htrj as Hlstj.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
Hbr_m: has_been_received (IM j) (s j) m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM j))
  (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  apply finite_valid_trace_from_to_last_pstate in Hlstj.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
Hbr_m: has_been_received (IM j) (s j) m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  apply proper_received in Hbr_m; [| done].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
Hbr_m: selected_message_exists_in_all_preloaded_traces
  (IM j) (field_selector input) 
  (s j) m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
tr: list transition_item
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  specialize (Hbr_m _ _ Htrj).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
Hbr_m: trace_has_message (field_selector input) m
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  apply Exists_exists in Hbr_m.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
Hbr_m: ∃ x : transition_item,
  x
  ∈ VLSMTotalProjection.VLSM_projection_finite_trace_project
      (preloaded_component_projection IM j) tr
  ∧ field_selector input m x
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  destruct Hbr_m as [itemj [Hitemj Hinput]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
Hitemj: itemj
∈ VLSMTotalProjection.VLSM_projection_finite_trace_project
    (preloaded_component_projection IM j) tr
Hinput: field_selector input m itemj
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  apply (finite_trace_projection_list_in_rev IM) in Hitemj
    as [item [Hitem [_ [Heq_input _]]]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
Hitem: item ∈ tr
Heq_input: input item = input itemj
Hinput: field_selector input m itemj
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  simpl in Hinput.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
Hitem: item ∈ tr
Heq_input: input item = input itemj
Hinput: input itemj = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m rewrite <- Heq_input in Hinput.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
Hitem: item ∈ tr
Heq_input: input item = input itemj
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m clear Heq_input.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
Hitem: item ∈ tr
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  apply elem_of_list_split in Hitem.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
Hitem: ∃ l1 l2 : list (composite_transition_item IM),
  tr = l1 ++ item :: l2
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  destruct Hitem as [prefix [suffix Heq_tr]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
∃ (prefix : list transition_item) (elem : transition_item) 
  (suffix : list transition_item),
  let lprefix := finite_trace_last is prefix in
  tr = prefix ++ elem :: suffix
  ∧ input elem = Some m
    ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m
  exists prefix, item, suffix.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
let lprefix := finite_trace_last is prefix in
tr = prefix ++ item :: suffix
∧ input item = Some m
  ∧ ¬ has_been_sent (IM (A v)) (lprefix (A v)) m split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
input item = Some m
∧ ¬ has_been_sent (IM (A v))
      (finite_trace_last is prefix (A v)) m split; [done |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
tr: list transition_item
itemj: transition_item
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
Heq_tr: tr = prefix ++ item :: suffix
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s tr
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j) tr)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  subst.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
v: validator
j: index
m: message
Hm: sender m = Some v
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
itemj: transition_item
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
Hinput: input item = Some m
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htrj: finite_constrained_trace_init_to 
  (IM j) (is j) (s j)
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM j)
     (prefix ++ item :: suffix))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s
  (prefix ++ item :: suffix)
Hlstj: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM j))
  (s j)
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  clear -Hnbs_m Htr.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s
  (prefix ++ item :: suffix)
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  apply preloaded_finite_valid_trace_init_to_projection with (j := A v) in Htr as Htrv.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) is s
  (prefix ++ item :: suffix)
Htrv: finite_constrained_trace_init_to 
  (IM (A v)) (is (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (prefix ++ item :: suffix))
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  apply proj1, finite_valid_trace_from_to_app_split, proj1
    , preloaded_finite_valid_trace_from_to_projection with (j := A v)
    , finite_valid_trace_from_to_last in Htr.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_constrained_trace_init_to 
  (IM (A v)) (is (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (prefix ++ item :: suffix))
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  rewrite (VLSMTotalProjection.VLSM_projection_finite_trace_project_app
    (preloaded_component_projection IM (A v))) in Htrv.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_constrained_trace_init_to 
  (IM (A v)) (is (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix ++
   VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  apply proj1, (finite_valid_trace_from_to_app_split (preloaded_with_all_messages_vlsm (IM (A v))))
    in Htrv as [_ Htrv].message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last (is (A v))
     (VLSMTotalProjection.VLSM_projection_finite_trace_project
        (preloaded_component_projection IM
           (A v)) prefix)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  rewrite Htr in Htrv.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
¬ has_been_sent (IM (A v))
    (finite_trace_last is prefix (A v)) m
  intro Hbs_m.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
Hbs_m: has_been_sent (IM (A v))
  (finite_trace_last is prefix (A v)) m
False elim Hnbs_m.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
Hnbs_m: has_not_been_sent (IM (A v)) (s (A v)) m
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
Hbs_m: has_been_sent (IM (A v))
  (finite_trace_last is prefix (A v)) m
has_been_sent (IM (A v)) (s (A v)) m clear Hnbs_m.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
Hbs_m: has_been_sent (IM (A v))
  (finite_trace_last is prefix (A v)) m
has_been_sent (IM (A v)) (s (A v)) m
  revert Hbs_m.message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
has_been_sent (IM (A v))
  (finite_trace_last is prefix (A v)) m
→ has_been_sent (IM (A v)) (s (A v)) m
  apply in_futures_preserving_oracle_from_stepwise with (field_selector output).message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
oracle_stepwise_props (field_selector output)
  (has_been_sent (IM (A v)))
message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
in_futures
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  -message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
oracle_stepwise_props (field_selector output)
  (has_been_sent (IM (A v))) by apply has_been_sent_stepwise_props.
  -message, index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
validator: Type
A: validator → index
s: composite_state IM
v: validator
m: message
item: composite_transition_item IM
prefix, suffix: list (composite_transition_item IM)
is: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Htr: finite_trace_last (is (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     prefix) = finite_trace_last is prefix (A v)
Htrv: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) 
  (s (A v))
  (VLSMTotalProjection.VLSM_projection_finite_trace_project
     (preloaded_component_projection IM (A v))
     (item :: suffix))
in_futures
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (finite_trace_last is prefix (A v)) (s (A v)) by eexists.
Qed.

Lemma initial_state_not_is_equivocating_tracewise
  (s : composite_state IM)
  (Hs : composite_initial_state_prop IM s)
  (v : validator)
  : ~ is_equivocating_tracewise_no_has_been_sent s v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
Hs: composite_initial_state_prop IM s
v: validator
¬ is_equivocating_tracewise_no_has_been_sent s v
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
Hs: composite_initial_state_prop IM s
v: validator
¬ is_equivocating_tracewise_no_has_been_sent s v
  intros Heqv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
Hs: composite_initial_state_prop IM s
v: validator
Heqv: is_equivocating_tracewise_no_has_been_sent s v
False
  specialize (Heqv s []).message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
Hs: composite_initial_state_prop IM s
v: validator
Heqv: finite_constrained_trace_init_to
  (free_composite_vlsm IM) s s []
→ ∃ m : message,
    sender m = Some v
    ∧ equivocation_in_trace
        (preloaded_with_all_messages_vlsm
           (free_composite_vlsm IM)) m []
False
  spec Heqv; [by split; [| done]; constructor; apply initial_state_is_valid |].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
Hs: composite_initial_state_prop IM s
v: validator
Heqv: ∃ m : message,
  sender m = Some v
  ∧ equivocation_in_trace
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) m []
False
  destruct Heqv as [m [_ [prefix [suf [item [Heq _]]]]]].message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
s: composite_state IM
Hs: composite_initial_state_prop IM s
v: validator
m: message
prefix: list transition_item
suf: transition_item
item: list transition_item
Heq: [] = prefix ++ suf :: item
False
  by destruct prefix; inversion Heq.
Qed.

Context
  `{RelDecision _ _ is_equivocating_tracewise_no_has_been_sent}
  .

#[export] Program Instance equivocation_dec_tracewise
  : BasicEquivocation (composite_state IM) validator Cv threshold :=
  {
    state_validators := fun _ => list_to_set (enum validator);
    is_equivocating := is_equivocating_tracewise_no_has_been_sent;
  }.

Lemma equivocating_validators_is_equivocating_tracewise_iff s v
  : v ∈ equivocating_validators s <-> is_equivocating_tracewise_no_has_been_sent s v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
v: validator
v ∈ equivocating_validators s
↔ is_equivocating_tracewise_no_has_been_sent s v
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
v: validator
v ∈ equivocating_validators s
↔ is_equivocating_tracewise_no_has_been_sent s v
  unfold equivocating_validators.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
v: validator
v
∈ filter (λ v : validator, is_equivocating s v)
    (state_validators s)
↔ is_equivocating_tracewise_no_has_been_sent s v
  simpl.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
v: validator
v
∈ filter
    (λ v : validator,
       is_equivocating_tracewise_no_has_been_sent s v)
    (list_to_set (enum validator))
↔ is_equivocating_tracewise_no_has_been_sent s v
  rewrite elem_of_filter, elem_of_list_to_set.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
v: validator
is_equivocating_tracewise_no_has_been_sent s v
∧ v ∈ enum validator
↔ is_equivocating_tracewise_no_has_been_sent s v
  by itauto (apply elem_of_enum).
Qed.

Lemma equivocating_validators_empty_in_initial_state
  (s : composite_state IM)
  (His : composite_initial_state_prop IM s)
  : equivocating_validators s ≡@{Cv} ∅.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
equivocating_validators s ≡ ∅
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
equivocating_validators s ≡ ∅
  intro v.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
v: validator
v ∈ equivocating_validators s ↔ v ∈ ∅ split.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
v: validator
v ∈ equivocating_validators s → v ∈ ∅
message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
v: validator
v ∈ ∅ → v ∈ equivocating_validators s
  -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
v: validator
v ∈ equivocating_validators s → v ∈ ∅ rewrite equivocating_validators_is_equivocating_tracewise_iff.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
v: validator
is_equivocating_tracewise_no_has_been_sent s v → v ∈ ∅
    by apply initial_state_not_is_equivocating_tracewise with (v := v) in His.
  -message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
His: composite_initial_state_prop IM s
v: validator
v ∈ ∅ → v ∈ equivocating_validators s by intro HV; contradict HV; apply not_elem_of_empty.
Qed.

Lemma input_valid_transition_receiving_no_sender_reflects_equivocating_validators
  l s om s' om'
  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
  (Hno_sender : om ≫= sender = None)
  : equivocating_validators s' ⊆ equivocating_validators s.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
equivocating_validators s' ⊆ equivocating_validators s
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
equivocating_validators s' ⊆ equivocating_validators s
  intros v Hs'%equivocating_validators_is_equivocating_tracewise_iff.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
v: validator
Hs': is_equivocating_tracewise_no_has_been_sent s' v
v ∈ equivocating_validators s
  by eapply equivocating_validators_is_equivocating_tracewise_iff,
            transition_receiving_no_sender_reflects_is_equivocating_tracewise.
Qed.

Lemma initial_state_equivocators_weight
  (s : composite_state IM)
  (Hs : composite_initial_state_prop IM s)
  : equivocation_fault s = 0%R.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
Hs: composite_initial_state_prop IM s
equivocation_fault s = 0%R
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
Hs: composite_initial_state_prop IM s
equivocation_fault s = 0%R
  apply equivocating_validators_empty_in_initial_state, elements_empty_iff in Hs.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
Hs: elements (equivocating_validators s) = []
equivocation_fault s = 0%R
  unfold equivocation_fault.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
s: composite_state IM
Hs: elements (equivocating_validators s) = []
sum_weights (equivocating_validators s) = 0%R
  by apply sum_weights_empty, elements_empty_iff.
Qed.

Lemma composite_transition_no_sender_equivocators_weight
  l s om s' om'
  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s, om) (s', om'))
  (Hno_sender : om ≫= sender = None)
  : (equivocation_fault s' <= equivocation_fault s)%R.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
(equivocation_fault s' <= equivocation_fault s)%R
Proof.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
(equivocation_fault s' <= equivocation_fault s)%R
  specialize (input_valid_transition_receiving_no_sender_reflects_equivocating_validators
    _ _ _ _ _ Ht Hno_sender) as Heqv.message: Type
EqDecision0: EqDecision message
index: Type
EqDecision1: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HasBeenSentCapability (IM i)
H0: ∀ i : index, HasBeenReceivedCapability (IM i)
validator: Type
EqDecision2: EqDecision validator
threshold: R
Hmeasurable_V: Measurable validator
Cv: Type
H1: ElemOf validator Cv
H2: Empty Cv
H3: Singleton validator Cv
H4: Union Cv
H5: Intersection Cv
H6: Difference Cv
H7: Elements validator Cv
EqDecision3: EqDecision validator
H8: FinSet validator Cv
ReachableThreshold0: ReachableThreshold validator Cv
  threshold
EqDecision4: EqDecision validator
H9: finite.Finite validator
A: validator → index
sender: message → option validator
H10: RelDecision
  is_equivocating_tracewise_no_has_been_sent
l: label
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om: option message
s': state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om': option message
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s, om) (s', om')
Hno_sender: om ≫= sender = None
Heqv: equivocating_validators s'
⊆ equivocating_validators s
(equivocation_fault s' <= equivocation_fault s)%R
  by apply incl_equivocating_validators_equivocation_fault.
Qed.

End sec_tracewise_equivocation.