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 StreamExtras StreamFilters.
From VLSM.Core Require Import VLSM VLSMProjections.VLSMTotalProjection.

Core: VLSM Embedding

A VLSM projection guaranteeing the existence of projection for all labels and states, and the full correspondence between transition_items. We say that VLSM X fully projects (embeds) into VLSM Y (sharing the same messages) if there exist maps label_project taking X-labels to Y-labels and state_project taking X-states to Y-states, such that the finite_valid_trace_property is preserved by the trace transformation induced by the label and state projection functions, in which each X-transition_item is projected to an Y-transition_item preserving the messages and transforming labels and states accordingly.

Besides VLSM_inclusions, which are a prototypical example of VLSM embeddings, we can also prove "lifting" relations between components and the composition that they are part of as being embeddings (see, e.g., lift_to_composite_VLSM_embedding or projection_friendliness_lift_to_composite_VLSM_embedding).

Section sec_VLSM_embedding.

Section sec_pre_definitions.

Context
  {message : Type}
  (TX TY : VLSMType message)
  (label_project : label TX -> label TY)
  (state_project : state TX -> state TY)
  .

Definition pre_VLSM_embedding_transition_item_project
  : transition_item TX -> transition_item TY
  :=
  fun item =>
  {| l := label_project (l item)
   ; input := input item
   ; destination := state_project (destination item)
   ; output := output item
  |}.

Definition pre_VLSM_embedding_finite_trace_project
  : list (transition_item TX) -> list (transition_item TY)
  := map pre_VLSM_embedding_transition_item_project.

Definition pre_VLSM_embedding_infinite_trace_project
  : Streams.Stream (transition_item TX) -> Streams.Stream (transition_item TY)
  := Streams.map pre_VLSM_embedding_transition_item_project.

Lemma pre_VLSM_embedding_infinite_trace_project_infinitely_often
  : forall s, InfinitelyOften (is_Some ∘ (Some ∘ label_project ∘ l)) s.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ s : Streams.Stream transition_item,
  InfinitelyOften
    (is_Some ∘ (Some ∘ label_project ∘ l)) s
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ s : Streams.Stream transition_item,
  InfinitelyOften
    (is_Some ∘ (Some ∘ label_project ∘ l)) s
  cofix H.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
H: ∀ s : Streams.Stream transition_item,
  InfinitelyOften
    (is_Some ∘ (Some ∘ label_project ∘ l)) s
∀ s : Streams.Stream transition_item,
  InfinitelyOften
    (is_Some ∘ (Some ∘ label_project ∘ l)) s intros (a, s).message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
H: ∀ s : Streams.Stream transition_item,
  InfinitelyOften
    (is_Some ∘ (Some ∘ label_project ∘ l)) s
a: transition_item
s: Streams.Stream transition_item
InfinitelyOften (is_Some ∘ (Some ∘ label_project ∘ l))
  (Streams.Cons a s) constructor; simpl; [| by apply H].message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
H: ∀ s : Streams.Stream transition_item,
  InfinitelyOften
    (is_Some ∘ (Some ∘ label_project ∘ l)) s
a: transition_item
s: Streams.Stream transition_item
Exists1 (is_Some ∘ (Some ∘ label_project ∘ l))
  (Streams.Cons a s)
  by apply Streams.Here; eexists.
Qed.

Lemma pre_VLSM_embedding_infinite_trace_project_EqSt
  : forall s (Hinf := pre_VLSM_embedding_infinite_trace_project_infinitely_often s),
  Streams.EqSt
    (pre_VLSM_embedding_infinite_trace_project s)
    (pre_VLSM_projection_infinite_trace_project _ _ (Some ∘ label_project) state_project s Hinf).message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ s : Streams.Stream transition_item,
  let Hinf :
    InfinitelyOften
      (is_Some ∘ (Some ∘ label_project ∘ l)) s :=
    pre_VLSM_embedding_infinite_trace_project_infinitely_often
      s in
  Streams.EqSt
    (pre_VLSM_embedding_infinite_trace_project s)
    (pre_VLSM_projection_infinite_trace_project TX TY
       (Some ∘ label_project) state_project s Hinf)
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ s : Streams.Stream transition_item,
  let Hinf :
    InfinitelyOften
      (is_Some ∘ (Some ∘ label_project ∘ l)) s :=
    pre_VLSM_embedding_infinite_trace_project_infinitely_often
      s in
  Streams.EqSt
    (pre_VLSM_embedding_infinite_trace_project s)
    (pre_VLSM_projection_infinite_trace_project TX TY
       (Some ∘ label_project) state_project s Hinf)
  intros.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
s: Streams.Stream transition_item
Hinf:= pre_VLSM_embedding_infinite_trace_project_infinitely_often
  s: InfinitelyOften
  (is_Some ∘ (Some ∘ label_project ∘ l)) s
Streams.EqSt
  (pre_VLSM_embedding_infinite_trace_project s)
  (pre_VLSM_projection_infinite_trace_project TX TY
     (Some ∘ label_project) state_project s Hinf)
  by apply stream_map_option_EqSt.
Qed.

Lemma pre_VLSM_embedding_finite_trace_last
  : forall sX trX,
    state_project (finite_trace_last sX trX) =
    finite_trace_last (state_project sX) (pre_VLSM_embedding_finite_trace_project trX).message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ (sX : state TX) (trX : list transition_item),
  state_project (finite_trace_last sX trX) =
  finite_trace_last (state_project sX)
    (pre_VLSM_embedding_finite_trace_project trX)
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ (sX : state TX) (trX : list transition_item),
  state_project (finite_trace_last sX trX) =
  finite_trace_last (state_project sX)
    (pre_VLSM_embedding_finite_trace_project trX)
  intros.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
sX: state TX
trX: list transition_item
state_project (finite_trace_last sX trX) =
finite_trace_last (state_project sX)
  (pre_VLSM_embedding_finite_trace_project trX)
  destruct_list_last trX trX' lst HtrX; [done |].message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
