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.Lib Require Import Preamble ListExtras StdppExtras.
From VLSM.Core Require Import VLSM PreloadedVLSM ConstrainedVLSM.
From VLSM.Core Require Import Composition VLSMProjections Validator.

Section sec_projections.

Core: Composite VLSM Induced Projections

In this section we define a VLSM representing the induced projection of a composite VLSM to a single component (composite_vlsm_induced_projection), and we study the relation between their traces.

Let us fix an indexed set of VLSMs IM and their composition X constrained using the constraint predicate.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (constraint : composite_label IM -> composite_state IM * option message -> Prop)
  (X := composite_vlsm IM constraint)
  .

Definition composite_vlsm_induced_projection j : VLSM message :=
  preloaded_vlsm (IM j) (valid_message_prop X).

Lemma composite_vlsm_induced_projection_is_projection :
  forall j,
    VLSM_projection X (composite_vlsm_induced_projection j)
      (composite_project_label IM j) (fun s => s j).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
∀ j : index,
  VLSM_projection X
    (composite_vlsm_induced_projection j)
    (composite_project_label IM j)
    (λ s : state X, s j)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
∀ j : index,
  VLSM_projection X
    (composite_vlsm_induced_projection j)
    (composite_project_label IM j)
    (λ s : state X, s j)
  intro j; apply basic_VLSM_projection.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_valid_preservation X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) (λ s : state X, s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_transition_preservation_Some X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) 
  (λ s : state X, s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_transition_consistency_None X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) 
  (λ s : state X, s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
strong_projection_initial_state_preservation X
  (composite_vlsm_induced_projection j)
  (λ s : state X, s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_valid_message_preservation X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) 
  (λ s : state X, s j)
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_valid_preservation X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) (λ s : state X, s j) intros [i li] lY HlX s om (_ & _ & Hv & _) _ _.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j, i: index
li: label (IM i)
lY: label (composite_vlsm_induced_projection j)
HlX: composite_project_label IM j (existT i li) =
Some lY
s: state X
om: option message
Hv: valid (existT i li) (s, om)
valid lY (s j, om)
    by unfold composite_project_label in HlX; cbn in HlX;
      case_decide; inversion HlX; subst; clear HlX; cbn in *.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_transition_preservation_Some X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) (λ s : state X, s j) intros [i li] lY HlX s om s' om' [_ Ht].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j, i: index
li: label (IM i)
lY: label (composite_vlsm_induced_projection j)
HlX: composite_project_label IM j (existT i li) =
Some lY
s: state X
om: option message
s': state X
om': option message
Ht: transition (existT i li) (s, om) = (s', om')
transition lY (s j, om) = (s' j, om')
    unfold composite_project_label in HlX; cbn in HlX;
      case_decide; inversion HlX; subst; clear HlX; cbn in *.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
li: label (IM i)
s: composite_state IM
om: option message
s': composite_state IM
om': option message
Ht: (let (si', om') := transition li (s i, om) in
 (state_update IM s i si', om')) = (
s', om')
transition li (s i, om) = (s' i, om')
    destruct (transition _ _) as (si', _om').message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
li: label (IM i)
s: composite_state IM
om: option message
s': composite_state IM
om': option message
si': state (IM i)
_om': option message
Ht: (state_update IM s i si', _om') = (s', om')
(si', _om') = (s' i, om')
    by inversion Ht; state_update_simpl.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_transition_consistency_None X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) (λ s : state X, s j) intros [i li] HlX s om s' om' [_ Ht].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j, i: index
li: label (IM i)
HlX: composite_project_label IM j (existT i li) =
None
s: state X
om: option message
s': state X
om': option message
Ht: transition (existT i li) (s, om) = (s', om')
s' j = s j
      unfold composite_project_label in HlX; cbn in HlX;
      case_decide; inversion HlX; cbn in *.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j, i: index
li: label (IM i)
H: j ≠ i
HlX: None = None
s: composite_state IM
om: option message
s': composite_state IM
om': option message
Ht: (let (si', om') := transition li (s i, om) in
 (state_update IM s i si', om')) = (
s', om')
s' j = s j
    destruct (transition _ _ _); inversion Ht.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j, i: index
li: label (IM i)
H: j ≠ i
HlX: None = None
s: composite_state IM
om: option message
s': composite_state IM
om': option message
s0: state (IM i)
o: option message
Ht: (state_update IM s i s0, o) = (s', om')
H1: state_update IM s i s0 = s'
H2: o = om'
state_update IM s i s0 j = s j
    by state_update_simpl.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
strong_projection_initial_state_preservation X
  (composite_vlsm_induced_projection j)
  (λ s : state X, s j) by intros sX HsX; specialize (HsX j).
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
weak_projection_valid_message_preservation X
  (composite_vlsm_induced_projection j)
  (composite_project_label IM j) (λ s : state X, s j) intros [i li] lY HlX s m (_ & Hm & _ & _) _.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j, i: index
li: label (IM i)
lY: label (composite_vlsm_induced_projection j)
HlX: composite_project_label IM j (existT i li) =
Some lY
s: state X
m: message
Hm: option_valid_message_prop X (Some m)
valid_message_prop
  (composite_vlsm_induced_projection j) m
    by apply initial_message_is_valid; right.
Qed.

Lemma composite_vlsm_induced_projection_composition_iff :
  VLSM_eq X (composite_vlsm composite_vlsm_induced_projection constraint).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
VLSM_eq X
  (composite_vlsm composite_vlsm_induced_projection
     constraint)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
VLSM_eq X
  (composite_vlsm composite_vlsm_induced_projection
     constraint)
  split.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
VLSM_incl {| vlsm_type := X; vlsm_machine := X |}
  {|
    vlsm_type := X;
    vlsm_machine :=
      composite_vlsm composite_vlsm_induced_projection
        constraint
  |}
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
VLSM_incl
  {|
    vlsm_type := X;
    vlsm_machine :=
      composite_vlsm composite_vlsm_induced_projection
        constraint
  |} {| vlsm_type := X; vlsm_machine := X |}
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
VLSM_incl {| vlsm_type := X; vlsm_machine := X |}
  {|
    vlsm_type := X;
    vlsm_machine :=
      composite_vlsm composite_vlsm_induced_projection
        constraint
  |} apply basic_VLSM_strong_incl; [| | by intro..].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
strong_incl_initial_state_preservation X
  (composite_vlsm composite_vlsm_induced_projection
     constraint)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
strong_incl_initial_message_preservation X
  (composite_vlsm composite_vlsm_induced_projection
     constraint)
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
strong_incl_initial_state_preservation X
  (composite_vlsm composite_vlsm_induced_projection
     constraint) by intros s Hs i; specialize (Hs i).
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
strong_incl_initial_message_preservation X
  (composite_vlsm composite_vlsm_induced_projection
     constraint) intros ? (i & [im Him] & <-).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
im: message
Him: initial_message_prop im
initial_message_prop (`(im ↾ Him))
      assert (Him' : initial_message_prop (composite_vlsm_induced_projection i) im) by (left; done).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
im: message
Him, Him': initial_message_prop im
initial_message_prop (`(im ↾ Him))
      by exists i, (exist _ _ Him').
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
VLSM_incl
  {|
    vlsm_type := X;
    vlsm_machine :=
      composite_vlsm composite_vlsm_induced_projection
        constraint
  |} {| vlsm_type := X; vlsm_machine := X |} apply basic_VLSM_incl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
strong_incl_initial_state_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
weak_incl_initial_message_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
weak_incl_valid_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
weak_incl_transition_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
strong_incl_initial_state_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X by intros s Hs i; specialize (Hs i).
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
weak_incl_initial_message_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X intros _ _ m _ _ (i & [im [Him | HX]] & <-); [| done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
im: message
Him: initial_message_prop im
valid_message_prop
  {| vlsm_type := X; vlsm_machine := X |}
  (`(im ↾ or_introl Him))
      apply initial_message_is_valid.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
im: message
Him: initial_message_prop im
initial_message_prop (`(im ↾ or_introl Him))
      by exists i, (exist _ _ Him).
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
weak_incl_valid_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X by intros ? ? ? (_ & _ & ?).
    +message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
weak_incl_transition_preservation
  (composite_vlsm composite_vlsm_induced_projection
     constraint) X by intros ? ? ? ? ? [_ ?].
Qed.

End sec_projections.

VLSM Projection Traces

Section sec_preloaded_projection_traces.

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

(* The projection of a preloaded finite valid trace remains a preloaded valid trace. *)
Lemma preloaded_component_projection :
  VLSM_projection
    (preloaded_with_all_messages_vlsm (free_composite_vlsm IM))
    (preloaded_with_all_messages_vlsm (IM j))
    (composite_project_label IM j) (fun s => s j).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), s j)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), s j)
  apply basic_VLSM_projection_preloaded; intro; intros; [.. | done]
  ; destruct lX as [i li]
  ; unfold composite_project_label in H; cbn in H
  ; case_decide; inversion H; subst; clear H; cbn in *.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
i: index
li: label (IM i)
s: composite_state IM
om: option message
H0: valid li (s i, om)
valid li (s i, om)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
i: index
li: label (IM i)
s: composite_state IM
om: option message
s': composite_state IM
om': option message
H0: (let (si', om') := transition li (s i, om) in
 (state_update IM s i si', om')) = (
s', om')
transition li (s i, om) = (s' i, om')
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
H1: j ≠ i
s: composite_state IM
om: option message
s': composite_state IM
om': option message
H0: (let (si', om') := transition li (s i, om) in
 (state_update IM s i si', om')) = (
s', om')
s' j = s j
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
i: index
li: label (IM i)
s: composite_state IM
om: option message
H0: valid li (s i, om)
valid li (s i, om) apply H0.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
i: index
li: label (IM i)
s: composite_state IM
om: option message
s': composite_state IM
om': option message
H0: (let (si', om') := transition li (s i, om) in
 (state_update IM s i si', om')) = (
s', om')
transition li (s i, om) = (s' i, om') destruct (transition _ _ _) as [si' _om']
    ; inversion H0; subst; clear H0.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
i: index
li: label (IM i)
s: composite_state IM
om, om': option message
si': state (IM i)
(si', om') = (state_update IM s i si' i, om')
    by state_update_simpl.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
H1: j ≠ i
s: composite_state IM
om: option message
s': composite_state IM
om': option message
H0: (let (si', om') := transition li (s i, om) in
 (state_update IM s i si', om')) = (
s', om')
s' j = s j destruct (transition _ _ _) as [si' _om']
    ; inversion H0; subst; clear H0.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
H1: j ≠ i
s: composite_state IM
om, om': option message
si': state (IM i)
state_update IM s i si' j = s j
    by state_update_simpl.
Qed.

Definition composite_transition_item_projection_from_eq
  (item : composite_transition_item IM)
  (i := projT1 (l item))
  j
  (e : j = i)
  : transition_item (IM j)
  :=
  let lj := eq_rect_r _ (projT2 (l item)) e in
  Build_transition_item (IM j) lj (input item) (destination item j) (output item).

Definition composite_transition_item_projection
  (item : composite_transition_item IM)
  (i := projT1 (l item))
  : transition_item (IM i)
  :=
  composite_transition_item_projection_from_eq item i eq_refl.

