From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.
From VLSM.Core Require Import VLSM Composition Equivocation MessageDependencies.
From VLSM.Core Require Import VLSMProjections ProjectionTraces.

Sufficient conditions for being a validator for the free composition

In this module we give sufficient conditions for a component to be a validator for the free composition it is part of.

Namely, we show that if an indexed collection of VLSMs IM satisfies the channel_authentication_property, the MessageDependencies and FullMessageDependencies assumptions, the HasBeenSentCapability and HasBeenReceivedCapability, then any component, which for every valid input guarantees that the message and all its dependencies are emittable by one of the components, is a validator for the free composition of IM (lemma free_valid_message_yields_projection_validator).

Specialized (simpler) conditions are provided and proved for components which additionally satisfy the message_dependencies_full_node_condition_property.

Message validators are validators for the free composition

Section sec_free_composition_validator.

Context
  `{EqDecision index}
  `(IM : index -> VLSM message)
  .

If a component is a message-validator for the free composition, then any constrained trace of the component lifts to a valid trace of the composition.

Lemma free_component_message_validator_valid_trace :
  forall (i : index),
    component_message_validator_prop IM (free_constraint IM) i ->
  forall is fi tr,
    finite_constrained_trace_init_to (IM i) is fi tr ->
    finite_valid_trace_init_to (free_composite_vlsm IM) (lift_to_composite_state' IM i is)
      (lift_to_composite_state' IM i fi) (lift_to_composite_finite_trace IM i tr).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
∀ i : index,
  component_message_validator_prop IM
    (free_constraint IM) i
  → ∀ (is
       fi : state
              (preloaded_with_all_messages_vlsm (IM i))) 
      (tr : list transition_item),
      finite_constrained_trace_init_to (IM i) is fi tr
      → finite_valid_trace_init_to
          (free_composite_vlsm IM)
          (lift_to_composite_state' IM i is)
          (lift_to_composite_state' IM i fi)
          (lift_to_composite_finite_trace IM i tr)
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
∀ i : index,
  component_message_validator_prop IM
    (free_constraint IM) i
  → ∀ (is
       fi : state
              (preloaded_with_all_messages_vlsm (IM i))) 
      (tr : list transition_item),
      finite_constrained_trace_init_to (IM i) is fi tr
      → finite_valid_trace_init_to
          (free_composite_vlsm IM)
          (lift_to_composite_state' IM i is)
          (lift_to_composite_state' IM i fi)
          (lift_to_composite_finite_trace IM i tr)
  intros i Hvalid isi fi tri Htri.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
finite_valid_trace_init_to (free_composite_vlsm IM)
  (lift_to_composite_state' IM i isi)
  (lift_to_composite_state' IM i fi)
  (lift_to_composite_finite_trace IM i tri)
  apply pre_traces_with_valid_inputs_are_valid.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
finite_constrained_trace_init_to
  (free_composite_vlsm IM)
  (lift_to_composite_state' IM i isi)
  (lift_to_composite_state' IM i fi)
  (lift_to_composite_finite_trace IM i tri)
index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
Forall
  (λ item : transition_item,
     option_valid_message_prop
       (free_composite_vlsm IM) 
       (input item))
  (lift_to_composite_finite_trace IM i tri)
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
finite_constrained_trace_init_to
  (free_composite_vlsm IM)
  (lift_to_composite_state' IM i isi)
  (lift_to_composite_state' IM i fi)
  (lift_to_composite_finite_trace IM i tri) by apply (VLSM_embedding_finite_valid_trace_init_to
      (lift_to_composite_preloaded_VLSM_embedding IM i)).
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
Forall
  (λ item : transition_item,
     option_valid_message_prop
       (free_composite_vlsm IM) (input item))
  (lift_to_composite_finite_trace IM i tri) rewrite Forall_forall.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
∀ x : transition_item,
  x ∈ lift_to_composite_finite_trace IM i tri
  → option_valid_message_prop (free_composite_vlsm IM)
      (input x)
    intros item Hitem.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
item: transition_item
Hitem: item ∈ lift_to_composite_finite_trace IM i tri
option_valid_message_prop (free_composite_vlsm IM)
  (input item)
    apply elem_of_list_fmap in Hitem as (itemi & -> & Hitem); cbn in isi, fi.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (IM i)
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
itemi: transition_item
Hitem: itemi ∈ tri
option_valid_message_prop (free_composite_vlsm IM)
  (input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i) itemi))
    apply elem_of_list_split in Hitem as (pre & suf & Heqtri).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (IM i)
tri: list transition_item
Htri: finite_constrained_trace_init_to 
  (IM i) isi fi tri
itemi: transition_item
pre, suf: list transition_item
Heqtri: tri = pre ++ itemi :: suf
option_valid_message_prop (free_composite_vlsm IM)
  (input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i) itemi))
    destruct Htri as [Htri _].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (IM i)
tri: list transition_item
Htri: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm (IM i)) isi
  fi tri
itemi: transition_item
pre, suf: list transition_item
Heqtri: tri = pre ++ itemi :: suf
option_valid_message_prop (free_composite_vlsm IM)
  (input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i) itemi))
    apply valid_trace_forget_last in Htri.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (IM i)
tri: list transition_item
Htri: finite_valid_trace_from
  (preloaded_with_all_messages_vlsm (IM i)) isi
  tri
itemi: transition_item
pre, suf: list transition_item
Heqtri: tri = pre ++ itemi :: suf
option_valid_message_prop (free_composite_vlsm IM)
  (input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i) itemi))
    eapply (input_valid_transition_to (preloaded_with_all_messages_vlsm (IM i)))
      in Heqtri as Ht; [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (IM i)
tri: list transition_item
Htri: finite_valid_trace_from
  (preloaded_with_all_messages_vlsm (IM i)) isi
  tri
itemi: transition_item
pre, suf: list transition_item
Heqtri: tri = pre ++ itemi :: suf
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  (l itemi)
  (finite_trace_last isi pre, input itemi)
  (destination itemi, output itemi)
option_valid_message_prop (free_composite_vlsm IM)
  (input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i) itemi))
    destruct itemi, input as [m |]; cbn in *;
      [| by apply option_valid_message_None].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (IM i)
tri: list transition_item
Htri: finite_valid_trace_from
  (preloaded_with_all_messages_vlsm (IM i)) isi
  tri
l: label (IM i)
m: message
destination: state (IM i)
output: option message
pre, suf: list transition_item
Heqtri: tri =
pre ++
{|
  l := l;
  input := Some m;
  destination := destination;
  output := output
|} :: suf
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l
  (finite_trace_last isi pre, Some m)
  (destination, output)
option_valid_message_prop (free_composite_vlsm IM)
  (Some m)
    unshelve eapply VLSM_incl_valid_message;
      [| by apply free_composite_vlsm_spec | by do 2 red |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
isi, fi: state (IM i)
tri: list transition_item
Htri: finite_valid_trace_from
  (preloaded_with_all_messages_vlsm (IM i)) isi
  tri
l: label (IM i)
m: message
destination: state (IM i)
output: option message
pre, suf: list transition_item
Heqtri: tri =
pre ++
{|
  l := l;
  input := Some m;
  destination := destination;
  output := output
|} :: suf
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l
  (finite_trace_last isi pre, Some m)
  (destination, output)
valid_message_prop
  {|
    vlsm_type := composite_type IM;
    vlsm_machine :=
      {|
        vlsm_type := free_composite_vlsm IM;
        vlsm_machine :=
          composite_vlsm IM (free_constraint IM)
      |}
  |} m
    by eapply Hvalid, input_valid_transition_iff; eexists.
Qed.

If a component is a message-validator for the free composition, then it is also a "full" validator for the free composition.

Lemma free_component_message_validator_yields_validator :
  forall (i : index),
    component_message_validator_prop IM (free_constraint IM) i ->
    component_projection_validator_prop IM (free_constraint IM) i.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
∀ i : index,
  component_message_validator_prop IM
    (free_constraint IM) i
  → component_projection_validator_prop IM
      (free_constraint IM) i
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
∀ i : index,
  component_message_validator_prop IM
    (free_constraint IM) i
  → component_projection_validator_prop IM
      (free_constraint IM) i
  intros i Hvalid li si iom Ht.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
Ht: input_constrained (IM i) li (si, iom)
valid li (si, iom)
  unfold input_constrained in Ht.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
Ht: input_valid
  (preloaded_with_all_messages_vlsm (IM i)) li
  (si, iom)
valid li (si, iom)
  apply input_valid_transition_iff in Ht as [[si' oom] Ht].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) li
  (si, iom) (si', oom)
valid li (si, iom)
  apply (exists_right_finite_trace_from (preloaded_with_all_messages_vlsm (IM i)))
    in Ht as (isi & tri & Htri & Hsi').index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htri: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm (IM i)) isi
  si'
  (tri ++
   [{|
      l := li;
      input := iom;
      destination := si';
      output := oom
    |}])
Hsi': finite_trace_last isi tri = si
valid li (si, iom)
  apply free_component_message_validator_valid_trace in Htri as [Htr _]; [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htr: finite_valid_trace_from_to
  (free_composite_vlsm IM)
  (lift_to_composite_state' IM i isi)
  (lift_to_composite_state' IM i si')
  (lift_to_composite_finite_trace IM i
     (tri ++
      [{|
         l := li;
         input := iom;
         destination := si';
         output := oom
       |}]))
Hsi': finite_trace_last isi tri = si
valid li (si, iom)
  setoid_rewrite map_app in Htr.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Htr: finite_valid_trace_from_to
  (free_composite_vlsm IM)
  (lift_to_composite_state' IM i isi)
  (lift_to_composite_state' IM i si')
  (map
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)) tri ++
   map
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i))
     [{|
        l := li;
        input := iom;
        destination := si';
        output := oom
      |}])
Hsi': finite_trace_last isi tri = si
valid li (si, iom)
  apply finite_valid_trace_from_to_app_split in Htr as [_ Ht].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Ht: finite_valid_trace_from_to
  (free_composite_vlsm IM)
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri))
  (lift_to_composite_state' IM i si')
  (map
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i))
     [{|
        l := li;
        input := iom;
        destination := si';
        output := oom
      |}])
Hsi': finite_trace_last isi tri = si
valid li (si, iom)
  apply valid_trace_forget_last, first_transition_valid in Ht as [Hv _].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Hv: input_valid (free_composite_vlsm IM)
  (l
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri),
   input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
Hsi': finite_trace_last isi tri = si
valid li (si, iom)
  eexists; split; cycle 1.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Hv: input_valid (free_composite_vlsm IM)
  (l
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri),
   input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
Hsi': finite_trace_last isi tri = si
input_valid (composite_vlsm IM (free_constraint IM))
  (existT i li) (?s, iom)
index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Hv: input_valid (free_composite_vlsm IM)
  (l
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri),
   input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
Hsi': finite_trace_last isi tri = si
?s i = si
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Hv: input_valid (free_composite_vlsm IM)
  (l
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri),
   input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
Hsi': finite_trace_last isi tri = si
input_valid (composite_vlsm IM (free_constraint IM))
  (existT i li) (?s, iom) apply (@VLSM_incl_input_valid _ _ (free_composite_vlsm IM)); [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Hv: input_valid (free_composite_vlsm IM)
  (l
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri),
   input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
Hsi': finite_trace_last isi tri = si
VLSM_incl_part (free_composite_vlsm IM)
  (constrained_vlsm_machine (free_composite_vlsm IM)
     (free_constraint IM))
    by apply free_composite_vlsm_spec.
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Hv: input_valid (free_composite_vlsm IM)
  (l
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri),
   input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
Hsi': finite_trace_last isi tri = si
finite_trace_last (lift_to_composite_state' IM i isi)
  (map
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)) tri) i = si cut (si = (lift_to_composite_state' IM i (finite_trace_last isi tri)) i);
      [by intros ->; rewrite (lift_to_composite_finite_trace_last IM) |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
Hvalid: component_message_validator_prop IM
  (free_constraint IM) i
li: label (IM i)
si: state (IM i)
iom: option message
si': state (preloaded_with_all_messages_vlsm (IM i))
oom: option message
isi: state (preloaded_with_all_messages_vlsm (IM i))
tri: list transition_item
Hv: input_valid (free_composite_vlsm IM)
  (l
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
  (finite_trace_last
     (lift_to_composite_state' IM i isi)
     (map
        (pre_VLSM_embedding_transition_item_project
           (IM i) (free_composite_vlsm IM)
           (lift_to_composite_label IM i)
           (lift_to_composite_state' IM i)) tri),
   input
     (pre_VLSM_embedding_transition_item_project
        (IM i) (free_composite_vlsm IM)
        (lift_to_composite_label IM i)
        (lift_to_composite_state' IM i)
        {|
          l := li;
          input := iom;
          destination := si';
          output := oom
        |}))
Hsi': finite_trace_last isi tri = si
si =
lift_to_composite_state' IM i
  (finite_trace_last isi tri) i
    by subst si; state_update_simpl.
Qed.

End sec_free_composition_validator.

Sufficient conditions for being a message validator for the free composition

Section sec_free_composition_message_validator.

Context
  `{EqDecision index}
  `(IM : index -> VLSM message)
  `(sender : message -> option validator)
  (A : validator -> index)
  (Hchannel : channel_authentication_prop  IM A sender)
  `{FinSet message Cm}
  (message_dependencies : message -> Cm)
  (full_message_dependencies : message -> Cm)
  `{!FullMessageDependencies message_dependencies full_message_dependencies}
  `{forall i : index, HasBeenSentCapability (IM i)}
  `{forall i : index, HasBeenReceivedCapability (IM i)}
  `{forall i : index, MessageDependencies (IM i) message_dependencies}
  .

Captures the union of constrained messages over all components of IM.

Definition emittable (m : message) : Prop :=
  exists i, can_emit (preloaded_with_all_messages_vlsm (IM i)) m.

A sufficient condition for determining that a message is valid for the free composition (see lemma free_valid_message_is_valid).

Inductive free_valid_message (m : message) : Prop :=
{
  fvm_emittable : emittable m;
  fvm_dependencies : set_Forall free_valid_message (message_dependencies m);
}.

A component satisfies the free_valid_message_condition property if the validity of receiving a message in a (constrained) state implies the free_valid_message property for that message

Definition free_valid_message_condition (i : index) : Prop :=
  forall l s m,
    input_constrained (IM i) l (s, Some m) ->
      free_valid_message m.

Under full-node assumptions, free_valid_message_condition can be simplified to only requiring that the message is emittable.

Definition full_node_free_valid_message_condition (i : index) : Prop :=
  forall l s m,
    input_constrained (IM i) l (s, Some m) ->
      emittable m.

Lemma full_node_free_valid_message_entails_helper :
  forall (i : index),
    message_dependencies_full_node_condition_prop (IM i) message_dependencies ->
    full_node_free_valid_message_condition i ->
  forall l s m,
    input_constrained (IM i) l (s, Some m) ->
    (forall dm, has_been_directly_observed (IM i) s dm -> free_valid_message dm) ->
      free_valid_message m.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ i : index,
  message_dependencies_full_node_condition_prop (IM i)
    message_dependencies
  → full_node_free_valid_message_condition i
    → ∀ (l : label
               (preloaded_with_all_messages_vlsm
                  (IM i))) (s : state
                                  (preloaded_with_all_messages_vlsm
                                     (IM i))) (m : message),
        input_constrained (IM i) l (s, Some m)
        → (∀ dm : message,
             has_been_directly_observed (IM i) s dm
             → free_valid_message dm)
          → free_valid_message m
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ i : index,
  message_dependencies_full_node_condition_prop (IM i)
    message_dependencies
  → full_node_free_valid_message_condition i
    → ∀ (l : label
               (preloaded_with_all_messages_vlsm
                  (IM i))) (s : state
                                  (preloaded_with_all_messages_vlsm
                                     (IM i))) (m : message),
        input_constrained (IM i) l (s, Some m)
        → (∀ dm : message,
             has_been_directly_observed (IM i) s dm
             → free_valid_message dm)
          → free_valid_message m
  intros i Hfulli Hfree l s m Hv Hobs.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
m: message
Hv: input_constrained (IM i) l (s, Some m)
Hobs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
free_valid_message m
  constructor; [by eapply Hfree |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
m: message
Hv: input_constrained (IM i) l (s, Some m)
Hobs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
set_Forall free_valid_message (message_dependencies m)
  intros dm Hdm.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
m: message
Hv: input_constrained (IM i) l (s, Some m)
Hobs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
dm: message
Hdm: dm ∈ message_dependencies m
free_valid_message dm
  eapply Hobs, Hfulli; [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
m: message
Hv: input_constrained (IM i) l (s, Some m)
Hobs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
dm: message
Hdm: dm ∈ message_dependencies m
valid ?l (s, Some m)
  by apply Hv.
Qed.

Lemma full_node_free_valid_message_entails :
  forall (i : index),
    message_dependencies_full_node_condition_prop (IM i) message_dependencies ->
    full_node_free_valid_message_condition i ->
      free_valid_message_condition i.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ i : index,
  message_dependencies_full_node_condition_prop (IM i)
    message_dependencies
  → full_node_free_valid_message_condition i
    → free_valid_message_condition i
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ i : index,
  message_dependencies_full_node_condition_prop (IM i)
    message_dependencies
  → full_node_free_valid_message_condition i
    → free_valid_message_condition i
  intros i Hfulli Hfree l s m Hv.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
m: message
Hv: input_constrained (IM i) l (s, Some m)
free_valid_message m
  eapply full_node_free_valid_message_entails_helper; [done.. |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
m: message
Hv: input_constrained (IM i) l (s, Some m)
∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
  destruct Hv as [Hs _].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
m: message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm (IM i)) s
∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
  induction Hs using valid_state_prop_ind; intros dm Hdm;
    [by contradict Hdm; apply has_been_directly_observed_no_inits |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om, om': option message
s: state (preloaded_with_all_messages_vlsm (IM i))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', om')
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
dm: message
Hdm: has_been_directly_observed (IM i) s' dm
free_valid_message dm
  eapply has_been_directly_observed_step_update in Hdm; [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om, om': option message
s: state (preloaded_with_all_messages_vlsm (IM i))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', om')
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
dm: message
Hdm: (om = Some dm ∨ om' = Some dm)
∨ has_been_directly_observed (IM i) s dm
free_valid_message dm
  destruct Hdm as [[-> | ->]|]; [.. | by apply IHHs].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om': option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, Some dm) (s', om')
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
free_valid_message dm
index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
free_valid_message dm
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om': option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, Some dm) (s', om')
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
free_valid_message dm by destruct Ht; eapply full_node_free_valid_message_entails_helper.
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
free_valid_message dm assert (Hdm : can_produce (preloaded_with_all_messages_vlsm (IM i)) s' dm)
      by (eexists _,_; done).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
free_valid_message dm
    apply message_dependencies_are_necessary in Hdm as Hdeps.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
free_valid_message dm
    constructor; [by eexists; apply can_emit_iff; eexists |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
set_Forall free_valid_message
  (message_dependencies dm)
    intros dm' Hdm'.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
dm': message
Hdm': dm' ∈ message_dependencies dm
free_valid_message dm'
    assert (dm' <> dm).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
dm': message
Hdm': dm' ∈ message_dependencies dm
dm' ≠ dm
index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
dm': message
Hdm': dm' ∈ message_dependencies dm
H10: dm' ≠ dm
free_valid_message dm'
    {index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
dm': message
Hdm': dm' ∈ message_dependencies dm
dm' ≠ dm
      intros ->.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
Hdm': dm ∈ message_dependencies dm
False
      eapply (irreflexivity (msg_dep_happens_before message_dependencies) dm).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
Hdm': dm ∈ message_dependencies dm
msg_dep_happens_before message_dependencies dm dm
      by constructor.
    }index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
dm': message
Hdm': dm' ∈ message_dependencies dm
H10: dm' ≠ dm
free_valid_message dm'
    eapply Hdeps, has_been_directly_observed_step_update in Hdm'; [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
om: option message
s: state (preloaded_with_all_messages_vlsm (IM i))
dm: message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, om) (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
dm': message
H10: dm' ≠ dm
Hdm': (om = Some dm' ∨ Some dm = Some dm')
∨ has_been_directly_observed (IM i) s dm'
free_valid_message dm'
    destruct Hdm' as [[-> | Hdm'] |]; [.. | by congruence | by apply IHHs].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
l: label (preloaded_with_all_messages_vlsm (IM i))
m: message
s': state (preloaded_with_all_messages_vlsm (IM i))
l0: label (preloaded_with_all_messages_vlsm (IM i))
s: state (preloaded_with_all_messages_vlsm (IM i))
dm, dm': message
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i)) l0
  (s, Some dm') (s', Some dm)
IHHs: ∀ dm : message,
  has_been_directly_observed (IM i) s dm
  → free_valid_message dm
Hdm: can_produce
  (preloaded_with_all_messages_vlsm (IM i)) s'
  dm
Hdeps: message_dependencies_full_node_condition
  (IM i) message_dependencies s' dm
H10: dm' ≠ dm
free_valid_message dm'
    by destruct Ht; eapply full_node_free_valid_message_entails_helper.
Qed.

Lemma free_valid_message_emittable_from_dependencies :
  forall (m : message),
    free_valid_message m ->
    Emittable_from_dependencies_prop IM A sender message_dependencies m.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ m : message,
  free_valid_message m
  → Emittable_from_dependencies_prop IM A sender
      message_dependencies m
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ m : message,
  free_valid_message m
  → Emittable_from_dependencies_prop IM A sender
      message_dependencies m
  intros m [[i Hemit] _].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
i: index
Hemit: can_emit
  (preloaded_with_all_messages_vlsm (IM i)) m
Emittable_from_dependencies_prop IM A sender
  message_dependencies m
  apply Hchannel in Hemit as Hauth.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
i: index
Hemit: can_emit
  (preloaded_with_all_messages_vlsm (IM i)) m
Hauth: channel_authenticated_message A sender i m
Emittable_from_dependencies_prop IM A sender
  message_dependencies m
  unfold channel_authenticated_message in Hauth.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
i: index
Hemit: can_emit
  (preloaded_with_all_messages_vlsm (IM i)) m
Hauth: option_map A (sender m) = Some i
Emittable_from_dependencies_prop IM A sender
  message_dependencies m
  destruct (sender m) eqn: Hsender; [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
i: index
Hemit: can_emit
  (preloaded_with_all_messages_vlsm (IM i)) m
v: validator
Hsender: sender m = Some v
Hauth: option_map A (Some v) = Some i
Emittable_from_dependencies_prop IM A sender
  message_dependencies m
  apply Some_inj in Hauth as <-.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
v: validator
Hemit: can_emit
  (preloaded_with_all_messages_vlsm (IM (A v)))
  m
Hsender: sender m = Some v
Emittable_from_dependencies_prop IM A sender
  message_dependencies m
  constructor 1 with v; [done |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
v: validator
Hemit: can_emit
  (preloaded_with_all_messages_vlsm (IM (A v)))
  m
Hsender: sender m = Some v
can_emit
  (preloaded_vlsm (IM (A v))
     (λ dm : message, dm ∈ message_dependencies m)) m
  by apply message_dependencies_are_sufficient.
Qed.

Lemma msg_dep_reflects_free_valid_message :
  forall (dm m : message),
    msg_dep_rel message_dependencies dm m ->
    free_valid_message m -> free_valid_message dm.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ dm m : message,
  msg_dep_rel message_dependencies dm m
  → free_valid_message m → free_valid_message dm
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ dm m : message,
  msg_dep_rel message_dependencies dm m
  → free_valid_message m → free_valid_message dm
  intros dm m Hdep [_ Hall].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
dm, m: message
Hdep: msg_dep_rel message_dependencies dm m
Hall: set_Forall free_valid_message
  (message_dependencies m)
free_valid_message dm
  by apply Hall.
Qed.

Lemma free_valid_message_is_valid :
  forall m : message,
    free_valid_message m ->
      valid_message_prop (free_composite_vlsm IM) m.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ m : message,
  free_valid_message m
  → valid_message_prop (free_composite_vlsm IM) m
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
∀ m : message,
  free_valid_message m
  → valid_message_prop (free_composite_vlsm IM) m
  intros m Hm.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
valid_message_prop (free_composite_vlsm IM) m
  eapply free_valid_from_all_dependencies_emitable_from_dependencies; [done |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
all_dependencies_emittable_from_dependencies_prop IM
  ?A ?sender message_dependencies
  full_message_dependencies m
  unfold all_dependencies_emittable_from_dependencies_prop.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
∀ dm : message,
  dm ∈ m :: elements (full_message_dependencies m)
  → Emittable_from_dependencies_prop IM ?A ?sender
      message_dependencies dm
  intros dm; rewrite elem_of_cons.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
dm: message
dm = m ∨ dm ∈ elements (full_message_dependencies m)
→ Emittable_from_dependencies_prop IM ?A ?sender
    message_dependencies dm
  intros [-> | Hdm]; [by apply free_valid_message_emittable_from_dependencies |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
dm: message
Hdm: dm ∈ elements (full_message_dependencies m)
Emittable_from_dependencies_prop IM A sender
  message_dependencies dm
  apply free_valid_message_emittable_from_dependencies.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
dm: message
Hdm: dm ∈ elements (full_message_dependencies m)
free_valid_message dm
  apply elem_of_elements, full_message_dependencies_happens_before in Hdm.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
dm: message
Hdm: msg_dep_happens_before message_dependencies dm m
free_valid_message dm
  eapply msg_dep_happens_before_reflect; [| done..].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
m: message
Hm: free_valid_message m
dm: message
Hdm: msg_dep_happens_before message_dependencies dm m
∀ dm m : message,
  msg_dep_rel message_dependencies dm m
  → free_valid_message m → free_valid_message dm
  by apply msg_dep_reflects_free_valid_message.
Qed.

Section sec_free_valid_message_validators.

If the validity predicate of a component implies that its input message satisfies free_valid_message, then the component is a message validator, and therefore, a validator for the free composition.

Context
  (i : index)
  (Hfree_valid_message_inputs : free_valid_message_condition i)
  .

Lemma free_valid_message_yields_message_validator :
  component_message_validator_prop IM (free_constraint IM) i.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfree_valid_message_inputs: free_valid_message_condition
  i
component_message_validator_prop IM
  (free_constraint IM) i
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfree_valid_message_inputs: free_valid_message_condition
  i
component_message_validator_prop IM
  (free_constraint IM) i
  intros li si im Him.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfree_valid_message_inputs: free_valid_message_condition
  i
li: label (preloaded_with_all_messages_vlsm (IM i))
si: state (preloaded_with_all_messages_vlsm (IM i))
im: message
Him: input_constrained (IM i) li (si, Some im)
valid_message_prop
  (composite_vlsm IM (free_constraint IM)) im
  unshelve eapply VLSM_incl_valid_message;
    [| by apply free_composite_vlsm_spec | by do 2 red |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfree_valid_message_inputs: free_valid_message_condition
  i
li: label (preloaded_with_all_messages_vlsm (IM i))
si: state (preloaded_with_all_messages_vlsm (IM i))
im: message
Him: input_constrained (IM i) li (si, Some im)
valid_message_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      {|
        vlsm_type := free_composite_vlsm IM;
        vlsm_machine := free_composite_vlsm IM
      |}
  |} im
  by eapply free_valid_message_is_valid, Hfree_valid_message_inputs, Him.
Qed.

Lemma free_valid_message_yields_projection_validator :
  component_projection_validator_prop IM (free_constraint IM) i.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfree_valid_message_inputs: free_valid_message_condition
  i
component_projection_validator_prop IM
  (free_constraint IM) i
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfree_valid_message_inputs: free_valid_message_condition
  i
component_projection_validator_prop IM
  (free_constraint IM) i
  by apply free_component_message_validator_yields_validator,
    free_valid_message_yields_message_validator.
Qed.

End sec_free_valid_message_validators.

Section sec_full_node_free_valid_message_validators.

Context
  (i : index)
  (Hfulli : message_dependencies_full_node_condition_prop (IM i) message_dependencies)
  (Hfree : full_node_free_valid_message_condition i)
  .

Lemma full_node_free_valid_message_yields_message_validator :
  component_message_validator_prop IM (free_constraint IM) i.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
component_message_validator_prop IM
  (free_constraint IM) i
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
component_message_validator_prop IM
  (free_constraint IM) i
  by apply free_valid_message_yields_message_validator,
    full_node_free_valid_message_entails.
Qed.

Lemma full_node_free_valid_message_yields_projection_validator :
  component_projection_validator_prop IM (free_constraint IM) i.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
component_projection_validator_prop IM
  (free_constraint IM) i
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
validator: Type
sender: message → option validator
A: validator → index
Hchannel: channel_authentication_prop IM A sender
Cm: Type
H: ElemOf message Cm
H0: Empty Cm
H1: Singleton message Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements message Cm
EqDecision1: EqDecision message
H6: FinSet message Cm
message_dependencies, full_message_dependencies: message → Cm
FullMessageDependencies0: FullMessageDependencies
  message_dependencies
  full_message_dependencies
H7: ∀ i : index, HasBeenSentCapability (IM i)
H8: ∀ i : index, HasBeenReceivedCapability (IM i)
H9: ∀ i : index,
  MessageDependencies (IM i) message_dependencies
i: index
Hfulli: message_dependencies_full_node_condition_prop
  (IM i) message_dependencies
Hfree: full_node_free_valid_message_condition i
component_projection_validator_prop IM
  (free_constraint IM) i
  by apply free_valid_message_yields_projection_validator,
    full_node_free_valid_message_entails.
Qed.

End sec_full_node_free_valid_message_validators.

End sec_free_composition_message_validator.