sX: state TX
trX, trX': list transition_item
lst: transition_item
HtrX: trX = trX' ++ [lst]
state_project (finite_trace_last sX (trX' ++ [lst])) =
finite_trace_last (state_project sX)
  (pre_VLSM_embedding_finite_trace_project
     (trX' ++ [lst]))
  by setoid_rewrite map_app; cbn; rewrite !finite_trace_last_is_last.
Qed.

Lemma pre_VLSM_embedding_finite_trace_last_output :
  forall trX,
    finite_trace_last_output trX
      =
    finite_trace_last_output (pre_VLSM_embedding_finite_trace_project trX).message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ trX : list transition_item,
  finite_trace_last_output trX =
  finite_trace_last_output
    (pre_VLSM_embedding_finite_trace_project trX)
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
∀ trX : list transition_item,
  finite_trace_last_output trX =
  finite_trace_last_output
    (pre_VLSM_embedding_finite_trace_project trX)
  intros trX.message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
trX: list transition_item
finite_trace_last_output trX =
finite_trace_last_output
  (pre_VLSM_embedding_finite_trace_project trX)
  destruct_list_last trX trX' lst HtrX; [done |].message: Type
TX, TY: VLSMType message
label_project: label TX → label TY
state_project: state TX → state TY
trX, trX': list transition_item
lst: transition_item
HtrX: trX = trX' ++ [lst]
finite_trace_last_output (trX' ++ [lst]) =
finite_trace_last_output
  (pre_VLSM_embedding_finite_trace_project
     (trX' ++ [lst]))
  by setoid_rewrite map_app; simpl; rewrite !finite_trace_last_output_is_last.
Qed.

End sec_pre_definitions.

Section sec_basic_definitions.

Context
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> label Y)
  (state_project : state X -> state Y)
  .

Similarly to VLSM_partial_projections and VLSM_projections, we distinguish two types of projections: VLSM_weak_embedding and VLSM_embedding, distinguished by the fact that the weak projections are not required to preserve initial states.

Proper examples of VLSM_weak_embedding are presented in Lemmas PreSubFree_PreFree_weak_embedding and EquivPreloadedBase_Fixed_weak_embedding, which show that a trace over a subset of components can be replayed on top of a valid state for the full composition. Note that in this case, the initial state of the trace not translated to an initial state but rather to a regular valid state.

Record VLSM_weak_embedding : Prop :=
{
  weak_full_trace_project_preserves_valid_trace :
    forall sX trX,
      finite_valid_trace_from X sX trX ->
      finite_valid_trace_from Y (state_project sX)
        (pre_VLSM_embedding_finite_trace_project _ _ label_project state_project trX);
}.

Record VLSM_embedding : Prop :=
{
  full_trace_project_preserves_valid_trace :
    forall sX trX,
      finite_valid_trace X sX trX ->
      finite_valid_trace Y (state_project sX)
        (pre_VLSM_embedding_finite_trace_project _ _ label_project state_project trX);
}.

Definition weak_embedding_valid_preservation : Prop :=
  forall (l : label X) (s : state X) (om : option message)
    (Hv : input_valid X l (s, om))
    (HsY : valid_state_prop Y (state_project s))
    (HomY : option_valid_message_prop Y om),
    valid Y (label_project l) ((state_project s), om).

Lemma weak_projection_valid_preservation_from_full
  : weak_embedding_valid_preservation ->
    weak_projection_valid_preservation X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
weak_embedding_valid_preservation
→ weak_projection_valid_preservation X Y
    (Some ∘ label_project) state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
weak_embedding_valid_preservation
→ weak_projection_valid_preservation X Y
    (Some ∘ label_project) state_project
  intros Hvalid lX lY Hl; inversion_clear Hl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation
lX: label X
lY: label Y
∀ (s : state X) (om : option message),
  input_valid X lX (s, om)
  → valid_state_prop Y (state_project s)
    → option_valid_message_prop Y om
      → valid (label_project lX) (state_project s, om)
  by apply Hvalid.
Qed.

Definition strong_embedding_valid_preservation : Prop :=
  forall (l : label X) (s : state X) (om : option message),
    valid X l (s, om) -> valid Y (label_project l) ((state_project s), om).

Lemma strong_projection_valid_preservation_from_full
  : strong_embedding_valid_preservation ->
    strong_projection_valid_preservation X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_valid_preservation
→ strong_projection_valid_preservation X Y
    (Some ∘ label_project) state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_valid_preservation
→ strong_projection_valid_preservation X Y
    (Some ∘ label_project) state_project
  intros Hvalid lX lY Hl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
∀ (s : state X) (om : option message),
  valid lX (s, om) → valid lY (state_project s, om)
  inversion_clear Hl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation
lX: label X
lY: label Y
∀ (s : state X) (om : option message),
  valid lX (s, om)
  → valid (label_project lX) (state_project s, om)
  by apply Hvalid.
Qed.

Lemma strong_embedding_valid_preservation_weaken
  : strong_embedding_valid_preservation ->
    weak_embedding_valid_preservation.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_valid_preservation
→ weak_embedding_valid_preservation
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_valid_preservation
→ weak_embedding_valid_preservation
  intros Hstrong l s om Hpv Hs Hom.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hstrong: strong_embedding_valid_preservation
l: label X
s: state X
om: option message
Hpv: input_valid X l (s, om)
Hs: valid_state_prop Y (state_project s)
Hom: option_valid_message_prop Y om
valid (label_project l) (state_project s, om)
  by apply Hstrong, Hpv.
Qed.

Definition weak_embedding_transition_preservation : Prop :=
  forall l s om s' om',
    input_valid_transition X l (s, om) (s', om') ->
    transition Y (label_project l) (state_project s, om) = (state_project s', om').

Lemma weak_projection_transition_preservation_Some_from_full
  : weak_embedding_transition_preservation ->
    weak_projection_transition_preservation_Some X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
weak_embedding_transition_preservation
→ weak_projection_transition_preservation_Some X Y
    (Some ∘ label_project) state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
weak_embedding_transition_preservation
→ weak_projection_transition_preservation_Some X Y
    (Some ∘ label_project) state_project
  intros Htransition lX lY Hl; inversion_clear Hl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Htransition: weak_embedding_transition_preservation
lX: label X
lY: label Y
∀ (s : state X) (om : option message) (s' : state X) 
  (om' : option message),
  input_valid_transition X lX (s, om) (s', om')
  → transition (label_project lX)
      (state_project s, om) = (state_project s', om')
  by apply Htransition.
Qed.

Lemma weak_projection_transition_consistency_None_from_full
  : weak_projection_transition_consistency_None _ _ (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
weak_projection_transition_consistency_None X Y
  (Some ∘ label_project) state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
weak_projection_transition_consistency_None X Y
  (Some ∘ label_project) state_project by inversion 1. Qed.

Definition strong_embedding_transition_preservation : Prop :=
  forall l s om s' om',
      transition X l (s, om) = (s', om') ->
      transition Y (label_project l) (state_project s, om) = (state_project s', om').

Lemma strong_projection_transition_preservation_Some_from_full
  : strong_embedding_transition_preservation ->
    strong_projection_transition_preservation_Some X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_transition_preservation
→ strong_projection_transition_preservation_Some X Y
    (Some ∘ label_project) state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_transition_preservation
→ strong_projection_transition_preservation_Some X Y
    (Some ∘ label_project) state_project
  intros Htransition lX lY Hl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Htransition: strong_embedding_transition_preservation
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
∀ (s : state X) (om : option message) (s' : state X) 
  (om' : option message),
  transition lX (s, om) = (s', om')
  → transition lY (state_project s, om) =
    (state_project s', om')
  inversion_clear Hl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Htransition: strong_embedding_transition_preservation
lX: label X
lY: label Y
∀ (s : state X) (om : option message) (s' : state X) 
  (om' : option message),
  transition lX (s, om) = (s', om')
  → transition (label_project lX)
      (state_project s, om) = (state_project s', om')
  by apply Htransition.
Qed.

Lemma strong_projection_transition_consistency_None_from_full
  : strong_projection_transition_consistency_None _ _ (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_projection_transition_consistency_None X Y
  (Some ∘ label_project) state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_projection_transition_consistency_None X Y
  (Some ∘ label_project) state_project inversion 1. Qed.

Lemma strong_embedding_transition_preservation_weaken
  : strong_embedding_transition_preservation ->
    weak_embedding_transition_preservation.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_transition_preservation
→ weak_embedding_transition_preservation
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_transition_preservation
→ weak_embedding_transition_preservation
  intros Hstrong l s om s' om' Ht.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hstrong: strong_embedding_transition_preservation
l: label X
s: state X
om: option message
s': state X
om': option message
Ht: input_valid_transition X l (s, om) (s', om')
transition (label_project l) (state_project s, om) =
(state_project s', om')
  by apply Hstrong, Ht.
Qed.

Definition weak_embedding_initial_message_preservation : Prop :=
  forall (l : label X) (s : state X) (m : message)
    (Hv : input_valid X l (s, Some m))
    (HsY : valid_state_prop Y (state_project s))
    (HmX : initial_message_prop X m),
    valid_message_prop Y m.

Definition strong_embedding_initial_message_preservation : Prop :=
  forall m : message,
    initial_message_prop X m -> initial_message_prop Y m.

Lemma strong_embedding_initial_message_preservation_weaken
  : strong_embedding_initial_message_preservation ->
    weak_embedding_initial_message_preservation.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_initial_message_preservation
→ weak_embedding_initial_message_preservation
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
strong_embedding_initial_message_preservation
→ weak_embedding_initial_message_preservation
  intros Hstrong l s m Hv HsY Him.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hstrong: strong_embedding_initial_message_preservation
l: label X
s: state X
m: message
Hv: input_valid X l (s, Some m)
HsY: valid_state_prop Y (state_project s)
Him: initial_message_prop m
valid_message_prop Y m
  apply Hstrong in Him.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hstrong: strong_embedding_initial_message_preservation
l: label X
s: state X
m: message
Hv: input_valid X l (s, Some m)
HsY: valid_state_prop Y (state_project s)
Him: initial_message_prop m
valid_message_prop Y m
  by apply initial_message_is_valid.
Qed.

End sec_basic_definitions.

Definition VLSM_embedding_transition_item_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> label Y}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_embedding X Y label_project state_project)
  := pre_VLSM_embedding_transition_item_project _ _  label_project state_project
  .

Definition VLSM_embedding_finite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> label Y}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_embedding X Y label_project state_project)
  := pre_VLSM_embedding_finite_trace_project _ _  label_project state_project.

Definition VLSM_embedding_infinite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> label Y}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_embedding X Y label_project state_project)
  := pre_VLSM_embedding_infinite_trace_project _ _  label_project state_project.

Definition VLSM_weak_embedding_finite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> label Y}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_weak_embedding X Y label_project state_project)
  := pre_VLSM_embedding_finite_trace_project _ _ label_project state_project.

Definition VLSM_weak_embedding_infinite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> label Y}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_weak_embedding X Y label_project state_project)
  := pre_VLSM_embedding_infinite_trace_project _ _  label_project state_project.

Lemma VLSM_embedding_projection_type
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> label Y)
  (state_project : state X -> state Y)
  : VLSM_projection_type X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
VLSM_projection_type X Y (Some ∘ label_project)
  state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
VLSM_projection_type X Y (Some ∘ label_project)
  state_project
  split; intros.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
sX: state X
trX: list transition_item
H: finite_valid_trace_from X sX trX
state_project (finite_trace_last sX trX) =
finite_trace_last (state_project sX)
  (pre_VLSM_projection_finite_trace_project X Y
     (Some ∘ label_project) state_project trX)
  destruct_list_last trX trX' lstX Heq; [done |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
sX: state X
trX, trX': list transition_item
lstX: transition_item
H: finite_valid_trace_from X sX (trX' ++ [lstX])
Heq: trX = trX' ++ [lstX]
state_project (finite_trace_last sX (trX' ++ [lstX])) =
finite_trace_last (state_project sX)
  (pre_VLSM_projection_finite_trace_project X Y
     (Some ∘ label_project) state_project
     (trX' ++ [lstX]))
  by apply pre_VLSM_embedding_finite_trace_last.
Qed.

Section sec_weak_projection_properties.

Weak projection properties

Context
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> label Y}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_weak_embedding X Y label_project state_project)
  .

Lemma VLSM_weak_embedding_finite_trace_last :
  forall (sX : state X) (trX : list (transition_item X)),
    state_project (finite_trace_last sX trX)
      =
    finite_trace_last (state_project sX) (VLSM_weak_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  state_project (finite_trace_last sX trX) =
  finite_trace_last (state_project sX)
    (VLSM_weak_embedding_finite_trace_project Hsimul
       trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  state_project (finite_trace_last sX trX) =
  finite_trace_last (state_project sX)
    (VLSM_weak_embedding_finite_trace_project Hsimul
       trX)
  exact (pre_VLSM_embedding_finite_trace_last _ _ label_project state_project).
Qed.

Lemma VLSM_weak_embedding_finite_valid_trace_from :
  forall (s : state X) (tr : list (transition_item X)),
    finite_valid_trace_from X s tr ->
    finite_valid_trace_from Y (state_project s)
      (VLSM_weak_embedding_finite_trace_project Hsimul tr).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace_from X s tr
  → finite_valid_trace_from Y (state_project s)
      (VLSM_weak_embedding_finite_trace_project Hsimul
         tr)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace_from X s tr
  → finite_valid_trace_from Y (state_project s)
      (VLSM_weak_embedding_finite_trace_project Hsimul
         tr)
  exact (weak_full_trace_project_preserves_valid_trace _ _ _ _ Hsimul).
Qed.

Any VLSM_embedding determines a VLSM_projection, allowing us to lift to VLSM embeddings the generic results proved about VLSM projections.

Lemma VLSM_weak_embedding_is_projection
  : VLSM_weak_projection X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
VLSM_weak_projection X Y (Some ∘ label_project)
  state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
VLSM_weak_projection X Y (Some ∘ label_project)
  state_project
  split.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
VLSM_projection_type X Y (Some ∘ label_project)
  state_project
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y 
      (state_project sX)
      (pre_VLSM_projection_finite_trace_project X Y
         (Some ∘ label_project) state_project trX)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
VLSM_projection_type X Y (Some ∘ label_project)
  state_project by apply VLSM_embedding_projection_type.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (pre_VLSM_projection_finite_trace_project X Y
         (Some ∘ label_project) state_project trX) by apply VLSM_weak_embedding_finite_valid_trace_from.
Qed.

Lemma VLSM_weak_embedding_valid_state :
  forall (s : state X) (Hs : valid_state_prop X s),
    valid_state_prop Y (state_project s).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ s : state X,
  valid_state_prop X s
  → valid_state_prop Y (state_project s)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ s : state X,
  valid_state_prop X s
  → valid_state_prop Y (state_project s)
  exact (VLSM_weak_projection_valid_state VLSM_weak_embedding_is_projection).
Qed.

Lemma VLSM_weak_embedding_finite_valid_trace_from_to :
  forall (s f : state X) (tr : list (transition_item X)),
    finite_valid_trace_from_to X s f tr ->
    finite_valid_trace_from_to Y (state_project s) (state_project f)
      (VLSM_weak_embedding_finite_trace_project Hsimul tr).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (s f : state X) (tr : list transition_item),
  finite_valid_trace_from_to X s f tr
  → finite_valid_trace_from_to Y (state_project s)
      (state_project f)
      (VLSM_weak_embedding_finite_trace_project Hsimul
         tr)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (s f : state X) (tr : list transition_item),
  finite_valid_trace_from_to X s f tr
  → finite_valid_trace_from_to Y (state_project s)
      (state_project f)
      (VLSM_weak_embedding_finite_trace_project Hsimul
         tr)
  exact (VLSM_weak_projection_finite_valid_trace_from_to VLSM_weak_embedding_is_projection).
Qed.

Lemma VLSM_weak_embedding_in_futures :
  forall (s1 s2 : state X),
    in_futures X s1 s2 -> in_futures Y (state_project s1) (state_project s2).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ s1 s2 : state X,
  in_futures X s1 s2
  → in_futures Y (state_project s1) (state_project s2)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ s1 s2 : state X,
  in_futures X s1 s2
  → in_futures Y (state_project s1) (state_project s2)
  exact (VLSM_weak_projection_in_futures VLSM_weak_embedding_is_projection).
Qed.

Lemma VLSM_weak_embedding_input_valid_transition
  : forall l s im s' om,
  input_valid_transition X l (s, im) (s', om) ->
  input_valid_transition Y (label_project l) (state_project s, im) (state_project s', om).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → input_valid_transition Y (label_project l)
      (state_project s, im) (state_project s', om)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → input_valid_transition Y (label_project l)
      (state_project s, im) (state_project s', om)
  intros.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
l: label X
s: state X
im: option message
s': state X
om: option message
H: input_valid_transition X l (s, im) (s', om)
input_valid_transition Y (label_project l)
  (state_project s, im) (state_project s', om)
  by apply (VLSM_weak_projection_input_valid_transition VLSM_weak_embedding_is_projection)
      with (lY := label_project l) in H.
Qed.

Lemma VLSM_weak_embedding_input_valid l s im
  : input_valid X l (s, im) -> input_valid Y (label_project l) (state_project s, im).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
l: label X
s: state X
im: option message
input_valid X l (s, im)
→ input_valid Y (label_project l)
    (state_project s, im)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
l: label X
s: state X
im: option message
input_valid X l (s, im)
→ input_valid Y (label_project l)
    (state_project s, im)
  by intros; eapply (VLSM_weak_projection_input_valid VLSM_weak_embedding_is_projection).
Qed.

Lemma VLSM_weak_embedding_infinite_valid_trace_from
  : forall sX trX,
    infinite_valid_trace_from X sX trX ->
    infinite_valid_trace_from Y
      (state_project sX) (VLSM_weak_embedding_infinite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_embedding_infinite_trace_project
         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_embedding_infinite_trace_project
         Hsimul trX)
  intros.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
H: infinite_valid_trace_from X sX trX
infinite_valid_trace_from Y (state_project sX)
  (VLSM_weak_embedding_infinite_trace_project Hsimul
     trX)
  specialize (pre_VLSM_embedding_infinite_trace_project_EqSt
    _ _ label_project state_project trX) as Heq.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
H: infinite_valid_trace_from X sX trX
Heq: let Hinf :
  InfinitelyOften
    (is_Some ∘ (Some ∘ label_project ∘ l)) trX :=
  pre_VLSM_embedding_infinite_trace_project_infinitely_often
    X Y label_project trX in
Streams.EqSt
  (pre_VLSM_embedding_infinite_trace_project X Y
     label_project state_project trX)
  (pre_VLSM_projection_infinite_trace_project X
     Y (Some ∘ label_project) state_project trX
     Hinf)
infinite_valid_trace_from Y (state_project sX)
  (VLSM_weak_embedding_infinite_trace_project Hsimul
     trX)
  apply Streams.sym_EqSt in Heq.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
H: infinite_valid_trace_from X sX trX
Heq: Streams.EqSt
  (pre_VLSM_projection_infinite_trace_project X
     Y (Some ∘ label_project) state_project trX
     (pre_VLSM_embedding_infinite_trace_project_infinitely_often
        X Y label_project trX))
  (pre_VLSM_embedding_infinite_trace_project X Y
     label_project state_project trX)
infinite_valid_trace_from Y (state_project sX)
  (VLSM_weak_embedding_infinite_trace_project Hsimul
     trX)
  apply (infinite_valid_trace_from_EqSt Y _ _ _ Heq).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
H: infinite_valid_trace_from X sX trX
Heq: Streams.EqSt
  (pre_VLSM_projection_infinite_trace_project X
     Y (Some ∘ label_project) state_project trX
     (pre_VLSM_embedding_infinite_trace_project_infinitely_often
        X Y label_project trX))
  (pre_VLSM_embedding_infinite_trace_project X Y
     label_project state_project trX)
infinite_valid_trace_from Y (state_project sX)
  (pre_VLSM_projection_infinite_trace_project X Y
     (Some ∘ label_project) state_project trX
     (pre_VLSM_embedding_infinite_trace_project_infinitely_often
        X Y label_project trX))
  by apply (VLSM_weak_projection_infinite_valid_trace_from
    VLSM_weak_embedding_is_projection sX trX).
Qed.

Lemma VLSM_weak_embedding_can_produce
  (s : state X)
  (om : option message)
  : option_can_produce X s om -> option_can_produce Y (state_project s) om.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
s: state X
om: option message
option_can_produce X s om
→ option_can_produce Y (state_project s) om
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
s: state X
om: option message
option_can_produce X s om
→ option_can_produce Y (state_project s) om
  intros [(s0, im) [l Ht]].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
s: state X
om: option message
s0: state X
im: option message
l: label X
Ht: input_valid_transition X l (s0, im) (s, om)
option_can_produce Y (state_project s) om
  apply VLSM_weak_embedding_input_valid_transition in Ht.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
s: state X
om: option message
s0: state X
im: option message
l: label X
Ht: input_valid_transition Y 
  (label_project l) (state_project s0, im)
  (state_project s, om)
option_can_produce Y (state_project s) om
  by do 2 eexists.
Qed.

Lemma VLSM_weak_embedding_can_emit
  (m : message)
  : can_emit X m -> can_emit Y m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
m: message
can_emit X m → can_emit Y m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
m: message
can_emit X m → can_emit Y m
  repeat rewrite can_emit_iff.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
m: message
(∃ s : state X, can_produce X s m)
→ ∃ s : state Y, can_produce Y s m
  intros [s Hsm].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
m: message
s: state X
Hsm: can_produce X s m
∃ s : state Y, can_produce Y s m exists (state_project s).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
m: message
s: state X
Hsm: can_produce X s m
can_produce Y (state_project s) m revert Hsm.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
m: message
s: state X
can_produce X s m → can_produce Y (state_project s) m
  by apply VLSM_weak_embedding_can_produce.
Qed.

Lemma VLSM_weak_embedding_valid_message
  (Hinitial_valid_message : strong_embedding_initial_message_preservation X Y)
  (m : message)
  : valid_message_prop X m -> valid_message_prop Y m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
valid_message_prop X m → valid_message_prop Y m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
valid_message_prop X m → valid_message_prop Y m
  intros Hm.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
Hm: valid_message_prop X m
valid_message_prop Y m
  apply emitted_messages_are_valid_iff in Hm as [Hinit | Hemit].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
Hinit: initial_message_prop m
valid_message_prop Y m
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
Hemit: can_emit X m
valid_message_prop Y m
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
Hinit: initial_message_prop m
valid_message_prop Y m apply Hinitial_valid_message in Hinit.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
Hinit: initial_message_prop m
valid_message_prop Y m
    by apply initial_message_is_valid.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding X Y label_project
  state_project
Hinitial_valid_message: strong_embedding_initial_message_preservation
  X Y
m: message
Hemit: can_emit X m
valid_message_prop Y m by apply emitted_messages_are_valid, VLSM_weak_embedding_can_emit.
Qed.

End sec_weak_projection_properties.

Section sec_embedding_properties.

Embedding properties

Context
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> label Y}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_embedding X Y label_project state_project)
  .

Lemma VLSM_embedding_finite_trace_last :
  forall (sX : state X) (trX : list (transition_item X)),
    state_project (finite_trace_last sX trX) =
    finite_trace_last (state_project sX) (VLSM_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  state_project (finite_trace_last sX trX) =
  finite_trace_last (state_project sX)
    (VLSM_embedding_finite_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  state_project (finite_trace_last sX trX) =
  finite_trace_last (state_project sX)
    (VLSM_embedding_finite_trace_project Hsimul trX)
  exact (pre_VLSM_embedding_finite_trace_last _ _ label_project state_project).
Qed.

Lemma VLSM_embedding_finite_valid_trace :
  forall (s : state X) (tr : list (transition_item X)),
    finite_valid_trace X s tr ->
    finite_valid_trace Y (state_project s) (VLSM_embedding_finite_trace_project Hsimul tr).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y (state_project s)
      (VLSM_embedding_finite_trace_project Hsimul tr)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y (state_project s)
      (VLSM_embedding_finite_trace_project Hsimul tr)
  exact (full_trace_project_preserves_valid_trace _ _ _ _ Hsimul).
Qed.

Any VLSM_embedding determines a VLSM_projection, allowing us to lift to VLSM embeddings the generic results proved about VLSM projections.

Lemma VLSM_embedding_is_projection
  : VLSM_projection X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
VLSM_projection X Y (Some ∘ label_project)
  state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
VLSM_projection X Y (Some ∘ label_project)
  state_project
  split.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
VLSM_projection_type X Y (Some ∘ label_project)
  state_project
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y 
      (state_project sX)
      (pre_VLSM_projection_finite_trace_project X Y
         (Some ∘ label_project) state_project trX)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
VLSM_projection_type X Y (Some ∘ label_project)
  state_project by apply VLSM_embedding_projection_type.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (pre_VLSM_projection_finite_trace_project X Y
         (Some ∘ label_project) state_project trX) by apply VLSM_embedding_finite_valid_trace.
Qed.

Lemma VLSM_embedding_finite_valid_trace_from :
  forall (s : state X) (tr : list (transition_item X)),
    finite_valid_trace_from X s tr ->
    finite_valid_trace_from Y (state_project s) (VLSM_embedding_finite_trace_project Hsimul tr).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace_from X s tr
  → finite_valid_trace_from Y (state_project s)
      (VLSM_embedding_finite_trace_project Hsimul tr)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace_from X s tr
  → finite_valid_trace_from Y (state_project s)
      (VLSM_embedding_finite_trace_project Hsimul tr)
  exact (VLSM_projection_finite_valid_trace_from VLSM_embedding_is_projection).
Qed.

Lemma VLSM_embedding_finite_valid_trace_init_to :
  forall (s f : state X) (tr : list (transition_item X)),
    finite_valid_trace_init_to X s f tr ->
    finite_valid_trace_init_to Y (state_project s) (state_project f)
      (VLSM_embedding_finite_trace_project Hsimul tr).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s f : state X) (tr : list transition_item),
  finite_valid_trace_init_to X s f tr
  → finite_valid_trace_init_to Y (state_project s)
      (state_project f)
      (VLSM_embedding_finite_trace_project Hsimul tr)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s f : state X) (tr : list transition_item),
  finite_valid_trace_init_to X s f tr
  → finite_valid_trace_init_to Y (state_project s)
      (state_project f)
      (VLSM_embedding_finite_trace_project Hsimul tr)
  exact (VLSM_projection_finite_valid_trace_init_to VLSM_embedding_is_projection).
Qed.

Lemma VLSM_embedding_initial_state :
  forall (is : state X),
    initial_state_prop X is -> initial_state_prop Y (state_project is).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ is : state X,
  initial_state_prop is
  → initial_state_prop (state_project is)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ is : state X,
  initial_state_prop is
  → initial_state_prop (state_project is)
  exact (VLSM_projection_initial_state VLSM_embedding_is_projection).
Qed.

Lemma VLSM_embedding_weaken
  : VLSM_weak_embedding X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
VLSM_weak_embedding X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
VLSM_weak_embedding X Y label_project state_project
  by constructor; apply VLSM_embedding_finite_valid_trace_from.
Qed.

Lemma VLSM_embedding_valid_state :
  forall (s : state X) (Hs : valid_state_prop X s),
    valid_state_prop Y (state_project s).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ s : state X,
  valid_state_prop X s
  → valid_state_prop Y (state_project s)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ s : state X,
  valid_state_prop X s
  → valid_state_prop Y (state_project s)
  exact (VLSM_weak_embedding_valid_state VLSM_embedding_weaken).
Qed.

Lemma VLSM_embedding_finite_valid_trace_from_to :
  forall (s f : state X) (tr : list (transition_item X)),
    finite_valid_trace_from_to X s f tr ->
    finite_valid_trace_from_to Y (state_project s) (state_project f)
      (VLSM_embedding_finite_trace_project Hsimul tr).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s f : state X) (tr : list transition_item),
  finite_valid_trace_from_to X s f tr
  → finite_valid_trace_from_to Y (state_project s)
      (state_project f)
      (VLSM_embedding_finite_trace_project Hsimul tr)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s f : state X) (tr : list transition_item),
  finite_valid_trace_from_to X s f tr
  → finite_valid_trace_from_to Y (state_project s)
      (state_project f)
      (VLSM_embedding_finite_trace_project Hsimul tr)
  exact (VLSM_weak_embedding_finite_valid_trace_from_to VLSM_embedding_weaken).
Qed.

Lemma VLSM_embedding_in_futures :
  forall (s1 s2 : state X),
    in_futures X s1 s2 -> in_futures Y (state_project s1) (state_project s2).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ s1 s2 : state X,
  in_futures X s1 s2
  → in_futures Y (state_project s1) (state_project s2)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ s1 s2 : state X,
  in_futures X s1 s2
  → in_futures Y (state_project s1) (state_project s2)
  exact (VLSM_weak_embedding_in_futures VLSM_embedding_weaken).
Qed.

Lemma VLSM_embedding_input_valid_transition :
  forall l s im s' om,
    input_valid_transition X l (s, im) (s', om) ->
    input_valid_transition Y (label_project l) (state_project s, im) (state_project s', om).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → input_valid_transition Y (label_project l)
      (state_project s, im) (state_project s', om)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → input_valid_transition Y (label_project l)
      (state_project s, im) (state_project s', om)
  exact (VLSM_weak_embedding_input_valid_transition VLSM_embedding_weaken).
Qed.

Lemma VLSM_embedding_input_valid :
  forall l s im,
    input_valid X l (s, im) ->
    input_valid Y (label_project l) (state_project s, im).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (l : label X) (s : state X) (im : option message),
  input_valid X l (s, im)
  → input_valid Y (label_project l)
      (state_project s, im)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (l : label X) (s : state X) (im : option message),
  input_valid X l (s, im)
  → input_valid Y (label_project l)
      (state_project s, im)
  exact (VLSM_weak_embedding_input_valid VLSM_embedding_weaken).
Qed.

Lemma VLSM_embedding_can_produce :
  forall (s : state X) (om : option message),
    option_can_produce X s om -> option_can_produce Y (state_project s) om.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (om : option message),
  option_can_produce X s om
  → option_can_produce Y (state_project s) om
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (om : option message),
  option_can_produce X s om
  → option_can_produce Y (state_project s) om
  exact (VLSM_weak_embedding_can_produce VLSM_embedding_weaken).
Qed.

Lemma VLSM_embedding_can_emit :
  forall (m : message),
    can_emit X m -> can_emit Y m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ m : message, can_emit X m → can_emit Y m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ m : message, can_emit X m → can_emit Y m
  exact (VLSM_weak_embedding_can_emit VLSM_embedding_weaken).
Qed.

Lemma VLSM_embedding_valid_message :
  strong_embedding_initial_message_preservation X Y ->
  forall (m : message),
    valid_message_prop X m -> valid_message_prop Y m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
strong_embedding_initial_message_preservation X Y
→ ∀ m : message,
    valid_message_prop X m → valid_message_prop Y m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
strong_embedding_initial_message_preservation X Y
→ ∀ m : message,
    valid_message_prop X m → valid_message_prop Y m
  exact (fun Hinitial_valid_message =>
    VLSM_weak_embedding_valid_message VLSM_embedding_weaken Hinitial_valid_message).
Qed.

Definition VLSM_embedding_trace_project (t : Trace X) : Trace Y :=
  match t with
  | Finite s tr => Finite (state_project s) (VLSM_embedding_finite_trace_project Hsimul tr)
  | Infinite s tr =>
      Infinite (state_project s) (VLSM_embedding_infinite_trace_project Hsimul tr)
  end.

Lemma VLSM_embedding_infinite_valid_trace_from :
  forall s ls,
    infinite_valid_trace_from X s ls ->
    infinite_valid_trace_from Y (state_project s)
      (VLSM_embedding_infinite_trace_project Hsimul ls).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (ls : Streams.Stream transition_item),
  infinite_valid_trace_from X s ls
  → infinite_valid_trace_from Y (state_project s)
      (VLSM_embedding_infinite_trace_project Hsimul ls)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ (s : state X) (ls : Streams.Stream transition_item),
  infinite_valid_trace_from X s ls
  → infinite_valid_trace_from Y (state_project s)
      (VLSM_embedding_infinite_trace_project Hsimul ls)
  exact (fun s ls => VLSM_weak_embedding_infinite_valid_trace_from VLSM_embedding_weaken s ls).
Qed.

Lemma VLSM_embedding_infinite_valid_trace
  s ls
  : infinite_valid_trace X s ls ->
    infinite_valid_trace Y (state_project s) (VLSM_embedding_infinite_trace_project Hsimul ls).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
ls: Streams.Stream transition_item
infinite_valid_trace X s ls
→ infinite_valid_trace Y (state_project s)
    (VLSM_embedding_infinite_trace_project Hsimul ls)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
ls: Streams.Stream transition_item
infinite_valid_trace X s ls
→ infinite_valid_trace Y (state_project s)
    (VLSM_embedding_infinite_trace_project Hsimul ls)
  intros [Htr His].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
infinite_valid_trace Y (state_project s)
  (VLSM_embedding_infinite_trace_project Hsimul ls) split.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
infinite_valid_trace_from Y (state_project s)
  (VLSM_embedding_infinite_trace_project Hsimul ls)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
initial_state_prop (state_project s)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
infinite_valid_trace_from Y (state_project s)
  (VLSM_embedding_infinite_trace_project Hsimul ls) by apply VLSM_embedding_infinite_valid_trace_from.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
initial_state_prop (state_project s) by apply VLSM_embedding_initial_state.
Qed.

Lemma VLSM_embedding_valid_trace
  : forall t,
    valid_trace_prop X t ->
    valid_trace_prop Y (VLSM_embedding_trace_project t).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ t : Trace,
  valid_trace_prop X t
  → valid_trace_prop Y
      (VLSM_embedding_trace_project t)
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
∀ t : Trace,
  valid_trace_prop X t
  → valid_trace_prop Y
      (VLSM_embedding_trace_project t)
  intros [s tr | s tr]; simpl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
tr: list transition_item
finite_valid_trace X s tr
→ finite_valid_trace Y (state_project s)
    (VLSM_embedding_finite_trace_project Hsimul tr)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
tr: Streams.Stream transition_item
infinite_valid_trace X s tr
→ infinite_valid_trace Y 
    (state_project s)
    (VLSM_embedding_infinite_trace_project Hsimul tr)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
tr: list transition_item
finite_valid_trace X s tr
→ finite_valid_trace Y (state_project s)
    (VLSM_embedding_finite_trace_project Hsimul tr) by apply VLSM_embedding_finite_valid_trace.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
s: state X
tr: Streams.Stream transition_item
infinite_valid_trace X s tr
→ infinite_valid_trace Y (state_project s)
    (VLSM_embedding_infinite_trace_project Hsimul tr) by apply VLSM_embedding_infinite_valid_trace.
Qed.

VLSM_embedding almost implies inclusion of the valid_state_message_prop sets. Some additional hypotheses are required because VLSM_embedding only refers to traces, and valid_initial_state_message means that valid_state_message_prop includes some pairs that do not appear in any transition.

Lemma VLSM_embedding_valid_state_message
  (Hmessage : strong_embedding_initial_message_preservation X Y)
  : forall s om, valid_state_message_prop X s om -> valid_state_message_prop Y (state_project s) om.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
∀ (s : state X) (om : option message),
  valid_state_message_prop X s om
  → valid_state_message_prop Y (state_project s) om
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
∀ (s : state X) (om : option message),
  valid_state_message_prop X s om
  → valid_state_message_prop Y (state_project s) om
  intros s om Hsom.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
Hsom: valid_state_message_prop X s om
valid_state_message_prop Y (state_project s) om
  apply option_can_produce_valid_iff.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
Hsom: valid_state_message_prop X s om
option_can_produce Y (state_project s) om
∨ initial_state_prop (state_project s)
  ∧ option_initial_message_prop Y om
  apply option_can_produce_valid_iff in Hsom as [Hgen | [His Him]].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
Hgen: option_can_produce X s om
option_can_produce Y (state_project s) om
∨ initial_state_prop (state_project s)
  ∧ option_initial_message_prop Y om
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
His: initial_state_prop s
Him: option_initial_message_prop X om
option_can_produce Y (state_project s) om
∨ initial_state_prop (state_project s)
  ∧ option_initial_message_prop Y om
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
Hgen: option_can_produce X s om
option_can_produce Y (state_project s) om
∨ initial_state_prop (state_project s)
  ∧ option_initial_message_prop Y om by left; apply VLSM_embedding_can_produce.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
His: initial_state_prop s
Him: option_initial_message_prop X om
option_can_produce Y (state_project s) om
∨ initial_state_prop (state_project s)
  ∧ option_initial_message_prop Y om right; split.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
His: initial_state_prop s
Him: option_initial_message_prop X om
initial_state_prop (state_project s)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
His: initial_state_prop s
Him: option_initial_message_prop X om
option_initial_message_prop Y om
    +message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
His: initial_state_prop s
Him: option_initial_message_prop X om
initial_state_prop (state_project s) by apply VLSM_embedding_initial_state.
    +message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding X Y label_project
  state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
s: state X
om: option message
His: initial_state_prop s
Him: option_initial_message_prop X om
option_initial_message_prop Y om by destruct om as [m |]; [apply Hmessage |].
Qed.

End sec_embedding_properties.

End sec_VLSM_embedding.

It is natural to look for sufficient conditions for VLSM projections which are easy to verify in a practical setting. One such result is the following.

For VLSM X to fully-project to a VLSM Y, the following set of conditions is sufficient:

X's initial_states project to Y's initial_states
Every message m (including the empty one) which can be input to an input_valid transition in X, is a valid_message in Y
X's input_valid is included in Y's valid.
For all input_valid inputs (in X), Y's transition acts

like X's transition.

Section sec_basic_VLSM_embedding.

Basic full VLSM projection

Context
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> label Y)
  (state_project : state X -> state Y)
  (Hvalid : weak_embedding_valid_preservation X Y label_project state_project)
  (Htransition : weak_embedding_transition_preservation X Y label_project state_project)
  .

Section sec_weak_embedding.

Weak full VLSM projection

Context
  (Hstate : weak_projection_initial_state_preservation X Y state_project)
  (Hmessage : weak_embedding_initial_message_preservation X Y state_project)
  .

Lemma weak_projection_valid_message_preservation_from_full
  : weak_projection_valid_message_preservation X Y (Some ∘ label_project) state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
weak_projection_valid_message_preservation X Y
  (Some ∘ label_project) state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
weak_projection_valid_message_preservation X Y
  (Some ∘ label_project) state_project
  intros lX lY Hl s m Hv HsY.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
s: state X
m: message
Hv: input_valid X lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
valid_message_prop Y m
  apply proj2 in Hv as Hom.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
s: state X
m: message
Hv: input_valid X lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
Hom: option_valid_message_prop X (Some m)
∧ valid lX (s, Some m)
valid_message_prop Y m
  apply proj1 in Hom.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
s: state X
m: message
Hv: input_valid X lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
Hom: option_valid_message_prop X (Some m)
valid_message_prop Y m
  apply emitted_messages_are_valid_iff in Hom.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
s: state X
m: message
Hv: input_valid X lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
Hom: initial_message_prop m ∨ can_emit X m
valid_message_prop Y m
  destruct Hom as [Him | Hemit]; [by apply (Hmessage _ _ _ Hv) |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
s: state X
m: message
Hv: input_valid X lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
Hemit: can_emit X m
valid_message_prop Y m
  apply can_emit_has_trace in Hemit as [is [tr [item [Htr Hm]]]].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
s: state X
m: message
Hv: input_valid X lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
item: transition_item
Htr: finite_valid_trace X is (tr ++ [item])
Hm: output item = Some m
valid_message_prop Y m
  destruct item.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: (Some ∘ label_project) lX = Some lY
s: state X
m: message
Hv: input_valid X lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
output: option message
Htr: finite_valid_trace X is
  (tr ++
   [{|
      l := l;
      input := input;
      destination := destination;
      output := output
    |}])
Hm: VLSM.output
  {|
    l := l;
    input := input;
    destination := destination;
    output := output
  |} = Some m
valid_message_prop Y m simpl in *.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
output: option message
Htr: finite_valid_trace X is
  (tr ++
   [{|
      l := l;
      input := input;
      destination := destination;
      output := output
    |}])
Hm: output = Some m
valid_message_prop Y m subst.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
Htr: finite_valid_trace X is
  (tr ++
   [{|
      l := l;
      input := input;
      destination := destination;
      output := Some m
    |}])
valid_message_prop Y m
  apply valid_trace_add_default_last in Htr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
Htr: finite_valid_trace_init_to X is
  (finite_trace_last is
     (tr ++
      [{|
         l := l;
         input := input;
         destination := destination;
         output := Some m
       |}]))
  (tr ++
   [{|
      l := l;
      input := input;
      destination := destination;
      output := Some m
    |}])
valid_message_prop Y m
  rewrite finite_trace_last_is_last in Htr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
Htr: finite_valid_trace_init_to X is
  (VLSM.destination
     {|
       l := l;
       input := input;
       destination := destination;
       output := Some m
     |})
  (tr ++
   [{|
      l := l;
      input := input;
      destination := destination;
      output := Some m
    |}])
valid_message_prop Y m simpl in Htr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
Htr: finite_valid_trace_init_to X is destination
  (tr ++
   [{|
      l := l;
      input := input;
      destination := destination;
      output := Some m
    |}])
valid_message_prop Y m
  remember (tr ++ _) as tr'.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
tr': list transition_item
Heqtr': tr' =
tr ++
[{|
   l := l;
   input := input;
   destination := destination;
   output := Some m
 |}]
Htr: finite_valid_trace_init_to X is destination tr'
valid_message_prop Y m
  cut (option_valid_message_prop Y (Some m)); [done |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
tr': list transition_item
Heqtr': tr' =
tr ++
[{|
   l := l;
   input := input;
   destination := destination;
   output := Some m
 |}]
Htr: finite_valid_trace_init_to X is destination tr'
option_valid_message_prop Y (Some m)
  exists (state_project destination).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
lX: label X
lY: label Y
Hl: Some (label_project lX) = Some lY
s: state X
m: message
Hv: valid_state_prop X s
∧ option_valid_message_prop X (Some m)
  ∧ valid lX (s, Some m)
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
tr': list transition_item
Heqtr': tr' =
tr ++
[{|
   l := l;
   input := input;
   destination := destination;
   output := Some m
 |}]
Htr: finite_valid_trace_init_to X is destination tr'
valid_state_message_prop Y (state_project destination)
  (Some m)
  clear Hv Hl lX lY.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is: state X
tr: list transition_item
l: label X
input: option message
destination: state X
tr': list transition_item
Heqtr': tr' =
tr ++
[{|
   l := l;
   input := input;
   destination := destination;
   output := Some m
 |}]
Htr: finite_valid_trace_init_to X is destination tr'
valid_state_message_prop Y (state_project destination)
  (Some m)
  revert tr l input Heqtr'.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, destination: state X
tr': list transition_item
Htr: finite_valid_trace_init_to X is destination tr'
∀ (tr : list transition_item) (l : label X) (input : 
                                             option
                                               message),
  tr' =
  tr ++
  [{|
     l := l;
     input := input;
     destination := destination;
     output := Some m
   |}]
  → valid_state_message_prop Y
      (state_project destination) (Some m)
  generalize (Some m) as om.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, destination: state X
tr': list transition_item
Htr: finite_valid_trace_init_to X is destination tr'
∀ (om : option message) (tr : list transition_item) 
  (l : label X) (input : option message),
  tr' =
  tr ++
  [{|
     l := l;
     input := input;
     destination := destination;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project destination) om
  induction Htr using finite_valid_trace_init_to_rev_strong_ind
  ; intros; [by destruct tr; simpl in *; congruence |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s0, iom) (sf, oom)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
om: option message
tr0: list transition_item
l0: label X
input: option message
Heqtr': tr ++
[{|
   l := l;
   input := iom;
   destination := sf;
   output := oom
 |}] =
tr0 ++
[{|
   l := l0;
   input := input;
   destination := sf;
   output := om
 |}]
valid_state_message_prop Y (state_project sf) om
  apply app_inj_tail in Heqtr' as [Heqtr Heqitem].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s0, iom) (sf, oom)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
om: option message
tr0: list transition_item
l0: label X
input: option message
Heqtr: tr = tr0
Heqitem: {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|} =
{|
  l := l0;
  input := input;
  destination := sf;
  output := om
|}
valid_state_message_prop Y (state_project sf) om
  subst tr0.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s0, iom) (sf, oom)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
om: option message
l0: label X
input: option message
Heqitem: {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|} =
{|
  l := l0;
  input := input;
  destination := sf;
  output := om
|}
valid_state_message_prop Y (state_project sf) om
  inversion Heqitem.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s0, iom) (sf, oom)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
om: option message
l0: label X
input: option message
Heqitem: {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|} =
{|
  l := l0;
  input := input;
  destination := sf;
  output := om
|}
H0: l = l0
H1: iom = input
H2: oom = om
valid_state_message_prop Y (state_project sf) om subst l0 input oom.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Heqitem: {|
  l := l;
  input := iom;
  destination := sf;
  output := om
|} =
{|
  l := l;
  input := iom;
  destination := sf;
  output := om
|}
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_message_prop Y (state_project sf) om clear Heqitem.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_message_prop Y (state_project sf) om
  assert (Hs : valid_state_prop Y (state_project s0)).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_prop Y (state_project s0)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Hs: valid_state_prop Y (state_project s0)
valid_state_message_prop Y (state_project sf) om
  {message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_prop Y (state_project s0)
    destruct_list_last tr s_tr' s_item Heqtr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 []
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Heqtr: tr = []
valid_state_prop Y (state_project s0)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr, s_tr': list transition_item
s_item: transition_item
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++ [s_item])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  s_tr' ++ [s_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Heqtr: tr = s_tr' ++ [s_item]
valid_state_prop Y (state_project s0)
    -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 []
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Heqtr: tr = []
valid_state_prop Y (state_project s0) subst tr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
Htr1: finite_valid_trace_init_to X is s0 []
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_prop Y (state_project s0) destruct Htr1 as [Hs His].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
Hs: finite_valid_trace_from_to X is s0 []
His: initial_state_prop is
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_prop Y (state_project s0)
      inversion Hs.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
Hs: finite_valid_trace_from_to X is s0 []
His: initial_state_prop is
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
s1: state X
Hs0: valid_state_prop X s0
H: s1 = is
H0: is = s0
valid_state_prop Y (state_project s0) subst.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
s0: state X
His: initial_state_prop s0
Hs: finite_valid_trace_from_to X s0 s0 []
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Hs0: valid_state_prop X s0
valid_state_prop Y (state_project s0)
      by apply Hstate.
    -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr, s_tr': list transition_item
s_item: transition_item
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++ [s_item])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  s_tr' ++ [s_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Heqtr: tr = s_tr' ++ [s_item]
valid_state_prop Y (state_project s0) subst.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
s_tr': list transition_item
s_item: transition_item
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++ [s_item])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  s_tr' ++ [s_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_prop Y (state_project s0)
      apply valid_trace_get_last in Htr1 as Hs0.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
s_tr': list transition_item
s_item: transition_item
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++ [s_item])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  s_tr' ++ [s_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Hs0: finite_trace_last is (s_tr' ++ [s_item]) = s0
valid_state_prop Y (state_project s0)
      rewrite finite_trace_last_is_last in Hs0.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
s_tr': list transition_item
s_item: transition_item
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++ [s_item])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  s_tr' ++ [s_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Hs0: destination s_item = s0
valid_state_prop Y (state_project s0)
      destruct s_item.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
s_tr': list transition_item
l0: label X
input: option message
destination: state X
output: option message
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++
   [{|
      l := l0;
      input := input;
      destination := destination;
      output := output
    |}])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input0 : option message),
  s_tr' ++
  [{|
     l := l0;
     input := input;
     destination := destination;
     output := output
   |}] =
  tr ++
  [{|
     l := l;
     input := input0;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Hs0: VLSM.destination
  {|
    l := l0;
    input := input;
    destination := destination;
    output := output
  |} = s0
valid_state_prop Y (state_project s0) simpl in Hs0.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
s_tr': list transition_item
l0: label X
input: option message
destination: state X
output: option message
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++
   [{|
      l := l0;
      input := input;
      destination := destination;
      output := output
    |}])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input0 : option message),
  s_tr' ++
  [{|
     l := l0;
     input := input;
     destination := destination;
     output := output
   |}] =
  tr ++
  [{|
     l := l;
     input := input0;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Hs0: destination = s0
valid_state_prop Y (state_project s0) subst destination.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
s_tr': list transition_item
l0: label X
input, output: option message
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++
   [{|
      l := l0;
      input := input;
      destination := s0;
      output := output
    |}])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input0 : option message),
  s_tr' ++
  [{|
     l := l0;
     input := input;
     destination := s0;
     output := output
   |}] =
  tr ++
  [{|
     l := l;
     input := input0;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_prop Y (state_project s0)
      specialize (IHHtr1 _ _ _ _ eq_refl).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
s_tr': list transition_item
l0: label X
input, output: option message
Htr1: finite_valid_trace_init_to X is s0
  (s_tr' ++
   [{|
      l := l0;
      input := input;
      destination := s0;
      output := output
    |}])
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: valid_state_message_prop Y 
  (state_project s0) output
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
valid_state_prop Y (state_project s0)
      by eexists.
  }message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
Hs: valid_state_prop Y (state_project s0)
valid_state_message_prop Y (state_project sf) om
  destruct Hs as [_om Hs].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
valid_state_message_prop Y (state_project sf) om
  assert (Hom : option_valid_message_prop Y iom).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y iom
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
Hom: option_valid_message_prop Y iom
valid_state_message_prop Y (state_project sf) om
  {message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y iom
    destruct iom as [im |]; [| by apply option_valid_message_None].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr (Some im)
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im)
    unfold empty_initial_message_or_final_output in Heqiom.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: match has_last_or_null iom_tr with
| inleft (existT x (x0 ↾ _)) =>
    output x0 = Some im
| inright _ =>
    option_initial_message_prop X (Some im)
end
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im)
    destruct_list_last iom_tr iom_tr' iom_item Heqiom_tr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom_tr: iom_tr = []
Heqiom: option_initial_message_prop X (Some im)
Htr2: finite_valid_trace_init_to X iom_si iom_s []
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr, iom_tr': list transition_item
iom_item: transition_item
Heqiom_tr: iom_tr = iom_tr' ++ [iom_item]
Heqiom: output iom_item = Some im
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++ [iom_item])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr' ++ [iom_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im)
    -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom_tr: iom_tr = []
Heqiom: option_initial_message_prop X (Some im)
Htr2: finite_valid_trace_init_to X iom_si iom_s []
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  [] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im) by apply (Hmessage _ _ _ (proj1 Ht)); [eexists |].
    -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr, iom_tr': list transition_item
iom_item: transition_item
Heqiom_tr: iom_tr = iom_tr' ++ [iom_item]
Heqiom: output iom_item = Some im
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++ [iom_item])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr' ++ [iom_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im) subst.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr': list transition_item
iom_item: transition_item
Heqiom: output iom_item = Some im
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++ [iom_item])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr' ++ [iom_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im)
      apply valid_trace_get_last in Htr2 as Hs0.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr': list transition_item
iom_item: transition_item
Heqiom: output iom_item = Some im
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++ [iom_item])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr' ++ [iom_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
Hs0: finite_trace_last iom_si (iom_tr' ++ [iom_item]) =
iom_s
option_valid_message_prop Y (Some im)
      rewrite finite_trace_last_is_last in Hs0.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr': list transition_item
iom_item: transition_item
Heqiom: output iom_item = Some im
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++ [iom_item])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr' ++ [iom_item] =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
Hs0: destination iom_item = iom_s
option_valid_message_prop Y (Some im)
      destruct iom_item.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr': list transition_item
l0: label X
input: option message
destination: state X
output: option message
Heqiom: VLSM.output
  {|
    l := l0;
    input := input;
    destination := destination;
    output := output
  |} = Some im
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++
   [{|
      l := l0;
      input := input;
      destination := destination;
      output := output
    |}])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input0 : option message),
  iom_tr' ++
  [{|
     l := l0;
     input := input;
     destination := destination;
     output := output
   |}] =
  tr ++
  [{|
     l := l;
     input := input0;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
Hs0: VLSM.destination
  {|
    l := l0;
    input := input;
    destination := destination;
    output := output
  |} = iom_s
option_valid_message_prop Y (Some im) simpl in *.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr': list transition_item
l0: label X
input: option message
destination: state X
output: option message
Heqiom: output = Some im
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++
   [{|
      l := l0;
      input := input;
      destination := destination;
      output := output
    |}])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input0 : option message),
  iom_tr' ++
  [{|
     l := l0;
     input := input;
     destination := destination;
     output := output
   |}] =
  tr ++
  [{|
     l := l;
     input := input0;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
Hs0: destination = iom_s
option_valid_message_prop Y (Some im) subst.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr': list transition_item
l0: label X
input: option message
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++
   [{|
      l := l0;
      input := input;
      destination := iom_s;
      output := Some im
    |}])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input0 : option message),
  iom_tr' ++
  [{|
     l := l0;
     input := input;
     destination := iom_s;
     output := Some im
   |}] =
  tr ++
  [{|
     l := l;
     input := input0;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im)
      specialize (IHHtr2 _ _ _ _ eq_refl).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
im: message
iom_si, iom_s: state X
iom_tr': list transition_item
l0: label X
input: option message
Htr2: finite_valid_trace_init_to X iom_si iom_s
  (iom_tr' ++
   [{|
      l := l0;
      input := input;
      destination := iom_s;
      output := Some im
    |}])
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, Some im) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: valid_state_message_prop Y
  (state_project iom_s) 
  (Some im)
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
option_valid_message_prop Y (Some im)
      by eexists.
  }message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