Lemma composite_transition_item_projection_iff
  (item : composite_transition_item IM)
  (i := projT1 (l item))
  : pre_VLSM_projection_transition_item_project (composite_type IM) _
      (composite_project_label IM i) (fun s => s i)
      item
    = Some (composite_transition_item_projection item).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
item: composite_transition_item IM
i:= projT1 (l item): index
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM i)
  (composite_project_label IM i)
  (λ s : state (composite_type IM), s i) item =
Some (composite_transition_item_projection item)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
item: composite_transition_item IM
i:= projT1 (l item): index
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM i)
  (composite_project_label IM i)
  (λ s : state (composite_type IM), s i) item =
Some (composite_transition_item_projection item)
  destruct item.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
l: label (composite_type IM)
input: option message
destination: state (composite_type IM)
output: option message
i:= projT1
  (VLSM.l
     {|
       l := l;
       input := input;
       destination := destination;
       output := output
     |}): index
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM i)
  (composite_project_label IM i)
  (λ s : state (composite_type IM), s i)
  {|
    l := l;
    input := input;
    destination := destination;
    output := output
  |} =
Some
  (composite_transition_item_projection
     {|
       l := l;
       input := input;
       destination := destination;
       output := output
     |}) subst i.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
l: label (composite_type IM)
input: option message
destination: state (composite_type IM)
output: option message
pre_VLSM_projection_transition_item_project
  (composite_type IM)
  (IM
     (projT1
        (VLSM.l
           {|
             l := l;
             input := input;
             destination := destination;
             output := output
           |})))
  (composite_project_label IM
     (projT1
        (VLSM.l
           {|
             l := l;
             input := input;
             destination := destination;
             output := output
           |})))
  (λ s : state (composite_type IM),
     s
       (projT1
          (VLSM.l
             {|
               l := l;
               input := input;
               destination := destination;
               output := output
             |})))
  {|
    l := l;
    input := input;
    destination := destination;
    output := output
  |} =
Some
  (composite_transition_item_projection
     {|
       l := l;
       input := input;
       destination := destination;
       output := output
     |}) destruct l as (i, li).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
pre_VLSM_projection_transition_item_project
  (composite_type IM)
  (IM
     (projT1
        (l
           {|
             l := existT i li;
             input := input;
             destination := destination;
             output := output
           |})))
  (composite_project_label IM
     (projT1
        (l
           {|
             l := existT i li;
             input := input;
             destination := destination;
             output := output
           |})))
  (λ s : state (composite_type IM),
     s
       (projT1
          (l
             {|
               l := existT i li;
               input := input;
               destination := destination;
               output := output
             |})))
  {|
    l := existT i li;
    input := input;
    destination := destination;
    output := output
  |} =
Some
  (composite_transition_item_projection
     {|
       l := existT i li;
       input := input;
       destination := destination;
       output := output
     |})
  simpl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM i)
  (composite_project_label IM i)
  (λ s : composite_state IM, s i)
  {|
    l := existT i li;
    input := input;
    destination := destination;
    output := output
  |} =
Some
  (composite_transition_item_projection
     {|
       l := existT i li;
       input := input;
       destination := destination;
       output := output
     |}) unfold pre_VLSM_projection_transition_item_project, composite_project_label.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
match
  match
    decide
      (i =
       projT1
         (l
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |}))
  with
  | left e =>
      Some
        (eq_rect_r (λ n : index, label (IM n))
           (projT2
              (l
                 {|
                   l := existT i li;
                   input := input;
                   destination := destination;
                   output := output
                 |})) e)
  | right _ => None
  end
with
| Some lY =>
    Some
      {|
        l := lY;
        input :=
          VLSM.input
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |};
        destination :=
          VLSM.destination
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |} i;
        output :=
          VLSM.output
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |}
      |}
| None => None
end =
Some
  (composite_transition_item_projection
     {|
       l := existT i li;
       input := input;
       destination := destination;
       output := output
     |})
  simpl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
match
  match decide (i = i) with
  | left e =>
      Some
        (eq_rect_r (λ n : index, label (IM n)) li e)
  | right _ => None
  end
with
| Some lY =>
    Some
      {|
        l := lY;
        input := input;
        destination := destination i;
        output := output
      |}
| None => None
end =
Some
  (composite_transition_item_projection
     {|
       l := existT i li;
       input := input;
       destination := destination;
       output := output
     |})
  destruct (decide _); [| by congruence].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
e: i = i
Some
  {|
    l := eq_rect_r (λ n : index, label (IM n)) li e;
    input := input;
    destination := destination i;
    output := output
  |} =
Some
  (composite_transition_item_projection
     {|
       l := existT i li;
       input := input;
       destination := destination;
       output := output
     |})
  f_equal.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
e: i = i
{|
  l := eq_rect_r (λ n : index, label (IM n)) li e;
  input := input;
  destination := destination i;
  output := output
|} =
composite_transition_item_projection
  {|
    l := existT i li;
    input := input;
    destination := destination;
    output := output
  |} unfold composite_transition_item_projection, composite_transition_item_projection_from_eq.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
e: i = i
{|
  l := eq_rect_r (λ n : index, label (IM n)) li e;
  input := input;
  destination := destination i;
  output := output
|} =
{|
  l :=
    eq_rect_r (λ n : index, label (IM n))
      (projT2
         (l
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |})) eq_refl;
  input :=
    VLSM.input
      {|
        l := existT i li;
        input := input;
        destination := destination;
        output := output
      |};
  destination :=
    VLSM.destination
      {|
        l := existT i li;
        input := input;
        destination := destination;
        output := output
      |}
      (projT1
         (l
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |}));
  output :=
    VLSM.output
      {|
        l := existT i li;
        input := input;
        destination := destination;
        output := output
      |}
|}
  simpl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
e: i = i
{|
  l := eq_rect_r (λ n : index, label (IM n)) li e;
  input := input;
  destination := destination i;
  output := output
|} =
{|
  l :=
    eq_rect_r (λ n : index, label (IM n)) li eq_refl;
  input := input;
  destination := destination i;
  output := output
|}
  f_equal.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
e: i = i
eq_rect_r (λ n : index, label (IM n)) li e =
eq_rect_r (λ n : index, label (IM n)) li eq_refl
  replace e with (eq_refl (A := index) (x := i)); [done |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
e: i = i
eq_refl = e
  by apply Eqdep_dec.UIP_dec.
Qed.

Lemma composite_transition_item_projection_neq
  (item : composite_transition_item IM)
  (Hneq : j <> projT1 (l item))
  : pre_VLSM_projection_transition_item_project (composite_type IM) _
      (composite_project_label IM j) (fun s => s j)
      item
    = None.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
item: composite_transition_item IM
Hneq: j ≠ projT1 (l item)
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_type IM), s j) item = None
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
item: composite_transition_item IM
Hneq: j ≠ projT1 (l item)
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_type IM), s j) item = None
  destruct item.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
l: label (composite_type IM)
input: option message
destination: state (composite_type IM)
output: option message
Hneq: j
≠ projT1
    (VLSM.l
       {|
         l := l;
         input := input;
         destination := destination;
         output := output
       |})
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_type IM), s j)
  {|
    l := l;
    input := input;
    destination := destination;
    output := output
  |} = None destruct l as (i, li).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
Hneq: j
≠ projT1
    (l
       {|
         l := existT i li;
         input := input;
         destination := destination;
         output := output
       |})
pre_VLSM_projection_transition_item_project
  (composite_type IM) (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_type IM), s j)
  {|
    l := existT i li;
    input := input;
    destination := destination;
    output := output
  |} = None
  unfold pre_VLSM_projection_transition_item_project, composite_project_label.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: state (composite_type IM)
output: option message
Hneq: j
≠ projT1
    (l
       {|
         l := existT i li;
         input := input;
         destination := destination;
         output := output
       |})
match
  match
    decide
      (j =
       projT1
         (l
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |}))
  with
  | left e =>
      Some
        (eq_rect_r (λ n : index, label (IM n))
           (projT2
              (l
                 {|
                   l := existT i li;
                   input := input;
                   destination := destination;
                   output := output
                 |})) e)
  | right _ => None
  end
with
| Some lY =>
    Some
      {|
        l := lY;
        input :=
          VLSM.input
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |};
        destination :=
          VLSM.destination
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |} j;
        output :=
          VLSM.output
            {|
              l := existT i li;
              input := input;
              destination := destination;
              output := output
            |}
      |}
| None => None
end = None
  simpl in *.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j, i: index
li: label (IM i)
input: option message
destination: composite_state IM
output: option message
Hneq: j ≠ i
match
  match decide (j = i) with
  | left e =>
      Some
        (eq_rect_r (λ n : index, label (IM n)) li e)
  | right _ => None
  end
with
| Some lY =>
    Some
      {|
        l := lY;
        input := input;
        destination := destination j;
        output := output
      |}
| None => None
end = None
  by destruct (decide _).
Qed.

Definition finite_trace_projection_list (tr : list (composite_transition_item IM))
  : list (transition_item (IM j)) :=
  pre_VLSM_projection_finite_trace_project (composite_type IM) _
    (composite_project_label IM j) (fun s => s j) tr.

Lemma preloaded_valid_state_projection
  (s : state _)
  (Hps : constrained_state_prop (free_composite_vlsm IM) s)
  : constrained_state_prop (IM j) (s j).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hps: constrained_state_prop 
  (free_composite_vlsm IM) s
constrained_state_prop (IM j) (s j)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hps: constrained_state_prop 
  (free_composite_vlsm IM) s
constrained_state_prop (IM j) (s j)
  by apply (VLSM_projection_valid_state preloaded_component_projection).
Qed.

Lemma preloaded_finite_valid_trace_projection
  (s : composite_state IM)
  (trx : list (composite_transition_item IM))
  (Htr : finite_constrained_trace_from (free_composite_vlsm IM) s trx)
   : finite_constrained_trace_from (IM j) (s j)
      (VLSM_projection_finite_trace_project preloaded_component_projection trx).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s: composite_state IM
trx: list (composite_transition_item IM)
Htr: finite_constrained_trace_from
  (free_composite_vlsm IM) s trx
finite_constrained_trace_from (IM j) (s j)
  (VLSM_projection_finite_trace_project
     preloaded_component_projection trx)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s: composite_state IM
trx: list (composite_transition_item IM)
Htr: finite_constrained_trace_from
  (free_composite_vlsm IM) s trx
finite_constrained_trace_from (IM j) (s j)
  (VLSM_projection_finite_trace_project
     preloaded_component_projection trx)
  by apply (VLSM_projection_finite_valid_trace_from preloaded_component_projection).
Qed.

Lemma preloaded_finite_valid_trace_from_to_projection
  (s s' : composite_state IM)
  (trx : list (composite_transition_item IM))
  (Htr : finite_constrained_trace_from_to (free_composite_vlsm IM) s s' trx)
   : finite_constrained_trace_from_to (IM j) (s j) (s' j)
      (VLSM_projection_finite_trace_project preloaded_component_projection trx).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s, s': composite_state IM
trx: list (composite_transition_item IM)
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm IM) s s' trx
finite_constrained_trace_from_to (IM j) (s j) (s' j)
  (VLSM_projection_finite_trace_project
     preloaded_component_projection trx)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s, s': composite_state IM
trx: list (composite_transition_item IM)
Htr: finite_constrained_trace_from_to
  (free_composite_vlsm IM) s s' trx
finite_constrained_trace_from_to (IM j) (s j) (s' j)
  (VLSM_projection_finite_trace_project
     preloaded_component_projection trx)
  by apply (VLSM_projection_finite_valid_trace_from_to preloaded_component_projection).
Qed.

Lemma preloaded_finite_valid_trace_init_to_projection
  (s s' : composite_state IM)
  (trx : list (composite_transition_item IM))
  (Htr : finite_constrained_trace_init_to (free_composite_vlsm IM) s s' trx)
   : finite_constrained_trace_init_to (IM j) (s j) (s' j)
      (VLSM_projection_finite_trace_project preloaded_component_projection trx).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s, s': composite_state IM
trx: list (composite_transition_item IM)
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) s s' trx
finite_constrained_trace_init_to (IM j) (s j) (s' j)
  (VLSM_projection_finite_trace_project
     preloaded_component_projection trx)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s, s': composite_state IM
trx: list (composite_transition_item IM)
Htr: finite_constrained_trace_init_to
  (free_composite_vlsm IM) s s' trx
finite_constrained_trace_init_to (IM j) (s j) (s' j)
  (VLSM_projection_finite_trace_project
     preloaded_component_projection trx)
  by apply (VLSM_projection_finite_valid_trace_init_to preloaded_component_projection).
Qed.

Lemma preloaded_with_all_messages_projection_input_valid_transition_eq
  (s1 s2 : composite_state IM)
  (om1 om2 : option message)
  (l : label (free_composite_vlsm IM))
  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2))
  (Hl : projT1 l = j)
  : input_constrained_transition (IM (projT1 l))
      (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hl: projT1 l = j
input_constrained_transition (IM (projT1 l))
  (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hl: projT1 l = j
input_constrained_transition (IM (projT1 l))
  (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2)
  specialize
    (VLSM_projection_input_valid_transition preloaded_component_projection l) as Hivt.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hl: projT1 l = j
Hivt: ∀ lY : label
         (preloaded_with_all_messages_vlsm
            (IM j)),
  composite_project_label IM j l = Some lY
  → ∀ (s : state
             (preloaded_with_all_messages_vlsm
                (free_composite_vlsm IM))) 
      (im : option message) 
      (s' : state
              (preloaded_with_all_messages_vlsm
                 (free_composite_vlsm IM))) 
      (om : option message),
      input_valid_transition
        (preloaded_with_all_messages_vlsm
           (free_composite_vlsm IM)) l (
        s, im) (s', om)
      → input_valid_transition
          (preloaded_with_all_messages_vlsm
             (IM j)) lY
          ((λ s0 : state
                     (preloaded_with_all_messages_vlsm
                      (free_composite_vlsm IM)),
              s0 j) s, im)
          ((λ s0 : state
                     (preloaded_with_all_messages_vlsm
                      (free_composite_vlsm IM)),
              s0 j) s', om)
input_constrained_transition (IM (projT1 l))
  (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2)
  subst j.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hivt: ∀ lY : label
         (preloaded_with_all_messages_vlsm
            (IM (projT1 l))),
  composite_project_label IM (projT1 l) l =
  Some lY
  → ∀ (s : state
             (preloaded_with_all_messages_vlsm
                (free_composite_vlsm IM))) 
      (im : option message) 
      (s' : state
              (preloaded_with_all_messages_vlsm
                 (free_composite_vlsm IM))) 
      (om : option message),
      input_valid_transition
        (preloaded_with_all_messages_vlsm
           (free_composite_vlsm IM)) l (
        s, im) (s', om)
      → input_valid_transition
          (preloaded_with_all_messages_vlsm
             (IM (projT1 l))) lY
          (s (projT1 l), im)
          (s' (projT1 l), om)
input_constrained_transition (IM (projT1 l))
  (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2) specialize (Hivt (projT2 l)).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hivt: composite_project_label IM (projT1 l) l =
Some (projT2 l)
→ ∀ (s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM))) 
    (im : option message) 
    (s' : state
            (preloaded_with_all_messages_vlsm
               (free_composite_vlsm IM))) 
    (om : option message),
    input_valid_transition
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) l (
      s, im) (s', om)
    → input_valid_transition
        (preloaded_with_all_messages_vlsm
           (IM (projT1 l))) 
        (projT2 l) (s (projT1 l), im)
        (s' (projT1 l), om)
input_constrained_transition (IM (projT1 l))
  (projT2 l) (s1 (projT1 l), om1) (s2 (projT1 l), om2)
  apply Hivt; [| done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hivt: composite_project_label IM (projT1 l) l =
Some (projT2 l)
→ ∀ (s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM))) 
    (im : option message) 
    (s' : state
            (preloaded_with_all_messages_vlsm
               (free_composite_vlsm IM))) 
    (om : option message),
    input_valid_transition
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) l (
      s, im) (s', om)
    → input_valid_transition
        (preloaded_with_all_messages_vlsm
           (IM (projT1 l))) 
        (projT2 l) (s (projT1 l), im)
        (s' (projT1 l), om)
composite_project_label IM (projT1 l) l =
Some (projT2 l)
  unfold composite_project_label.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hivt: composite_project_label IM (projT1 l) l =
Some (projT2 l)
→ ∀ (s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM))) 
    (im : option message) 
    (s' : state
            (preloaded_with_all_messages_vlsm
               (free_composite_vlsm IM))) 
    (om : option message),
    input_valid_transition
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) l (
      s, im) (s', om)
    → input_valid_transition
        (preloaded_with_all_messages_vlsm
           (IM (projT1 l))) 
        (projT2 l) (s (projT1 l), im)
        (s' (projT1 l), om)
match decide (projT1 l = projT1 l) with
| left e =>
    Some
      (eq_rect_r (λ n : index, label (IM n))
         (projT2 l) e)
| right _ => None
end = Some (projT2 l) destruct (decide _); [| by elim n].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hivt: composite_project_label IM (projT1 l) l =
Some (projT2 l)
→ ∀ (s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM))) 
    (im : option message) 
    (s' : state
            (preloaded_with_all_messages_vlsm
               (free_composite_vlsm IM))) 
    (om : option message),
    input_valid_transition
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) l (
      s, im) (s', om)
    → input_valid_transition
        (preloaded_with_all_messages_vlsm
           (IM (projT1 l))) 
        (projT2 l) (s (projT1 l), im)
        (s' (projT1 l), om)
e: projT1 l = projT1 l
Some
  (eq_rect_r (λ n : index, label (IM n)) (projT2 l) e) =
Some (projT2 l)
  replace e with (eq_refl (A := index) (x := projT1 l)); [done |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
Hivt: composite_project_label IM (projT1 l) l =
Some (projT2 l)
→ ∀ (s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM))) 
    (im : option message) 
    (s' : state
            (preloaded_with_all_messages_vlsm
               (free_composite_vlsm IM))) 
    (om : option message),
    input_valid_transition
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM)) l (
      s, im) (s', om)
    → input_valid_transition
        (preloaded_with_all_messages_vlsm
           (IM (projT1 l))) 
        (projT2 l) (s (projT1 l), im)
        (s' (projT1 l), om)
e: projT1 l = projT1 l
eq_refl = e
  by apply Eqdep_dec.UIP_dec.
Qed.

Lemma preloaded_with_all_messages_projection_input_valid_transition_neq
  [s1 s2 : composite_state IM]
  [om1 om2 : option message]
  [l : label (free_composite_vlsm IM)]
  (Ht : input_constrained_transition (free_composite_vlsm IM) l (s1, om1) (s2, om2))
  [i : index]
  (Hi : i <> projT1 l)
  : s1 i = s2 i.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
i: index
Hi: i ≠ projT1 l
s1 i = s2 i
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Ht: input_constrained_transition
  (free_composite_vlsm IM) l (
  s1, om1) (s2, om2)
i: index
Hi: i ≠ projT1 l
s1 i = s2 i
  destruct Ht as [[Hs1 [Hom1 Hv]] Ht]; cbn in Hv, Ht.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
l: label (free_composite_vlsm IM)
Hs1: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) s1
Hom1: option_valid_message_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) om1
Hv: let (i, li) := l in valid li (s1 i, om1)
Ht: (let (i, li) := l in
 let (si', om') := transition li (s1 i, om1) in
 (state_update IM s1 i si', om')) = (
s2, om2)
i: index
Hi: i ≠ projT1 l
s1 i = s2 i
  destruct l as [il l].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
il: index
l: label (IM il)
Hs1: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) s1
Hom1: option_valid_message_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) om1
Hv: valid l (s1 il, om1)
Ht: (let (si', om') := transition l (s1 il, om1) in
 (state_update IM s1 il si', om')) = (
s2, om2)
i: index
Hi: i ≠ projT1 (existT il l)
s1 i = s2 i
  destruct (transition _ _ _) as (si', om') eqn: Htj.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1, s2: composite_state IM
om1, om2: option message
il: index
l: label (IM il)
Hs1: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) s1
Hom1: option_valid_message_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) om1
Hv: valid l (s1 il, om1)
si': state (IM il)
om': option message
Htj: transition l (s1 il, om1) = (si', om')
Ht: (state_update IM s1 il si', om') = (s2, om2)
i: index
Hi: i ≠ projT1 (existT il l)
s1 i = s2 i
  inversion Ht; subst; clear Ht.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
j: index
s1: composite_state IM
om1, om2: option message
il: index
l: label (IM il)
Hs1: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) s1
Hom1: option_valid_message_prop
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) om1
Hv: valid l (s1 il, om1)
si': state (IM il)
Htj: transition l (s1 il, om1) = (si', om2)
i: index
Hi: i ≠ projT1 (existT il l)
s1 i = state_update IM s1 il si' i
  by state_update_simpl.
Qed.

End sec_preloaded_projection_traces.

Section sec_projection_traces_membership.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (constraint : composite_label IM -> composite_state IM * option message -> Prop)
  (X := composite_vlsm IM constraint)
  .

Lemma finite_trace_projection_list_in
  (tr : list (composite_transition_item IM))
  (itemX : composite_transition_item IM)
  (HitemX : itemX ∈ tr)
  (j := projT1 (l itemX)) :
    Build_transition_item (IM j) (projT2 (l itemX)) (input itemX) (destination itemX j)
      (output itemX)
      ∈
    VLSM_projection_finite_trace_project (preloaded_component_projection IM j) tr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
itemX: composite_transition_item IM
HitemX: itemX ∈ tr
j:= projT1 (l itemX): index
{|
  l := projT2 (l itemX);
  input := input itemX;
  destination := destination itemX j;
  output := output itemX
|}
∈ VLSM_projection_finite_trace_project
    (preloaded_component_projection IM j) tr
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
itemX: composite_transition_item IM
HitemX: itemX ∈ tr
j:= projT1 (l itemX): index
{|
  l := projT2 (l itemX);
  input := input itemX;
  destination := destination itemX j;
  output := output itemX
|}
∈ VLSM_projection_finite_trace_project
    (preloaded_component_projection IM j) tr
  apply elem_of_list_omap.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
itemX: composite_transition_item IM
HitemX: itemX ∈ tr
j:= projT1 (l itemX): index
∃ x : transition_item,
  x ∈ tr
  ∧ pre_VLSM_projection_transition_item_project
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM))
      (preloaded_with_all_messages_vlsm (IM j))
      (composite_project_label IM j)
      (λ s : state
               (preloaded_with_all_messages_vlsm
                  (free_composite_vlsm IM)), s j) x =
    Some
      {|
        l := projT2 (l itemX);
        input := input itemX;
        destination := destination itemX j;
        output := output itemX
      |}
  exists itemX; split; [done |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
itemX: composite_transition_item IM
HitemX: itemX ∈ tr
j:= projT1 (l itemX): index
pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), s j) itemX =
Some
  {|
    l := projT2 (l itemX);
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |}
  unfold pre_VLSM_projection_transition_item_project, composite_project_label; subst j.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