Hom: option_valid_message_prop Y iom
valid_state_message_prop Y (state_project sf) om
  destruct Hom as [_s Hom].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
_s: state Y
Hom: valid_state_message_prop Y _s iom
valid_state_message_prop Y (state_project sf) om
  apply (valid_generated_state_message Y _ _ Hs _ _ Hom (label_project l)).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
_s: state Y
Hom: valid_state_message_prop Y _s iom
valid (label_project l) (state_project s0, iom)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
_s: state Y
Hom: valid_state_message_prop Y _s iom
transition (label_project l) (state_project s0, iom) =
(state_project sf, om)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
_s: state Y
Hom: valid_state_message_prop Y _s iom
valid (label_project l) (state_project s0, iom) by apply Hvalid; [apply Ht | exists _om | exists _s].
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
s: state X
m: message
HsY: valid_state_prop Y (state_project s)
is, s0: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s0 tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
l: label X
om: option message
Ht: input_valid_transition X l (s0, iom) (sf, om)
IHHtr1: ∀ (om : option message) 
  (tr0 : list transition_item) 
  (l : label X) (input : option message),
  tr =
  tr0 ++
  [{|
     l := l;
     input := input;
     destination := s0;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project s0) om
IHHtr2: ∀ (om : option message) 
  (tr : list transition_item) 
  (l : label X) (input : option message),
  iom_tr =
  tr ++
  [{|
     l := l;
     input := input;
     destination := iom_s;
     output := om
   |}]
  → valid_state_message_prop Y
      (state_project iom_s) om
_om: option message
Hs: valid_state_message_prop Y (state_project s0) _om
_s: state Y
Hom: valid_state_message_prop Y _s iom
transition (label_project l) (state_project s0, iom) =
(state_project sf, om) by apply Htransition.
Qed.

Lemma basic_VLSM_weak_embedding : VLSM_weak_embedding X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
VLSM_weak_embedding X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
VLSM_weak_embedding X Y label_project state_project
  specialize (basic_VLSM_weak_projection X Y (Some ∘ label_project) state_project) as Hproj.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: weak_projection_valid_preservation X Y
  (Some ∘ label_project) state_project
→ weak_projection_transition_preservation_Some
    X Y (Some ∘ label_project) state_project
  → weak_projection_transition_consistency_None
      X Y (Some ∘ label_project) state_project
    → weak_projection_initial_state_preservation
        X Y state_project
      → weak_projection_valid_message_preservation
          X Y (Some ∘ label_project)
          state_project
        → VLSM_weak_projection X Y
            (Some ∘ label_project)
            state_project
VLSM_weak_embedding X Y label_project state_project
  spec Hproj; [by apply weak_projection_valid_preservation_from_full |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: weak_projection_transition_preservation_Some X
  Y (Some ∘ label_project) state_project
→ weak_projection_transition_consistency_None
    X Y (Some ∘ label_project) state_project
  → weak_projection_initial_state_preservation
      X Y state_project
    → weak_projection_valid_message_preservation
        X Y (Some ∘ label_project)
        state_project
      → VLSM_weak_projection X Y
          (Some ∘ label_project) state_project
VLSM_weak_embedding X Y label_project state_project
  spec Hproj; [by apply weak_projection_transition_preservation_Some_from_full |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: weak_projection_transition_consistency_None X
  Y (Some ∘ label_project) state_project
→ weak_projection_initial_state_preservation X
    Y state_project
  → weak_projection_valid_message_preservation
      X Y (Some ∘ label_project) state_project
    → VLSM_weak_projection X Y
        (Some ∘ label_project) state_project
VLSM_weak_embedding X Y label_project state_project
  spec Hproj; [by apply weak_projection_transition_consistency_None_from_full |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: weak_projection_initial_state_preservation X Y
  state_project
→ weak_projection_valid_message_preservation X
    Y (Some ∘ label_project) state_project
  → VLSM_weak_projection X Y
      (Some ∘ label_project) state_project
VLSM_weak_embedding X Y label_project state_project
  spec Hproj; [done |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: weak_projection_valid_message_preservation X Y
  (Some ∘ label_project) state_project
→ VLSM_weak_projection X Y
    (Some ∘ label_project) state_project
VLSM_weak_embedding X Y label_project state_project
  spec Hproj; [by apply weak_projection_valid_message_preservation_from_full |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: VLSM_weak_projection X Y
  (Some ∘ label_project) state_project
VLSM_weak_embedding X Y label_project state_project
  constructor.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: VLSM_weak_projection X Y
  (Some ∘ label_project) state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (pre_VLSM_embedding_finite_trace_project X Y
         label_project state_project trX) intro; intros.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
Hproj: VLSM_weak_projection X Y
  (Some ∘ label_project) state_project
sX: state X
trX: list transition_item
H: finite_valid_trace_from X sX trX
finite_valid_trace_from Y (state_project sX)
  (pre_VLSM_embedding_finite_trace_project X Y
     label_project state_project trX)
  by apply (VLSM_weak_projection_finite_valid_trace_from Hproj) in H.
Qed.

End sec_weak_embedding.

Lemma basic_VLSM_weak_embedding_strengthen
  (Hweak : VLSM_weak_embedding X Y label_project state_project)
  (Hstate : strong_projection_initial_state_preservation X Y state_project)
  : VLSM_embedding X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
VLSM_embedding X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
VLSM_embedding X Y label_project state_project
  constructor.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (pre_VLSM_embedding_finite_trace_project X Y
         label_project state_project trX) intros sX trX [HtrX HsX].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace Y (state_project sX)
  (pre_VLSM_embedding_finite_trace_project X Y
     label_project state_project trX)
  split.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (pre_VLSM_embedding_finite_trace_project X Y
     label_project state_project trX)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (pre_VLSM_embedding_finite_trace_project X Y
     label_project state_project trX) by apply (VLSM_weak_embedding_finite_valid_trace_from Hweak).
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hweak: VLSM_weak_embedding X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX) by apply Hstate.
Qed.

Lemma basic_VLSM_embedding
  (Hstate : strong_projection_initial_state_preservation X Y state_project)
  (Hmessage : weak_embedding_initial_message_preservation X Y state_project)
  : VLSM_embedding X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
VLSM_embedding X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
VLSM_embedding X Y label_project state_project
  apply basic_VLSM_weak_embedding_strengthen; [| done].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
VLSM_weak_embedding X Y label_project state_project
  apply basic_VLSM_weak_embedding; [| done].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: weak_embedding_valid_preservation X Y
  label_project state_project
Htransition: weak_embedding_transition_preservation X
  Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_embedding_initial_message_preservation
  X Y state_project
weak_projection_initial_state_preservation X Y
  state_project
  by apply strong_projection_initial_state_preservation_weaken.
Qed.

End sec_basic_VLSM_embedding.

Lemma basic_VLSM_strong_embedding
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> label Y)
  (state_project : state X -> state Y)
  (Hvalid : strong_embedding_valid_preservation X Y label_project state_project)
  (Htransition : strong_embedding_transition_preservation X Y label_project state_project)
  (Hstate : strong_projection_initial_state_preservation X Y state_project)
  (Hmessage : strong_embedding_initial_message_preservation X Y)
  : VLSM_embedding X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
VLSM_embedding X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
VLSM_embedding X Y label_project state_project
  apply basic_VLSM_embedding.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
weak_embedding_valid_preservation X Y label_project
  state_project
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
weak_embedding_transition_preservation X Y
  label_project state_project
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
strong_projection_initial_state_preservation X Y
  state_project
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
weak_embedding_initial_message_preservation X Y
  state_project
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
weak_embedding_valid_preservation X Y label_project
  state_project by apply strong_embedding_valid_preservation_weaken.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
weak_embedding_transition_preservation X Y
  label_project state_project by apply strong_embedding_transition_preservation_weaken.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
strong_projection_initial_state_preservation X Y
  state_project done.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y
  label_project state_project
Htransition: strong_embedding_transition_preservation
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_embedding_initial_message_preservation
  X Y
weak_embedding_initial_message_preservation X Y
  state_project by apply strong_embedding_initial_message_preservation_weaken.
Qed.