itemX: composite_transition_item IM
HitemX: itemX ∈ tr
match
  match
    decide (projT1 (l itemX) = projT1 (l itemX))
  with
  | left e =>
      Some
        (eq_rect_r (λ n : index, label (IM n))
           (projT2 (l itemX)) e)
  | right _ => None
  end
with
| Some lY =>
    Some
      {|
        l := lY;
        input := input itemX;
        destination :=
          destination itemX (projT1 (l itemX));
        output := output itemX
      |}
| None => None
end =
Some
  {|
    l := projT2 (l itemX);
    input := input itemX;
    destination :=
      destination itemX (projT1 (l itemX));
    output := output itemX
  |}
  case_decide; [| by elim H].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
itemX: composite_transition_item IM
HitemX: itemX ∈ tr
H: projT1 (l itemX) = projT1 (l itemX)
Some
  {|
    l :=
      eq_rect_r (λ n : index, label (IM n))
        (projT2 (l itemX)) H;
    input := input itemX;
    destination :=
      destination itemX (projT1 (l itemX));
    output := output itemX
  |} =
Some
  {|
    l := projT2 (l itemX);
    input := input itemX;
    destination :=
      destination itemX (projT1 (l itemX));
    output := output itemX
  |}
  replace H with (eq_refl (A := index) (x := projT1 (l itemX))); [done |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
itemX: composite_transition_item IM
HitemX: itemX ∈ tr
H: projT1 (l itemX) = projT1 (l itemX)
eq_refl = H
  by apply Eqdep_dec.UIP_dec.
Qed.

Lemma finite_trace_projection_list_in_rev
  (tr : list (composite_transition_item IM))
  (j : index)
  (itemj : transition_item (IM j))
  (Hitemj : itemj ∈ VLSM_projection_finite_trace_project (preloaded_component_projection IM j) tr)
  : exists (itemX : composite_transition_item IM), itemX ∈ tr /\
    output itemX = output itemj /\
    input itemX = input itemj /\
    destination itemX j = destination itemj /\
    exists (Hl1 : j = projT1 (l itemX)),
    eq_rect_r _ (projT2 (l itemX)) Hl1 = l itemj.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj: transition_item
Hitemj: itemj
∈ VLSM_projection_finite_trace_project
    (preloaded_component_projection IM j) tr
∃ itemX : composite_transition_item IM,
  itemX ∈ tr
  ∧ output itemX = output itemj
    ∧ input itemX = input itemj
      ∧ destination itemX j = destination itemj
        ∧ (∃ Hl1 : j = projT1 (l itemX),
             eq_rect_r (λ n : index, label (IM n))
               (projT2 (l itemX)) Hl1 = l itemj)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj: transition_item
Hitemj: itemj
∈ VLSM_projection_finite_trace_project
    (preloaded_component_projection IM j) tr
∃ itemX : composite_transition_item IM,
  itemX ∈ tr
  ∧ output itemX = output itemj
    ∧ input itemX = input itemj
      ∧ destination itemX j = destination itemj
        ∧ (∃ Hl1 : j = projT1 (l itemX),
             eq_rect_r (λ n : index, label (IM n))
               (projT2 (l itemX)) Hl1 = l itemj)
  apply elem_of_list_omap in Hitemj as [itemX [HitemX HitemX_pr]].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj, itemX: transition_item
HitemX: itemX ∈ tr
HitemX_pr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)),
     s j) itemX = Some itemj
∃ itemX : composite_transition_item IM,
  itemX ∈ tr
  ∧ output itemX = output itemj
    ∧ input itemX = input itemj
      ∧ destination itemX j = destination itemj
        ∧ (∃ Hl1 : j = projT1 (l itemX),
             eq_rect_r (λ n : index, label (IM n))
               (projT2 (l itemX)) Hl1 = l itemj)
  exists itemX.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj, itemX: transition_item
HitemX: itemX ∈ tr
HitemX_pr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)),
     s j) itemX = Some itemj
itemX ∈ tr
∧ output itemX = output itemj
  ∧ input itemX = input itemj
    ∧ destination itemX j = destination itemj
      ∧ (∃ Hl1 : j = projT1 (l itemX),
           eq_rect_r (λ n : index, label (IM n))
             (projT2 (l itemX)) Hl1 = l itemj) split; [done |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj, itemX: transition_item
HitemX: itemX ∈ tr
HitemX_pr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)),
     s j) itemX = Some itemj
output itemX = output itemj
∧ input itemX = input itemj
  ∧ destination itemX j = destination itemj
    ∧ (∃ Hl1 : j = projT1 (l itemX),
         eq_rect_r (λ n : index, label (IM n))
           (projT2 (l itemX)) Hl1 = l itemj)
  unfold pre_VLSM_projection_transition_item_project in HitemX_pr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj, itemX: transition_item
HitemX: itemX ∈ tr
HitemX_pr: match
  composite_project_label IM j (l itemX)
with
| Some lY =>
    Some
      {|
        l := lY;
        input := input itemX;
        destination := destination itemX j;
        output := output itemX
      |}
| None => None
end = Some itemj
output itemX = output itemj
∧ input itemX = input itemj
  ∧ destination itemX j = destination itemj
    ∧ (∃ Hl1 : j = projT1 (l itemX),
         eq_rect_r (λ n : index, label (IM n))
           (projT2 (l itemX)) Hl1 = l itemj)
  destruct (composite_project_label _ _ _) as [lY |] eqn: Hly; [| by congruence].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj, itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
Hly: composite_project_label IM j (l itemX) = Some lY
HitemX_pr: Some
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |} = Some itemj
output itemX = output itemj
∧ input itemX = input itemj
  ∧ destination itemX j = destination itemj
    ∧ (∃ Hl1 : j = projT1 (l itemX),
         eq_rect_r (λ n : index, label (IM n))
           (projT2 (l itemX)) Hl1 = l itemj)
  inversion HitemX_pr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemj, itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
Hly: composite_project_label IM j (l itemX) = Some lY
HitemX_pr: Some
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |} = Some itemj
H0: {|
  l := lY;
  input := input itemX;
  destination := destination itemX j;
  output := output itemX
|} = itemj
output itemX =
output
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |}
∧ input itemX =
  input
    {|
      l := lY;
      input := input itemX;
      destination := destination itemX j;
      output := output itemX
    |}
  ∧ destination itemX j =
    destination
      {|
        l := lY;
        input := input itemX;
        destination := destination itemX j;
        output := output itemX
      |}
    ∧ (∃ Hl1 : j = projT1 (l itemX),
         eq_rect_r (λ n : index, label (IM n))
           (projT2 (l itemX)) Hl1 =
         l
           {|
             l := lY;
             input := input itemX;
             destination := destination itemX j;
             output := output itemX
           |}) subst.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
Hly: composite_project_label IM j (l itemX) = Some lY
HitemX_pr: Some
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |} =
Some
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |}
output itemX =
output
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |}
∧ input itemX =
  input
    {|
      l := lY;
      input := input itemX;
      destination := destination itemX j;
      output := output itemX
    |}
  ∧ destination itemX j =
    destination
      {|
        l := lY;
        input := input itemX;
        destination := destination itemX j;
        output := output itemX
      |}
    ∧ (∃ Hl1 : j = projT1 (l itemX),
         eq_rect_r (λ n : index, label (IM n))
           (projT2 (l itemX)) Hl1 =
         l
           {|
             l := lY;
             input := input itemX;
             destination := destination itemX j;
             output := output itemX
           |}) clear HitemX_pr.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
Hly: composite_project_label IM j (l itemX) = Some lY
output itemX =
output
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |}
∧ input itemX =
  input
    {|
      l := lY;
      input := input itemX;
      destination := destination itemX j;
      output := output itemX
    |}
  ∧ destination itemX j =
    destination
      {|
        l := lY;
        input := input itemX;
        destination := destination itemX j;
        output := output itemX
      |}
    ∧ (∃ Hl1 : j = projT1 (l itemX),
         eq_rect_r (λ n : index, label (IM n))
           (projT2 (l itemX)) Hl1 =
         l
           {|
             l := lY;
             input := input itemX;
             destination := destination itemX j;
             output := output itemX
           |})
  repeat split.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
Hly: composite_project_label IM j (l itemX) = Some lY
∃ Hl1 : j = projT1 (l itemX),
  eq_rect_r (λ n : index, label (IM n))
    (projT2 (l itemX)) Hl1 =
  l
    {|
      l := lY;
      input := input itemX;
      destination := destination itemX j;
      output := output itemX
    |}
  unfold composite_project_label in Hly.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
Hly: match decide (j = projT1 (l itemX)) with
| left e =>
    Some
      (eq_rect_r (λ n : index, label (IM n))
         (projT2 (l itemX)) e)
| right _ => None
end = Some lY
∃ Hl1 : j = projT1 (l itemX),
  eq_rect_r (λ n : index, label (IM n))
    (projT2 (l itemX)) Hl1 =
  l
    {|
      l := lY;
      input := input itemX;
      destination := destination itemX j;
      output := output itemX
    |}
  case_decide; [| by congruence].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
H: j = projT1 (l itemX)
Hly: Some
  (eq_rect_r (λ n : index, label (IM n))
     (projT2 (l itemX)) H) = 
Some lY
∃ Hl1 : j = projT1 (l itemX),
  eq_rect_r (λ n : index, label (IM n))
    (projT2 (l itemX)) Hl1 =
  l
    {|
      l := lY;
      input := input itemX;
      destination := destination itemX j;
      output := output itemX
    |}
  exists H.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
tr: list (composite_transition_item IM)
j: index
itemX: transition_item
HitemX: itemX ∈ tr
lY: label (IM j)
H: j = projT1 (l itemX)
Hly: Some
  (eq_rect_r (λ n : index, label (IM n))
     (projT2 (l itemX)) H) = 
Some lY
eq_rect_r (λ n : index, label (IM n))
  (projT2 (l itemX)) H =
l
  {|
    l := lY;
    input := input itemX;
    destination := destination itemX j;
    output := output itemX
  |}
  by inversion Hly.
Qed.

End sec_projection_traces_membership.

Section sec_binary_free_composition_projections.

Projections of Free composition of two VLSMs

This projections are used in defining the byzantine_trace_properties.

Context
  {message : Type}
  (M1 M2 : VLSM message)
  .

Definition binary_free_composition_fst : VLSM message :=
  pre_composite_vlsm_induced_projection_validator (binary_IM M1 M2)
    (free_constraint (binary_IM M1 M2)) first.

Definition binary_free_composition_snd : VLSM message :=
  pre_composite_vlsm_induced_projection_validator (binary_IM M1 M2)
    (free_constraint (binary_IM M1 M2)) second.

End sec_binary_free_composition_projections.

Section sec_fixed_projection.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (constraint : composite_label IM -> composite_state IM * option message -> Prop)
  (X := composite_vlsm IM constraint)
  .

Projection traces are Byzantine

Let us fix an index j and let Xj be the projection of X on component j.

In this section we establish some basic properties for projections, building up to Lemma proj_preloaded_with_all_messages_incl, which guarantees that all valid_traces of Xj are also valid_traces for the preloaded_with_all_messages_vlsm associated to the component IM j. In particular this ensures that the byzantine traces of IM j include all valid_traces of Xj (see Lemma preloaded_with_all_messages_alt_eq).

Context
  (j : index)
  (Xj := pre_composite_vlsm_induced_projection_validator IM constraint j)
  .

Lemma projection_valid_input_valid
  (l : label Xj)
  (som : state Xj * option message)
  (Hv : valid Xj l som)
  : input_valid Xj l som.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
som: (state Xj * option message)%type
Hv: valid l som
input_valid Xj l som
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
som: (state Xj * option message)%type
Hv: valid l som
input_valid Xj l som
  destruct som as (s, om).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
input_valid Xj l (s, om)
  destruct (id Hv) as [sX [Hsi [Hps [Hopm _]]]]; subst.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
sX: state (composite_vlsm IM constraint)
Hv: valid l (sX j, om)
Hps: valid_state_prop (composite_vlsm IM constraint)
  sX
Hopm: option_valid_message_prop
  (composite_vlsm IM constraint) om
input_valid Xj l (sX j, om)
  repeat split; [| | done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
sX: state (composite_vlsm IM constraint)
Hv: valid l (sX j, om)
Hps: valid_state_prop (composite_vlsm IM constraint)
  sX
Hopm: option_valid_message_prop
  (composite_vlsm IM constraint) om
valid_state_prop Xj (sX j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
sX: state (composite_vlsm IM constraint)
Hv: valid l (sX j, om)
Hps: valid_state_prop (composite_vlsm IM constraint)
  sX
Hopm: option_valid_message_prop
  (composite_vlsm IM constraint) om
option_valid_message_prop Xj om
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
sX: state (composite_vlsm IM constraint)
Hv: valid l (sX j, om)
Hps: valid_state_prop (composite_vlsm IM constraint)
  sX
Hopm: option_valid_message_prop
  (composite_vlsm IM constraint) om
valid_state_prop Xj (sX j) by eapply (VLSM_projection_valid_state (component_projection _ constraint j)).
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
sX: state (composite_vlsm IM constraint)
Hv: valid l (sX j, om)
Hps: valid_state_prop (composite_vlsm IM constraint)
  sX
Hopm: option_valid_message_prop
  (composite_vlsm IM constraint) om
option_valid_message_prop Xj om by apply any_message_is_valid_in_preloaded.
Qed.

Lemma projection_valid_implies_composition_valid_message
  (l : label Xj)
  (s : state Xj)
  (om : option message)
  (Hv : valid Xj l (s, om))
  : option_valid_message_prop X om.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
option_valid_message_prop X om
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
option_valid_message_prop X om
  by destruct Hv as (sx & Hs & HpsX & HpmX & Hv).
Qed.

Lemma projection_valid_implies_projection_valid_state
  (lj : label Xj)
  (sj : state Xj)
  (om : option message)
  (Hv : valid Xj lj (sj, om))
  : valid_state_prop Xj sj.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
lj: label Xj
sj: state Xj
om: option message
Hv: valid lj (sj, om)
valid_state_prop Xj sj
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
lj: label Xj
sj: state Xj
om: option message
Hv: valid lj (sj, om)
valid_state_prop Xj sj
  by destruct Hv as (s & <- & Hs & _)
  ; eapply (VLSM_projection_valid_state (component_projection _ constraint j)).
Qed.

Lemma projection_valid_implies_projection_valid_state_message_outputs
    (l : label Xj)
    (s : state Xj)
    (om : option message)
    (Hv : valid Xj l (s, om))
    s' om'
    (Ht : transition (IM j) l (s, om) = (s', om'))
    : valid_state_message_prop Xj s' om'.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
valid_state_message_prop Xj s' om'
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
valid_state_message_prop Xj s' om'
  apply projection_valid_implies_projection_valid_state in Hv as Hs.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
Hs: valid_state_prop Xj s
valid_state_message_prop Xj s' om'
  destruct Hs as [? Hs].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
x: option message
Hs: valid_state_message_prop Xj s x
valid_state_message_prop Xj s' om'
  eapply (valid_generated_state_message Xj s x Hs (` (vs0 (IM j)))); [| done..].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
x: option message
Hs: valid_state_message_prop Xj s x
valid_state_message_prop Xj (`(vs0 (IM j))) om
  apply valid_initial_state_message.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
x: option message
Hs: valid_state_message_prop Xj s x
initial_state_prop (`(vs0 (IM j)))
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
x: option message
Hs: valid_state_message_prop Xj s x
option_initial_message_prop Xj om
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
x: option message
Hs: valid_state_message_prop Xj s x
initial_state_prop (`(vs0 (IM j))) by destruct (vs0 (IM j)); cbn.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
x: option message
Hs: valid_state_message_prop Xj s x
option_initial_message_prop Xj om by destruct om; cbn; [right |].
Qed.

Lemma projection_valid_implies_destination_projection_valid_state
    (l : label Xj)
    (s : state Xj)
    (om : option message)
    (Hv : valid Xj l (s, om))
    s' om'
    (Ht : transition (IM j) l (s, om) = (s', om'))
    : valid_state_prop Xj s'.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
valid_state_prop Xj s'
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
valid_state_prop Xj s'
  by eexists; eapply projection_valid_implies_projection_valid_state_message_outputs.
Qed.

Lemma projection_valid_implies_destination_projection_valid_message
    (l : label Xj)
    (s : state Xj)
    (om : option message)
    (Hv : valid Xj l (s, om))
    s' om'
    (Ht : transition (IM j) l (s, om) = (s', om'))
    : option_valid_message_prop Xj om'.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
option_valid_message_prop Xj om'
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
s: state Xj
om: option message
Hv: valid l (s, om)
s': state (IM j)
om': option message
Ht: transition l (s, om) = (s', om')
option_valid_message_prop Xj om'
  by eexists; eapply projection_valid_implies_projection_valid_state_message_outputs.
Qed.

Interestingly enough, Xj cannot produce any additional messages than the initial ones available from X.

Lemma valid_message_projection_rev :
  forall m, can_emit Xj m -> can_emit X m.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
∀ m : message, can_emit Xj m → can_emit X m
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
∀ m : message, can_emit Xj m → can_emit X m
  intros m ((sj, om) & lj & sj' & (_ & _ & s & <- & Hv) & Ht).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
m: message
om: option message
lj: label Xj
sj': state Xj
s: state (composite_vlsm IM constraint)
Hv: input_valid (composite_vlsm IM constraint)
  (existT j lj) (s, om)
Ht: transition lj (s j, om) = (sj', Some m)
can_emit X m
  eexists _, _, (state_update IM s j sj'); split; [done |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
m: message
om: option message
lj: label Xj
sj': state Xj
s: state (composite_vlsm IM constraint)
Hv: input_valid (composite_vlsm IM constraint)
  (existT j lj) (s, om)
Ht: transition lj (s j, om) = (sj', Some m)
transition (existT j lj) (s, om) =
(state_update IM s j sj', Some m)
  by cbn in *; replace (transition _ _ _) with (sj', Some m).
Qed.

As a stepping stone towards proving trace inclusion between Xj and the preloaded_with_all_messages_vlsm associated to IM j, we prove that the valid_state_message_property is transferred.

Lemma proj_preloaded_with_all_messages_valid_state_message_preservation
  (s : state Xj)
  (om : option message)
  (Hps : valid_state_message_prop Xj s om)
  : constrained_state_message_prop (IM j) s om.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state Xj
om: option message
Hps: valid_state_message_prop Xj s om
constrained_state_message_prop (IM j) s om
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state Xj
om: option message
Hps: valid_state_message_prop Xj s om
constrained_state_message_prop (IM j) s om
  induction Hps.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state Xj
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop Xj om
constrained_state_message_prop (IM j) s om
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state Xj
_om: option message
Hps1: valid_state_message_prop Xj s _om
_s: state Xj
om: option message
Hps2: valid_state_message_prop Xj _s om
l: label Xj
Hv: valid l (s, om)
s': state Xj
om': option message
Ht: transition l (s, om) = (s', om')
IHHps1: constrained_state_message_prop (IM j) s _om
IHHps2: constrained_state_message_prop (IM j) _s om
constrained_state_message_prop (IM j) s' om'
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state Xj
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop Xj om
constrained_state_message_prop (IM j) s om by apply valid_initial_state_message; [| destruct om].
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state Xj
_om: option message
Hps1: valid_state_message_prop Xj s _om
_s: state Xj
om: option message
Hps2: valid_state_message_prop Xj _s om
l: label Xj
Hv: valid l (s, om)
s': state Xj
om': option message
Ht: transition l (s, om) = (s', om')
IHHps1: constrained_state_message_prop (IM j) s _om
IHHps2: constrained_state_message_prop (IM j) _s om
constrained_state_message_prop (IM j) s' om' apply (valid_generated_state_message (preloaded_with_all_messages_vlsm (IM j)))
      with s _om _s om l; [done.. | | done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state Xj
_om: option message
Hps1: valid_state_message_prop Xj s _om
_s: state Xj
om: option message
Hps2: valid_state_message_prop Xj _s om
l: label Xj
Hv: valid l (s, om)
s': state Xj
om': option message
Ht: transition l (s, om) = (s', om')
IHHps1: constrained_state_message_prop (IM j) s _om
IHHps2: constrained_state_message_prop (IM j) _s om
valid l (s, om)
    by cbn; eapply (projection_valid_implies_valid IM), Hv.
Qed.

We can now finally prove the main result for this section.

Lemma proj_preloaded_with_all_messages_incl :
  VLSM_incl Xj (preloaded_with_all_messages_vlsm (IM j)).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_incl Xj (preloaded_with_all_messages_vlsm (IM j))
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_incl Xj (preloaded_with_all_messages_vlsm (IM j))
  apply (basic_VLSM_incl Xj); intro; intros.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
H: initial_state_prop s
initial_state_prop (id s)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label {| vlsm_type := Xj; vlsm_machine := Xj |}
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
m: message
Hv: input_valid
  {| vlsm_type := Xj; vlsm_machine := Xj |} l
  (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |} m
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label {| vlsm_type := Xj; vlsm_machine := Xj |}
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
om: option message
Hv: input_valid
  {| vlsm_type := Xj; vlsm_machine := Xj |} l
  (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |} om
valid (id l) (id s, om)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label {| vlsm_type := Xj; vlsm_machine := Xj |}
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
om: option message
s': state {| vlsm_type := Xj; vlsm_machine := Xj |}
om': option message
H: input_valid_transition
  {| vlsm_type := Xj; vlsm_machine := Xj |} l
  (s, om) (s', om')
transition (id l) (id s, om) = (id s', om')
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
H: initial_state_prop s
initial_state_prop (id s) done.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label {| vlsm_type := Xj; vlsm_machine := Xj |}
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
m: message
Hv: input_valid
  {| vlsm_type := Xj; vlsm_machine := Xj |} l
  (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine (IM j)
        (λ _ : message, True)
  |} m by apply initial_message_is_valid.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label {| vlsm_type := Xj; vlsm_machine := Xj |}
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
om: option message
Hv: input_valid
  {| vlsm_type := Xj; vlsm_machine := Xj |} l
  (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := Xj;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |} om
valid (id l) (id s, om) by cbn; eapply (projection_valid_implies_valid IM), Hv.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label {| vlsm_type := Xj; vlsm_machine := Xj |}
s: state {| vlsm_type := Xj; vlsm_machine := Xj |}
om: option message
s': state {| vlsm_type := Xj; vlsm_machine := Xj |}
om': option message
H: input_valid_transition
  {| vlsm_type := Xj; vlsm_machine := Xj |} l
  (s, om) (s', om')
transition (id l) (id s, om) = (id s', om') by apply H.
Qed.

Lemma component_projection_to_preloaded :
  VLSM_projection X (preloaded_with_all_messages_vlsm (IM j))
    (composite_project_label IM j) (fun s => s j).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_projection X
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j) (λ s : state X, s j)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_projection X
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j) (λ s : state X, s j)
  eapply VLSM_projection_incl_trans.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_projection X
  {| vlsm_type := IM j; vlsm_machine := ?MY |}
  (composite_project_label IM j) (λ s : state X, s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_incl {| vlsm_type := IM j; vlsm_machine := ?MY |}
  {|
    vlsm_type := IM j;
    vlsm_machine :=
      preloaded_vlsm_machine 
        (IM j) (λ _ : message, True)
  |}
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_projection X
  {| vlsm_type := IM j; vlsm_machine := ?MY |}
  (composite_project_label IM j) (λ s : state X, s j) by apply component_projection.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
VLSM_incl
  {|
    vlsm_type := IM j;
    vlsm_machine :=
      preloaded_vlsm_machine
        (composite_vlsm_induced_projection_validator
           IM constraint j) (λ _ : message, True)
  |}
  {|
    vlsm_type := IM j;
    vlsm_machine :=
      preloaded_vlsm_machine (IM j)
        (λ _ : message, True)
  |} by apply proj_preloaded_with_all_messages_incl.
Qed.

We say that the component j of X is a validator for received messages if if validity in the component (for reachable states) implies validity in the composite_vlsm_induced_projection_validator.

Definition component_projection_validator_prop :=
  forall (lj : label (IM j)) (sj : state (IM j)) (omi : option message),
    input_constrained (IM j) lj (sj, omi) ->
    valid Xj lj (sj, omi).

Lemma component_projection_validator_prop_is_induced
  : component_projection_validator_prop <->
    @projection_validator_prop _ X (IM j) (composite_project_label IM j) (fun s => s j).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
component_projection_validator_prop
↔ projection_validator_prop (IM j)
    (composite_project_label IM j)
    (λ s : state X, s j)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
component_projection_validator_prop
↔ projection_validator_prop (IM j)
    (composite_project_label IM j)
    (λ s : state X, s j)
  split; intros Hvalidator li si omi Hvi.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
li: label (preloaded_with_all_messages_vlsm (IM j))
si: state (preloaded_with_all_messages_vlsm (IM j))
omi: option message
Hvi: input_constrained (IM j) li (si, omi)
∃ (lX : label X) (sX : state X),
  InputValidation (composite_project_label IM j)
    (λ s : state X, s j) li si omi lX sX
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: projection_validator_prop 
  (IM j) (composite_project_label IM j)
  (λ s : state X, s j)
li: label (IM j)
si: state (IM j)
omi: option message
Hvi: input_constrained (IM j) li (si, omi)
valid li (si, omi)
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
li: label (preloaded_with_all_messages_vlsm (IM j))
si: state (preloaded_with_all_messages_vlsm (IM j))
omi: option message
Hvi: input_constrained (IM j) li (si, omi)
∃ (lX : label X) (sX : state X),
  InputValidation (composite_project_label IM j)
    (λ s : state X, s j) li si omi lX sX apply Hvalidator in Hvi as (sX & <- & Hv).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
li: label (preloaded_with_all_messages_vlsm (IM j))
omi: option message
sX: state (composite_vlsm IM constraint)
Hv: input_valid (composite_vlsm IM constraint)
  (existT j li) (sX, omi)
∃ (lX : label X) (sX0 : state X),
  InputValidation (composite_project_label IM j)
    (λ s : state X, s j) li (sX j) omi lX sX0
    by eexists (existT j li), sX; split; [apply composite_project_label_eq | ..].
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: projection_validator_prop 
  (IM j) (composite_project_label IM j)
  (λ s : state X, s j)
li: label (IM j)
si: state (IM j)
omi: option message
Hvi: input_constrained (IM j) li (si, omi)
valid li (si, omi) apply Hvalidator in Hvi as ([i _li] & sX & []).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: projection_validator_prop 
  (IM j) (composite_project_label IM j)
  (λ s : state X, s j)
li: label (IM j)
si: state (IM j)
omi: option message
i: index
_li: label (IM i)
sX: state X
tiv_label_project: composite_project_label IM j
  (existT i _li) = Some li
tiv_state_project: sX j = si
lifted_transition_input_valid: input_valid X
  (existT i _li)
  (sX, omi)
valid li (si, omi)
    unfold composite_project_label in tiv_label_project; case_decide; [subst; cbn in * | done].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
_li, li: label (IM i)
Hvalidator: projection_validator_prop 
  (IM i) (composite_project_label IM i)
  (λ s : composite_state IM, s i)
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint i: VLSM message
omi: option message
sX: composite_state IM
tiv_label_project: Some _li = Some li
lifted_transition_input_valid: valid_state_prop X sX
∧ option_valid_message_prop
    X omi
  ∧ valid _li
      (sX i, omi)
    ∧ constraint
        (existT i _li)
        (sX, omi)
∃ s : composite_state IM,
  s i = sX i
  ∧ valid_state_prop (composite_vlsm IM constraint) s
    ∧ option_valid_message_prop
        (composite_vlsm IM constraint) omi
      ∧ valid li (s i, omi)
        ∧ constraint (existT i li) (s, omi)
    apply Some_inj in tiv_label_project; subst _li.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
i: index
li: label (IM i)
Hvalidator: projection_validator_prop 
  (IM i) (composite_project_label IM i)
  (λ s : composite_state IM, s i)
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint i: VLSM message
omi: option message
sX: composite_state IM
lifted_transition_input_valid: valid_state_prop X sX
∧ option_valid_message_prop
    X omi
  ∧ valid li
      (sX i, omi)
    ∧ constraint
        (existT i li)
        (sX, omi)
∃ s : composite_state IM,
  s i = sX i
  ∧ valid_state_prop (composite_vlsm IM constraint) s
    ∧ option_valid_message_prop
        (composite_vlsm IM constraint) omi
      ∧ valid li (s i, omi)
        ∧ constraint (existT i li) (s, omi)
    by eexists.
Qed.

Definition component_message_validator_prop : Prop :=
  @message_validator_prop _ X (IM j).

Lemma component_projection_validator_is_message_validator :
  component_projection_validator_prop -> component_message_validator_prop.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
component_projection_validator_prop
→ component_message_validator_prop
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
component_projection_validator_prop
→ component_message_validator_prop
  by intros ?; eapply projection_validator_is_message_validator,
    component_projection_validator_prop_is_induced.
Qed.

Assuming the component_projection_validator_property, the component preloaded_with_all_messages_vlsm is VLSM_equal (trace-equivalent) with its corresponding projection_induced_validator.

Lemma preloaded_with_all_messages_validator_component_proj_eq
  (Hvalidator : component_projection_validator_prop)
  : VLSM_eq (preloaded_with_all_messages_vlsm (IM j)) Xj.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
VLSM_eq (preloaded_with_all_messages_vlsm (IM j)) Xj
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
VLSM_eq (preloaded_with_all_messages_vlsm (IM j)) Xj
  eapply VLSM_eq_trans;
    [| apply VLSM_eq_sym, pre_composite_vlsm_induced_projection_validator_iff].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
VLSM_eq
  {|
    vlsm_type := IM j;
    vlsm_machine :=
      preloaded_vlsm_machine (IM j)
        (λ _ : message, True)
  |}
  {|
    vlsm_type := IM j;
    vlsm_machine :=
      preloaded_vlsm_machine
        (projection_induced_validator
           (composite_vlsm IM constraint) (IM j)
           (composite_project_label IM j)
           (λ s : state (composite_vlsm IM constraint),
              s j) (lift_to_composite_label IM j)
           (lift_to_composite_state' IM j))
        (λ _ : message, True)
  |}
  apply preloaded_with_all_messages_validator_proj_eq.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
weak_projection_transition_consistency_None
  (composite_vlsm IM constraint) (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
induced_validator_label_lift_prop
  (composite_project_label IM j)
  (lift_to_composite_label IM j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
induced_validator_state_lift_prop
  (λ s : state (composite_vlsm IM constraint), s j)
  (lift_to_composite_state' IM j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
strong_projection_initial_state_preservation 
  (IM j) (composite_vlsm IM constraint)
  (lift_to_composite_state' IM j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
induced_validator_transition_consistency_Some
  (composite_vlsm IM constraint) 
  (IM j) (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
VLSM_projection (composite_vlsm IM constraint)
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
projection_validator_prop 
  (IM j) (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j)
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
weak_projection_transition_consistency_None
  (composite_vlsm IM constraint) (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j) by apply component_transition_projection_None.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
induced_validator_label_lift_prop
  (composite_project_label IM j)
  (lift_to_composite_label IM j) by apply component_label_projection_lift.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
induced_validator_state_lift_prop
  (λ s : state (composite_vlsm IM constraint), s j)
  (lift_to_composite_state' IM j) by apply component_state_projection_lift.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
strong_projection_initial_state_preservation (IM j)
  (composite_vlsm IM constraint)
  (lift_to_composite_state' IM j) by intro s; apply (composite_initial_state_prop_lift IM).
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
induced_validator_transition_consistency_Some
  (composite_vlsm IM constraint) (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j) by apply component_transition_projection_Some.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
VLSM_projection (composite_vlsm IM constraint)
  (preloaded_with_all_messages_vlsm (IM j))
  (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j) by apply component_projection_to_preloaded.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
projection_validator_prop (IM j)
  (composite_project_label IM j)
  (λ s : state (composite_vlsm IM constraint), s j) intros li si omi Hiv.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
li: label (preloaded_with_all_messages_vlsm (IM j))
si: state (preloaded_with_all_messages_vlsm (IM j))
omi: option message
Hiv: input_constrained (IM j) li (si, omi)
∃ (lX : label (composite_vlsm IM constraint)) (sX : 
                                               state
                                                 (composite_vlsm
                                                 IM
                                                 constraint)),
  InputValidation (composite_project_label IM j)
    (λ s : state (composite_vlsm IM constraint), s j)
    li si omi lX sX
    apply Hvalidator in Hiv as (sX & <- & HivX).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
li: label (preloaded_with_all_messages_vlsm (IM j))
omi: option message
sX: state (composite_vlsm IM constraint)
HivX: input_valid (composite_vlsm IM constraint)
  (existT j li) (sX, omi)
∃ (lX : label (composite_vlsm IM constraint)) (sX0 : 
                                               state
                                                 (composite_vlsm
                                                 IM
                                                 constraint)),
  InputValidation (composite_project_label IM j)
    (λ s : state (composite_vlsm IM constraint), s j)
    li (sX j) omi lX sX0
    exists (existT j li), sX; split; [| done..].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hvalidator: component_projection_validator_prop
li: label (preloaded_with_all_messages_vlsm (IM j))
omi: option message
sX: state (composite_vlsm IM constraint)
HivX: input_valid (composite_vlsm IM constraint)
  (existT j li) (sX, omi)
composite_project_label IM j (existT j li) = Some li
    by unfold composite_project_label; cbn; rewrite (decide_True_pi eq_refl).
Qed.

Definition preloaded_with_all_messages_validator_component_proj_incl
  (Hvalidator : component_projection_validator_prop)
  : VLSM_incl (preloaded_with_all_messages_vlsm (IM j)) Xj :=
  proj1 (preloaded_with_all_messages_validator_component_proj_eq Hvalidator).

End sec_fixed_projection.

Section projection_validation_constraint_subsumption.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (constraint1 constraint2 : composite_label IM -> composite_state IM * option message -> Prop)
  (j : index)
  .

Lemma component_projection_validator_constraint_subsumption :
  weak_input_valid_constraint_subsumption (free_composite_vlsm IM) constraint1 constraint2 ->
  component_projection_validator_prop IM constraint1 j ->
  component_projection_validator_prop IM constraint2 j.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint1, constraint2: composite_label IM
→ composite_state IM * option message
  → Prop
j: index
weak_input_valid_constraint_subsumption
  (free_composite_vlsm IM) constraint1 constraint2
→ component_projection_validator_prop IM constraint1 j
  → component_projection_validator_prop IM constraint2
      j
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint1, constraint2: composite_label IM
→ composite_state IM * option message
  → Prop
j: index
weak_input_valid_constraint_subsumption
  (free_composite_vlsm IM) constraint1 constraint2
→ component_projection_validator_prop IM constraint1 j
  → component_projection_validator_prop IM constraint2
      j
  intros Hsubsumption Hvalidator lj sj omi Hivj.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint1, constraint2: composite_label IM
→ composite_state IM * option message
  → Prop
j: index
Hsubsumption: weak_input_valid_constraint_subsumption
  (free_composite_vlsm IM) constraint1
  constraint2
Hvalidator: component_projection_validator_prop IM
  constraint1 j
lj: label (IM j)
sj: state (IM j)
omi: option message
Hivj: input_constrained (IM j) lj (sj, omi)
valid lj (sj, omi)
  apply Hvalidator in Hivj as (s & Heqsj & Hivj).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint1, constraint2: composite_label IM
→ composite_state IM * option message
  → Prop
j: index
Hsubsumption: weak_input_valid_constraint_subsumption
  (free_composite_vlsm IM) constraint1
  constraint2
Hvalidator: component_projection_validator_prop IM
  constraint1 j
lj: label (IM j)
sj: state (IM j)
omi: option message
s: state (composite_vlsm IM constraint1)
Heqsj: s j = sj
Hivj: input_valid (composite_vlsm IM constraint1)
  (existT j lj) (s, omi)
valid lj (sj, omi)
  exists s; split; [done |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint1, constraint2: composite_label IM
→ composite_state IM * option message
  → Prop
j: index
Hsubsumption: weak_input_valid_constraint_subsumption
  (free_composite_vlsm IM) constraint1
  constraint2
Hvalidator: component_projection_validator_prop IM
  constraint1 j
lj: label (IM j)
sj: state (IM j)
omi: option message
s: state (composite_vlsm IM constraint1)
Heqsj: s j = sj
Hivj: input_valid (composite_vlsm IM constraint1)
  (existT j lj) (s, omi)
input_valid (composite_vlsm IM constraint2)
  (existT j lj) (s, omi)
  by revert Hivj; apply VLSM_incl_input_valid, weak_constraint_subsumption_incl.
Qed.

End projection_validation_constraint_subsumption.

Section sec_projection_friendliness_sufficient_condition.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  (constraint : composite_label IM -> composite_state IM * option message -> Prop)
  (X := composite_vlsm IM constraint)
  .

A sufficient condition for the projection friendly property

Context
  (j : index)
  (Xj := pre_composite_vlsm_induced_projection_validator IM constraint j)
  .

This condition states that input_validity in a projection Xj can be lifted to any valid_state in X which projects to the corresponding Xj state.

Definition projection_friendliness_sufficient_condition
  := forall
    (lj : label (IM j))
    (sj : state (IM j))
    (om : option message)
    (Hiv : input_valid Xj lj (sj, om))
    (s : state X)
    (Hs : valid_state_prop X s)
    (Hsi : s j = sj)
    , valid X (existT j lj) (s, om).

Lemma projection_friendliness_sufficient_condition_valid_state
  (Hfr : projection_friendliness_sufficient_condition)
  (s : state Xj)
  (Hp : valid_state_prop Xj s)
  : valid_state_prop X (lift_to_composite_state' IM j s).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s: state Xj
Hp: valid_state_prop Xj s
valid_state_prop X (lift_to_composite_state' IM j s)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s: state Xj
Hp: valid_state_prop Xj s
valid_state_prop X (lift_to_composite_state' IM j s)
  induction Hp using valid_state_prop_ind.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s: state Xj
Hs: initial_state_prop s
valid_state_prop X (lift_to_composite_state' IM j s)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s': state Xj
l: label Xj
om, om': option message
s: state Xj
Ht: input_valid_transition Xj l (s, om) (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
valid_state_prop X (lift_to_composite_state' IM j s')
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s: state Xj
Hs: initial_state_prop s
valid_state_prop X (lift_to_composite_state' IM j s) by apply initial_state_is_valid, (composite_initial_state_prop_lift IM j).
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s': state Xj
l: label Xj
om, om': option message
s: state Xj
Ht: input_valid_transition Xj l (s, om) (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
valid_state_prop X (lift_to_composite_state' IM j s') destruct Ht as [Hvj Ht].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s': state Xj
l: label Xj
om, om': option message
s: state Xj
Hvj: input_valid Xj l (s, om)
Ht: transition l (s, om) = (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
valid_state_prop X (lift_to_composite_state' IM j s')
    specialize (Hfr _ _ _ Hvj _ IHHp).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s: state Xj
Hfr: lift_to_composite_state' IM j s j = s
→ valid (existT j l)
    (lift_to_composite_state' IM j s, om)
s': state Xj
om': option message
Hvj: input_valid Xj l (s, om)
Ht: transition l (s, om) = (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
valid_state_prop X (lift_to_composite_state' IM j s')
    spec Hfr; [by apply state_update_eq |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: input_valid Xj l (s, om)
Ht: transition l (s, om) = (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
valid_state_prop X (lift_to_composite_state' IM j s')
    exists om'.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: input_valid Xj l (s, om)
Ht: transition l (s, om) = (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
valid_state_message_prop X
  (lift_to_composite_state' IM j s') om'
    destruct Hvj as [_ [_ Hvj]].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
valid_state_message_prop X
  (lift_to_composite_state' IM j s') om'
    apply (projection_valid_implies_composition_valid_message IM) in Hvj as Hom.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
IHHp: valid_state_prop X
  (lift_to_composite_state' IM j s)
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
Hom: option_valid_message_prop
  (composite_vlsm IM constraint) om
valid_state_message_prop X
  (lift_to_composite_state' IM j s') om'
    destruct IHHp as [_om HsX].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (lift_to_composite_state' IM j s) _om
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
Hom: option_valid_message_prop
  (composite_vlsm IM constraint) om
valid_state_message_prop X
  (lift_to_composite_state' IM j s') om'
    destruct Hom as [_s Hom].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (lift_to_composite_state' IM j s) _om
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
_s: state (composite_vlsm IM constraint)
Hom: valid_state_message_prop
  (composite_vlsm IM constraint) _s om
valid_state_message_prop X
  (lift_to_composite_state' IM j s') om'
    specialize (valid_generated_state_message X _ _ HsX _ _ Hom _ Hfr) as Hgen.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (lift_to_composite_state' IM j s) _om
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
_s: state (composite_vlsm IM constraint)
Hom: valid_state_message_prop
  (composite_vlsm IM constraint) _s om
Hgen: ∀ (s' : state X) (om' : option message),
  transition (existT j l)
    (lift_to_composite_state' IM j s, om) =
  (s', om') → valid_state_message_prop X s' om'
valid_state_message_prop X
  (lift_to_composite_state' IM j s') om'
    apply Hgen.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (lift_to_composite_state' IM j s) _om
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
_s: state (composite_vlsm IM constraint)
Hom: valid_state_message_prop
  (composite_vlsm IM constraint) _s om
Hgen: ∀ (s' : state X) (om' : option message),
  transition (existT j l)
    (lift_to_composite_state' IM j s, om) =
  (s', om') → valid_state_message_prop X s' om'
transition (existT j l)
  (lift_to_composite_state' IM j s, om) =
(lift_to_composite_state' IM j s', om')
    cbn; unfold lift_to_composite_state' at 1.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (lift_to_composite_state' IM j s) _om
Hfr: valid (existT j l)
  (lift_to_composite_state' IM j s, om)
_s: state (composite_vlsm IM constraint)
Hom: valid_state_message_prop
  (composite_vlsm IM constraint) _s om
Hgen: ∀ (s' : state X) (om' : option message),
  transition (existT j l)
    (lift_to_composite_state' IM j s, om) =
  (s', om') → valid_state_message_prop X s' om'
(let (si', om') :=
   transition l
     (lift_to_composite_state IM (`(composite_s0 IM))
        j s j, om) in
 (state_update IM (lift_to_composite_state' IM j s) j
    si', om')) =
(lift_to_composite_state' IM j s', om')
    state_update_simpl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (state_update IM (`(composite_s0 IM)) j s) _om
Hfr: valid (existT j l)
  (state_update IM (`(composite_s0 IM)) j s, om)
_s: state (composite_vlsm IM constraint)
Hom: valid_state_message_prop
  (composite_vlsm IM constraint) _s om
Hgen: ∀ (s' : state X) (om' : option message),
  transition (existT j l)
    (state_update IM (`(composite_s0 IM)) j s,
     om) = (s', om')
  → valid_state_message_prop X s' om'
(let (si', om') := transition l (s, om) in
 (state_update IM
    (state_update IM (`(composite_s0 IM)) j s) j si',
  om')) =
(state_update IM (`(composite_s0 IM)) j s', om')
    replace (transition (IM j) _ _) with (s', om').message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (state_update IM (`(composite_s0 IM)) j s) _om
Hfr: valid (existT j l)
  (state_update IM (`(composite_s0 IM)) j s, om)
_s: state (composite_vlsm IM constraint)
Hom: valid_state_message_prop
  (composite_vlsm IM constraint) _s om
Hgen: ∀ (s' : state X) (om' : option message),
  transition (existT j l)
    (state_update IM (`(composite_s0 IM)) j s,
     om) = (s', om')
  → valid_state_message_prop X s' om'
(state_update IM
   (state_update IM (`(composite_s0 IM)) j s) j s',
 om') =
(state_update IM (`(composite_s0 IM)) j s', om')
    f_equal.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
l: label Xj
om: option message
s, s': state Xj
om': option message
Hvj: valid l (s, om)
Ht: transition l (s, om) = (s', om')
_om: option message
HsX: valid_state_message_prop X
  (state_update IM (`(composite_s0 IM)) j s) _om
Hfr: valid (existT j l)
  (state_update IM (`(composite_s0 IM)) j s, om)
_s: state (composite_vlsm IM constraint)
Hom: valid_state_message_prop
  (composite_vlsm IM constraint) _s om
Hgen: ∀ (s' : state X) (om' : option message),
  transition (existT j l)
    (state_update IM (`(composite_s0 IM)) j s,
     om) = (s', om')
  → valid_state_message_prop X s' om'
state_update IM
  (state_update IM (`(composite_s0 IM)) j s) j s' =
state_update IM (`(composite_s0 IM)) j s'
    by apply state_update_twice.
Qed.

The result below shows that the projection_friendliness_sufficient_condition might be too strong, in the sense that it allows any trace from the projection to be lifted directly to X (all other machines stay in their initial state).

Lemma projection_friendliness_lift_to_composite_VLSM_embedding
  (Hfr : projection_friendliness_sufficient_condition)
  : VLSM_embedding Xj X (lift_to_composite_label IM j) (lift_to_composite_state' IM j).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
VLSM_embedding Xj X (lift_to_composite_label IM j)
  (lift_to_composite_state' IM j)
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
VLSM_embedding Xj X (lift_to_composite_label IM j)
  (lift_to_composite_state' IM j)
  apply basic_VLSM_embedding; intro; intros.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
Hv: input_valid Xj l (s, om)
HsY: valid_state_prop X
  (lift_to_composite_state' IM j s)
HomY: option_valid_message_prop X om
valid (lift_to_composite_label IM j l)
  (lift_to_composite_state' IM j s, om)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
s': state Xj
om': option message
H: input_valid_transition Xj l (s, om) (s', om')
transition (lift_to_composite_label IM j l)
  (lift_to_composite_state' IM j s, om) =
(lift_to_composite_state' IM j s', om')
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s: state Xj
H: initial_state_prop s
initial_state_prop (lift_to_composite_state' IM j s)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
m: message
Hv: input_valid Xj l (s, Some m)
HsY: valid_state_prop X
  (lift_to_composite_state' IM j s)
HmX: initial_message_prop m
valid_message_prop X m
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
Hv: input_valid Xj l (s, om)
HsY: valid_state_prop X
  (lift_to_composite_state' IM j s)
HomY: option_valid_message_prop X om
valid (lift_to_composite_label IM j l)
  (lift_to_composite_state' IM j s, om) apply (Hfr _ _ _ Hv); [| apply state_update_eq].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
Hv: input_valid Xj l (s, om)
HsY: valid_state_prop X
  (lift_to_composite_state' IM j s)
HomY: option_valid_message_prop X om
valid_state_prop X (lift_to_composite_state' IM j s)
    by apply (projection_friendliness_sufficient_condition_valid_state Hfr), Hv.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
s': state Xj
om': option message
H: input_valid_transition Xj l (s, om) (s', om')
transition (lift_to_composite_label IM j l)
  (lift_to_composite_state' IM j s, om) =
(lift_to_composite_state' IM j s', om') cbn; unfold lift_to_composite_state' at 1.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
s': state Xj
om': option message
H: input_valid_transition Xj l (s, om) (s', om')
(let (si', om') :=
   transition l
     (lift_to_composite_state IM (`(composite_s0 IM))
        j s j, om) in
 (state_update IM (lift_to_composite_state' IM j s) j
    si', om')) =
(lift_to_composite_state' IM j s', om')
    state_update_simpl.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
s': state Xj
om': option message
H: input_valid_transition Xj l (s, om) (s', om')
(let (si', om') := transition l (s, om) in
 (state_update IM
    (state_update IM (`(composite_s0 IM)) j s) j si',
  om')) =
(state_update IM (`(composite_s0 IM)) j s', om')
    replace (transition (IM j) _ _) with (s', om')
      by (symmetry; apply H).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
om: option message
s': state Xj
om': option message
H: input_valid_transition Xj l (s, om) (s', om')
(state_update IM
   (state_update IM (`(composite_s0 IM)) j s) j s',
 om') =
(state_update IM (`(composite_s0 IM)) j s', om')
    by rewrite state_update_twice.
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
s: state Xj
H: initial_state_prop s
initial_state_prop (lift_to_composite_state' IM j s) by apply (composite_initial_state_prop_lift IM j).
  -message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
constraint: composite_label IM
→ composite_state IM * option message
  → Prop
X:= composite_vlsm IM constraint: VLSM message
j: index
Xj:= pre_composite_vlsm_induced_projection_validator IM
  constraint j: VLSM message
Hfr: projection_friendliness_sufficient_condition
l: label Xj
s: state Xj
m: message
Hv: input_valid Xj l (s, Some m)
HsY: valid_state_prop X
  (lift_to_composite_state' IM j s)
HmX: initial_message_prop m
valid_message_prop X m by destruct Hv as [Hs [Homj [sX [Heqs [HsX [Hom Hv]]]]]].
Qed.

End sec_projection_friendliness_sufficient_condition.

Free composition

Section sec_composition.

Context
  `{EqDecision index}
  `[IM : index -> VLSM message]
  .

A stronger version of valid_state_component_initial_or_transition for the free composition, it guarantees that a component state of a valid state for the free composition is either initial or there is a valid transition in the free composition leading to the given state which corresponds to a component transition.

Lemma free_valid_state_component_initial_or_transition :
  forall (i : index) (s : composite_state IM),
    valid_state_prop (free_composite_vlsm IM) s ->
    initial_state_prop (IM i) (s i)
      \/
    exists (l : label (IM i)) (si0 : state (IM i)) (om om' : option message),
      input_valid_transition (free_composite_vlsm IM) (existT i l)
        (state_update IM s i si0, om) (s, om').index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
∀ (i : index) (s : composite_state IM),
  valid_state_prop (free_composite_vlsm IM) s
  → initial_state_prop (s i)
    ∨ (∃ (l : label (IM i)) (si0 : state (IM i)) (om
                                                 om' : 
                                                 option
                                                 message),
         input_valid_transition
           (free_composite_vlsm IM) (existT i l)
           (state_update IM s i si0, om) (s, om'))
Proof.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
∀ (i : index) (s : composite_state IM),
  valid_state_prop (free_composite_vlsm IM) s
  → initial_state_prop (s i)
    ∨ (∃ (l : label (IM i)) (si0 : state (IM i)) (om
                                                 om' : 
                                                 option
                                                 message),
         input_valid_transition
           (free_composite_vlsm IM) (existT i l)
           (state_update IM s i si0, om) (s, om'))
  intros i s Hs.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
initial_state_prop (s i)
∨ (∃ (l : label (IM i)) (si0 : state (IM i)) (om
                                              om' : 
                                              option
                                                message),
     input_valid_transition (free_composite_vlsm IM)
       (existT i l) (state_update IM s i si0, om)
       (s, om'))
  apply (VLSM_eq_valid_state (free_composite_vlsm_spec IM)) in Hs as Hs'.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
Hs': valid_state_prop
  {|
    vlsm_type := free_composite_vlsm IM;
    vlsm_machine :=
      composite_vlsm IM (free_constraint IM)
  |} s
initial_state_prop (s i)
∨ (∃ (l : label (IM i)) (si0 : state (IM i)) (om
                                              om' : 
                                              option
                                                message),
     input_valid_transition (free_composite_vlsm IM)
       (existT i l) (state_update IM s i si0, om)
       (s, om'))
  apply (valid_state_component_initial_or_transition i) in Hs'
    as [| (s1 & s2 & li & om & om' & Hfutures & Heq & Ht)]; [by left |].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
initial_state_prop (s i)
∨ (∃ (l : label (IM i)) (si0 : state (IM i)) (om
                                              om' : 
                                              option
                                                message),
     input_valid_transition (free_composite_vlsm IM)
       (existT i l) (state_update IM s i si0, om)
       (s, om'))
  right; exists li, (s1 i), om, om'.index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
input_valid_transition (free_composite_vlsm IM)
  (existT i li) (state_update IM s i (s1 i), om)
  (s, om')
  replace s with (state_update IM s i (s2 i)) at 2
    by (apply state_update_id; done).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
input_valid_transition (free_composite_vlsm IM)
  (existT i li) (state_update IM s i (s1 i), om)
  (state_update IM s i (s2 i), om')
  apply (VLSM_weak_embedding_input_valid_transition
    (pre_free_lift_to_free_weak_embedding i s Hs)).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
input_valid_transition
  (preloaded_vlsm (IM i)
     (valid_message_prop (free_composite_vlsm IM))) li
  (s1 i, om) (s2 i, om')
  unshelve eapply (VLSM_incl_input_valid_transition
    (preloaded_vlsm_incl (IM i)
      (valid_message_prop (composite_vlsm IM (free_constraint IM)))
      (valid_message_prop (free_composite_vlsm IM)) _)).index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
∀ m : message,
  valid_message_prop
    (composite_vlsm IM (free_constraint IM)) m
  → valid_message_prop (free_composite_vlsm IM) m
index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
input_valid_transition
  {|
    vlsm_type :=
      preloaded_vlsm (IM i)
        (valid_message_prop
           (composite_vlsm IM (free_constraint IM)));
    vlsm_machine :=
      preloaded_vlsm (IM i)
        (valid_message_prop
           (composite_vlsm IM (free_constraint IM)))
  |} li (s1 i, om) (s2 i, om')
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
∀ m : message,
  valid_message_prop
    (composite_vlsm IM (free_constraint IM)) m
  → valid_message_prop (free_composite_vlsm IM) m apply VLSM_incl_valid_message; [| by intro].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
VLSM_incl_part
  (constrained_vlsm_machine (free_composite_vlsm IM)
     (free_constraint IM))
  (free_composite_vlsm_machine IM)
    by apply free_composite_vlsm_spec.
  -index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
input_valid_transition
  {|
    vlsm_type :=
      preloaded_vlsm (IM i)
        (valid_message_prop
           (composite_vlsm IM (free_constraint IM)));
    vlsm_machine :=
      preloaded_vlsm (IM i)
        (valid_message_prop
           (composite_vlsm IM (free_constraint IM)))
  |} li (s1 i, om) (s2 i, om') eapply (VLSM_projection_input_valid_transition
      (composite_vlsm_induced_projection_is_projection IM _ _)); [| done].index: Type
EqDecision0: EqDecision index
message: Type
IM: index → VLSM message
i: index
s: composite_state IM
Hs: valid_state_prop (free_composite_vlsm IM) s
s1, s2: composite_state IM
li: label (IM i)
om, om': option message
Hfutures: in_futures
  (composite_vlsm IM (free_constraint IM))
  s2 s
Heq: s2 i = s i
Ht: input_valid_transition
  (composite_vlsm IM (free_constraint IM))
  (existT i li) (s1, om) (
  s2, om')
composite_project_label IM i (existT i li) = Some li
    by rewrite Validator.composite_project_label_eq.
Qed.

End sec_composition.