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

Core: VLSM Stuttering Embeddings

Stuttering embeddings are VLSM projections guaranteeing the existence of translations for all states and traces, in which a transition in the source VLSM translates to a (possibly empty) sequence of transitions in the target VLSM.

A stuttering embedding is established from VLSM X to VLSM Y (sharing the same messages) if there exists maps state_project taking X-states to Y-states, and transition_item_project, taking a transition from X to a list of transitions in Y, such that:

transition_item_project_consistency: the state-translation of the destination of a transition is the final state of the translation of the transition.
stuttering_embedding_preserves_valid_traces: traces obtained by concatenating the translations of transition of a valid trace are valid.

An example of proper stuttering embedding is given by a VLSM summarizing the transitions of another VLSM.

Section sec_pre_definitions.

Context
  {message : Type}
  {TX TY : VLSMType message}
  (state_project : state TX -> state TY)
  (transition_item_project : transition_item TX -> list (transition_item TY))
  .

Definition pre_VLSM_stuttering_embedding_finite_trace_project :
  list (transition_item TX) -> list (transition_item TY) :=
    mbind transition_item_project.

Definition pre_VLSM_stuttering_embedding_infinite_trace_project
  (s : Streams.Stream (transition_item TX))
  (Hs : InfinitelyOften (fun item => transition_item_project item <> []) s)
  : Streams.Stream (transition_item TY) :=
  stream_concat_map transition_item_project s Hs.

Definition pre_VLSM_stuttering_embedding_infinite_finite_trace_project
  (s : Streams.Stream (transition_item TX))
  (Hs : FinitelyManyBound (fun item => transition_item_project item <> []) s)
  : list (transition_item TY) :=
  bounded_stream_concat_map transition_item_project s Hs.

Lemma pre_VLSM_stuttering_embedding_finite_trace_project_app :
  forall (l1 l2 : list (transition_item TX)),
    pre_VLSM_stuttering_embedding_finite_trace_project (l1 ++ l2)
      =
    pre_VLSM_stuttering_embedding_finite_trace_project l1
      ++ pre_VLSM_stuttering_embedding_finite_trace_project l2.message: Type
TX, TY: VLSMType message
state_project: state TX → state TY
transition_item_project: transition_item
→ list transition_item
∀ l1 l2 : list transition_item,
  pre_VLSM_stuttering_embedding_finite_trace_project
    (l1 ++ l2) =
  pre_VLSM_stuttering_embedding_finite_trace_project
    l1 ++
  pre_VLSM_stuttering_embedding_finite_trace_project
    l2
Proof.message: Type
TX, TY: VLSMType message
state_project: state TX → state TY
transition_item_project: transition_item
→ list transition_item
∀ l1 l2 : list transition_item,
  pre_VLSM_stuttering_embedding_finite_trace_project
    (l1 ++ l2) =
  pre_VLSM_stuttering_embedding_finite_trace_project
    l1 ++
  pre_VLSM_stuttering_embedding_finite_trace_project
    l2
  exact (mbind_app _).
Qed.

Lemma elem_of_pre_VLSM_stuttering_embedding_finite_trace_project :
  forall (trX : list (transition_item TX)) (itemY : transition_item TY),
    itemY ∈ pre_VLSM_stuttering_embedding_finite_trace_project trX
      <->
    exists (itemX : transition_item TX), itemY ∈ transition_item_project itemX /\ itemX ∈ trX.message: Type
TX, TY: VLSMType message
state_project: state TX → state TY
transition_item_project: transition_item
→ list transition_item
∀ (trX : list transition_item) (itemY : transition_item),
  itemY
  ∈ pre_VLSM_stuttering_embedding_finite_trace_project
      trX
  ↔ (∃ itemX : transition_item,
       itemY ∈ transition_item_project itemX
       ∧ itemX ∈ trX)
Proof.message: Type
TX, TY: VLSMType message
state_project: state TX → state TY
transition_item_project: transition_item
→ list transition_item
∀ (trX : list transition_item) (itemY : transition_item),
  itemY
  ∈ pre_VLSM_stuttering_embedding_finite_trace_project
      trX
  ↔ (∃ itemX : transition_item,
       itemY ∈ transition_item_project itemX
       ∧ itemX ∈ trX) by intros; apply elem_of_list_bind. Qed.

End sec_pre_definitions.

Record VLSM_stuttering_embedding_type
  {message : Type}
  (X : VLSM message)
  (TY : VLSMType message)
  (state_project : state X -> state TY)
  (transition_item_project : transition_item X -> list (transition_item TY))
  : Prop :=
{
  transition_item_project_consistency :
    forall sX itemX,
      input_valid_transition_item X sX itemX ->
        finite_trace_last (state_project sX) (transition_item_project itemX)
          =
        state_project (destination itemX);
}.

Stuttering embedding definitions and properties

Section sec_stuttering_embedding_type_properties.

Definition strong_transition_item_project_consistency
  {message : Type}
  [X : VLSM message]
  [TY : VLSMType message]
  (state_project : state X -> state TY)
  (transition_item_project : transition_item X -> list (transition_item TY))
  : Prop :=
  forall sX lX inputX destinationX outputX,
    transition X lX (sX, inputX) = (destinationX, outputX) ->
    finite_trace_last (state_project sX)
      (transition_item_project
        {| l := lX; input := inputX; destination := destinationX; output := outputX |})
      =
    state_project destinationX.

Section sec_pre_properties.

Context
  {message : Type}
  (X : VLSM message)
  (TY : VLSMType message)
  (state_project : state X -> state TY)
  (transition_item_project : transition_item X -> list (transition_item TY))
  (Hsimul : VLSM_stuttering_embedding_type X TY state_project transition_item_project)
  .

Lemma pre_VLSM_stuttering_embedding_finite_trace_last :
  forall (s : state X) (tr : list (transition_item X)),
    finite_valid_trace_from X s tr ->
    finite_trace_last (state_project s)
      (pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project tr)
      =
    state_project (finite_trace_last s tr).message: Type
X: VLSM message
TY: VLSMType message
state_project: state X → state TY
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X TY
  state_project transition_item_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace_from X s tr
  → finite_trace_last (state_project s)
      (pre_VLSM_stuttering_embedding_finite_trace_project
         transition_item_project tr) =
    state_project (finite_trace_last s tr)
Proof.message: Type
X: VLSM message
TY: VLSMType message
state_project: state X → state TY
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X TY
  state_project transition_item_project
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace_from X s tr
  → finite_trace_last (state_project s)
      (pre_VLSM_stuttering_embedding_finite_trace_project
         transition_item_project tr) =
    state_project (finite_trace_last s tr)
  induction 1 using finite_valid_trace_from_rev_ind; [done |].message: Type
X: VLSM message
TY: VLSMType message
state_project: state X → state TY
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X TY
  state_project transition_item_project
s: state X
tr: list transition_item
H: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: input_valid_transition X l
  (finite_trace_last s tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHfinite_valid_trace_from: finite_trace_last
  (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project
     tr) =
state_project
  (finite_trace_last s tr)
finite_trace_last (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project (tr ++ [x])) =
state_project (finite_trace_last s (tr ++ [x]))
  erewrite finite_trace_last_is_last,
    pre_VLSM_stuttering_embedding_finite_trace_project_app,
    finite_trace_last_app, IHfinite_valid_trace_from,
    <- transition_item_project_consistency; [| done..].message: Type
X: VLSM message
TY: VLSMType message
state_project: state X → state TY
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X TY
  state_project transition_item_project
s: state X
tr: list transition_item
H: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: input_valid_transition X l
  (finite_trace_last s tr, iom) (
  sf, oom)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
IHfinite_valid_trace_from: finite_trace_last
  (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project
     tr) =
state_project
  (finite_trace_last s tr)
finite_trace_last
  (state_project (finite_trace_last s tr))
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project [x]) =
finite_trace_last
  (state_project (finite_trace_last s tr))
  (transition_item_project x)
  by cbn; rewrite app_nil_r.
Qed.

End sec_pre_properties.

Definition VLSM_partial_trace_project_from_stuttering_embedding
  {message : Type}
  {X : VLSM message}
  {TY : VLSMType message}
  (state_project : state X -> state TY)
  (transition_item_project : transition_item X -> list (transition_item TY))
  (trace_project := pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project)
  (str : state X * list (transition_item X))
  : option (state TY * list (transition_item TY)) :=
    let (s, tr) := str in Some (state_project s, trace_project tr).

Context
  {message : Type}
  {X Y : VLSM message}
  (state_project : state X -> state Y)
  (transition_item_project : transition_item X -> list (transition_item Y))
  (Hsimul : VLSM_stuttering_embedding_type X Y state_project transition_item_project)
  .

Any VLSM_stuttering_embedding_type determines a VLSM_partial_projection_type, allowing us to lift to VLSM stuttering embeddings the generic results proved about VLSM partial projections.

Lemma VLSM_partial_projection_type_from_stuttering_embedding :
  VLSM_partial_projection_type X Y
    (VLSM_partial_trace_project_from_stuttering_embedding state_project transition_item_project).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
  constructor; intros * Hpr * Hlst Htr.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
sX: state X
trX: list transition_item
sY: state Y
trY: list transition_item
Hpr: VLSM_partial_trace_project_from_stuttering_embedding
  state_project transition_item_project
  (sX, trX) = Some (sY, trY)
s'X: state X
preX: list transition_item
Hlst: finite_trace_last s'X preX = sX
Htr: finite_valid_trace_from X s'X (preX ++ trX)
∃ (s'Y : state Y) (preY : list transition_item),
  VLSM_partial_trace_project_from_stuttering_embedding
    state_project transition_item_project
    (s'X, preX ++ trX) = Some (s'Y, preY ++ trY)
  ∧ finite_trace_last s'Y preY = sY
  apply Some_inj, pair_equal_spec in Hpr as [<- <-]; cbn.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
sX: state X
trX: list transition_item
s'X: state X
preX: list transition_item
Hlst: finite_trace_last s'X preX = sX
Htr: finite_valid_trace_from X s'X (preX ++ trX)
∃ (s'Y : state Y) (preY : list transition_item),
  Some
    (state_project s'X,
     pre_VLSM_stuttering_embedding_finite_trace_project
       transition_item_project (preX ++ trX)) =
  Some
    (s'Y,
     preY ++
     pre_VLSM_stuttering_embedding_finite_trace_project
       transition_item_project trX)
  ∧ finite_trace_last s'Y preY = state_project sX
  rewrite pre_VLSM_stuttering_embedding_finite_trace_project_app.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
sX: state X
trX: list transition_item
s'X: state X
preX: list transition_item
Hlst: finite_trace_last s'X preX = sX
Htr: finite_valid_trace_from X s'X (preX ++ trX)
∃ (s'Y : state Y) (preY : list transition_item),
  Some
    (state_project s'X,
     pre_VLSM_stuttering_embedding_finite_trace_project
       transition_item_project preX ++
     pre_VLSM_stuttering_embedding_finite_trace_project
       transition_item_project trX) =
  Some
    (s'Y,
     preY ++
     pre_VLSM_stuttering_embedding_finite_trace_project
       transition_item_project trX)
  ∧ finite_trace_last s'Y preY = state_project sX
  eexists (state_project s'X), _.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
sX: state X
trX: list transition_item
s'X: state X
preX: list transition_item
Hlst: finite_trace_last s'X preX = sX
Htr: finite_valid_trace_from X s'X (preX ++ trX)
Some
  (state_project s'X,
   pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project preX ++
   pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project trX) =
Some
  (state_project s'X,
   ?Goal ++
   pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project trX)
∧ finite_trace_last (state_project s'X) ?Goal =
  state_project sX
  split; [done |].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
sX: state X
trX: list transition_item
s'X: state X
preX: list transition_item
Hlst: finite_trace_last s'X preX = sX
Htr: finite_valid_trace_from X s'X (preX ++ trX)
finite_trace_last (state_project s'X)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project preX) = state_project sX
  apply finite_valid_trace_from_app_iff in Htr as [].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding_type X Y
  state_project transition_item_project
sX: state X
trX: list transition_item
s'X: state X
preX: list transition_item
Hlst: finite_trace_last s'X preX = sX
H: finite_valid_trace_from X s'X preX
H0: finite_valid_trace_from X
  (finite_trace_last s'X preX) trX
finite_trace_last (state_project s'X)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project preX) = state_project sX
  by erewrite pre_VLSM_stuttering_embedding_finite_trace_last, Hlst.
Qed.

End sec_stuttering_embedding_type_properties.

Section sec_VLSM_stuttering_embedding_definitions.

Context
  {message : Type}
  (X Y : VLSM message)
  (state_project : state X -> state Y)
  (transition_item_project : transition_item X -> list (transition_item Y))
  (trace_project := pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project)
  .

Definition stuttering_embedding_input_valid_transition_item_validity : Prop :=
  forall s item,
    input_valid_transition_item X s item ->
    finite_valid_trace_from_to Y (state_project s) (state_project (destination item))
      (transition_item_project item).

Similarly to the VLSM_partial_projection case we distinguish two types of stuttering embeddings: VLSM_weak_stuttering_embedding and VLSM_stuttering_embedding, distinguished by the fact that the weak embeddings are not required to preserve initial states.

Record VLSM_weak_stuttering_embedding : Prop :=
{
  weak_stuttering_embedding_type :>
    VLSM_stuttering_embedding_type X Y state_project transition_item_project;
  weak_stuttering_embedding_preserves_valid_trace :
    forall sX trX,
      finite_valid_trace_from X sX trX ->
      finite_valid_trace_from Y (state_project sX) (trace_project trX);
}.

Record VLSM_stuttering_embedding : Prop :=
{
  stuttering_embedding_type :>
    VLSM_stuttering_embedding_type X Y state_project transition_item_project;
  stuttering_embedding_preserves_valid_trace :
    forall sX trX,
      finite_valid_trace X sX trX -> finite_valid_trace Y (state_project sX) (trace_project trX);
}.

Definition weak_stuttering_embedding_initial_state_preservation : Prop :=
  forall s : state X,
    initial_state_prop X s -> valid_state_prop Y (state_project s).

Definition strong_stuttering_embedding_initial_state_preservation : Prop :=
  forall s : state X,
    initial_state_prop X s -> initial_state_prop Y (state_project s).

Lemma strong_stuttering_embedding_initial_state_preservation_weaken :
  strong_stuttering_embedding_initial_state_preservation ->
    weak_stuttering_embedding_initial_state_preservation.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
trace_project:= pre_VLSM_stuttering_embedding_finite_trace_project
  transition_item_project: list transition_item
→ list transition_item
strong_stuttering_embedding_initial_state_preservation
→ weak_stuttering_embedding_initial_state_preservation
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
trace_project:= pre_VLSM_stuttering_embedding_finite_trace_project
  transition_item_project: list transition_item
→ list transition_item
strong_stuttering_embedding_initial_state_preservation
→ weak_stuttering_embedding_initial_state_preservation
  intros Hstrong s Hs.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
trace_project:= pre_VLSM_stuttering_embedding_finite_trace_project
  transition_item_project: list transition_item
→ list transition_item
Hstrong: strong_stuttering_embedding_initial_state_preservation
s: state X
Hs: initial_state_prop s
valid_state_prop Y (state_project s)
  apply initial_state_is_valid.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
trace_project:= pre_VLSM_stuttering_embedding_finite_trace_project
  transition_item_project: list transition_item
→ list transition_item
Hstrong: strong_stuttering_embedding_initial_state_preservation
s: state X
Hs: initial_state_prop s
initial_state_prop (state_project s)
  by apply Hstrong.
Qed.

End sec_VLSM_stuttering_embedding_definitions.

Section sec_weak_stuttering_embedding_properties.

Context
  {message : Type}
  {X Y : VLSM message}
  {state_project : state X -> state Y}
  {transition_item_project : transition_item X -> list (transition_item Y)}
  .

Section sec_weak_stuttering_embedding_trace_projection_redefinitions.

Here we restate the pre_ definitions above to depend on VLSM_weak_stuttering_embedding and have their state and transition item projection functions implicit.

Definition VLSM_weak_stuttering_embedding_finite_trace_project
  (Hsimul : VLSM_weak_stuttering_embedding X Y state_project transition_item_project)
  : list (transition_item X) -> list (transition_item Y)
  := pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project.

Lemma elem_of_VLSM_weak_stuttering_embedding :
  VLSM_weak_stuttering_embedding X Y state_project transition_item_project ->
  forall (trX : list transition_item) (itemY : transition_item),
    itemY ∈ pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project trX
      <->
    exists itemX : transition_item,
      itemY ∈ transition_item_project itemX /\ itemX ∈ trX.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
VLSM_weak_stuttering_embedding X Y state_project
  transition_item_project
→ ∀ (trX : list transition_item) (itemY : transition_item),
    itemY
    ∈ pre_VLSM_stuttering_embedding_finite_trace_project
        transition_item_project trX
    ↔ (∃ itemX : transition_item,
         itemY ∈ transition_item_project itemX
         ∧ itemX ∈ trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
VLSM_weak_stuttering_embedding X Y state_project
  transition_item_project
→ ∀ (trX : list transition_item) (itemY : transition_item),
    itemY
    ∈ pre_VLSM_stuttering_embedding_finite_trace_project
        transition_item_project trX
    ↔ (∃ itemX : transition_item,
         itemY ∈ transition_item_project itemX
         ∧ itemX ∈ trX)
  exact (fun _ => elem_of_pre_VLSM_stuttering_embedding_finite_trace_project
    transition_item_project).
Qed.

Definition VLSM_weak_stuttering_embedding_infinite_trace_project
  (Hsimul : VLSM_weak_stuttering_embedding X Y state_project transition_item_project)
  (s : Streams.Stream (transition_item X))
  (Hinf : InfinitelyOften (fun item => transition_item_project item <> []) s)
  : Streams.Stream (transition_item Y)
  := pre_VLSM_stuttering_embedding_infinite_trace_project transition_item_project s Hinf.

Definition VLSM_weak_stuttering_embedding_infinite_finite_trace_project
  (Hsimul : VLSM_weak_stuttering_embedding X Y state_project transition_item_project)
  (s : Streams.Stream (transition_item X))
  (Hfin : FinitelyManyBound (fun item => transition_item_project item <> []) s)
  : list (transition_item Y)
  := pre_VLSM_stuttering_embedding_infinite_finite_trace_project transition_item_project s Hfin.

End sec_weak_stuttering_embedding_trace_projection_redefinitions.

While for the above section, the VLSM_weak_stuttering_embedding was necessary to be mentioned explicitly, in the following we make it part of the context.

Context
  (Hsimul : VLSM_weak_stuttering_embedding X Y state_project transition_item_project).

Lemma VLSM_weak_stuttering_embedding_finite_trace_project_app :
  forall l1 l2,
    VLSM_weak_stuttering_embedding_finite_trace_project Hsimul (l1 ++ l2)
      =
    VLSM_weak_stuttering_embedding_finite_trace_project Hsimul l1
      ++ VLSM_weak_stuttering_embedding_finite_trace_project Hsimul l2.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ l1 l2 : list transition_item,
  VLSM_weak_stuttering_embedding_finite_trace_project
    Hsimul (l1 ++ l2) =
  VLSM_weak_stuttering_embedding_finite_trace_project
    Hsimul l1 ++
  VLSM_weak_stuttering_embedding_finite_trace_project
    Hsimul l2
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ l1 l2 : list transition_item,
  VLSM_weak_stuttering_embedding_finite_trace_project
    Hsimul (l1 ++ l2) =
  VLSM_weak_stuttering_embedding_finite_trace_project
    Hsimul l1 ++
  VLSM_weak_stuttering_embedding_finite_trace_project
    Hsimul l2
  exact (pre_VLSM_stuttering_embedding_finite_trace_project_app transition_item_project).
Qed.

Lemma VLSM_weak_stuttering_embedding_finite_trace_last :
  forall sX trX,
    finite_valid_trace_from X sX trX ->
    finite_trace_last (state_project sX)
      (VLSM_weak_stuttering_embedding_finite_trace_project Hsimul trX)
      =
    state_project (finite_trace_last sX trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_trace_last (state_project sX)
      (VLSM_weak_stuttering_embedding_finite_trace_project
         Hsimul trX) =
    state_project (finite_trace_last sX trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_trace_last (state_project sX)
      (VLSM_weak_stuttering_embedding_finite_trace_project
         Hsimul trX) =
    state_project (finite_trace_last sX trX)
  exact (pre_VLSM_stuttering_embedding_finite_trace_last _ _ _ _ Hsimul).
Qed.

Lemma VLSM_weak_stuttering_embedding_finite_valid_trace_from :
  forall sX trX,
    finite_valid_trace_from X sX trX ->
    finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_finite_trace_project
         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_finite_trace_project
         Hsimul trX)
  exact (weak_stuttering_embedding_preserves_valid_trace _ _ _ _ Hsimul).
Qed.

Lemma VLSM_weak_stuttering_embedding_infinite_valid_trace_from :
  forall sX trX (Hinf : InfinitelyOften (fun item => transition_item_project item <> []) trX),
    infinite_valid_trace_from X sX trX ->
    infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_infinite_trace_project Hsimul trX Hinf).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_infinite_trace_project
         Hsimul trX Hinf)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_infinite_trace_project
         Hsimul trX Hinf)
  intros sX trX Hinf HtrX.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
infinite_valid_trace_from Y (state_project sX)
  (VLSM_weak_stuttering_embedding_infinite_trace_project
     Hsimul trX Hinf)
  apply infinite_valid_trace_from_prefix_rev.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
∀ n : nat,
  finite_valid_trace_from Y (state_project sX)
    (stream_prefix
       (VLSM_weak_stuttering_embedding_infinite_trace_project
          Hsimul trX Hinf) n)
  intros n.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
n: nat
finite_valid_trace_from Y (state_project sX)
  (stream_prefix
     (VLSM_weak_stuttering_embedding_infinite_trace_project
        Hsimul trX Hinf) n)
  destruct (stream_concat_map_ex_prefix transition_item_project trX Hinf n)
    as (m & suf & Hrew).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
n, m: nat
suf: list transition_item
Hrew: stream_prefix trX m ≫= transition_item_project =
stream_prefix
  (stream_concat_map transition_item_project
     trX Hinf) n ++ suf
finite_valid_trace_from Y (state_project sX)
  (stream_prefix
     (VLSM_weak_stuttering_embedding_infinite_trace_project
        Hsimul trX Hinf) n)
  apply finite_valid_trace_from_app_iff with (ls' := suf).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
n, m: nat
suf: list transition_item
Hrew: stream_prefix trX m ≫= transition_item_project =
stream_prefix
  (stream_concat_map transition_item_project
     trX Hinf) n ++ suf
finite_valid_trace_from Y (state_project sX)
  (stream_prefix
     (VLSM_weak_stuttering_embedding_infinite_trace_project
        Hsimul trX Hinf) n ++ suf)
  setoid_rewrite <- Hrew.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
n, m: nat
suf: list transition_item
Hrew: stream_prefix trX m ≫= transition_item_project =
stream_prefix
  (stream_concat_map transition_item_project
     trX Hinf) n ++ suf
finite_valid_trace_from Y (state_project sX)
  (stream_prefix trX m ≫= transition_item_project)
  by apply VLSM_weak_stuttering_embedding_finite_valid_trace_from,
    infinite_valid_trace_from_prefix.
Qed.

Lemma VLSM_weak_stuttering_embedding_infinite_finite_valid_trace_from :
  forall sX trX (Hfin : FinitelyManyBound (fun item => transition_item_project item <> []) trX),
    infinite_valid_trace_from X sX trX ->
    finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_infinite_finite_trace_project Hsimul trX Hfin).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_infinite_finite_trace_project
         Hsimul trX Hfin)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_stuttering_embedding_infinite_finite_trace_project
         Hsimul trX Hfin)
  intros sX trX Hfin HtrX.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
finite_valid_trace_from Y (state_project sX)
  (VLSM_weak_stuttering_embedding_infinite_finite_trace_project
     Hsimul trX Hfin)
  apply VLSM_weak_stuttering_embedding_finite_valid_trace_from.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
finite_valid_trace_from X sX
  (stream_prefix trX (`Hfin))
  by apply infinite_valid_trace_from_prefix with (n := `Hfin) in HtrX.
Qed.

Any VLSM_weak_stuttering_embedding determines a VLSM_weak_partial_projection, allowing us to lift to weak stuttering embeddings the generic results proved about weak partial projections.

Lemma VLSM_weak_partial_projection_from_stuttering_embedding :
  VLSM_weak_partial_projection X Y
    (VLSM_partial_trace_project_from_stuttering_embedding state_project transition_item_project).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
  split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_stuttering_embedding
    state_project transition_item_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project) by apply VLSM_partial_projection_type_from_stuttering_embedding, Hsimul.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  VLSM_partial_trace_project_from_stuttering_embedding
    state_project transition_item_project (sX, trX) =
  Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY cbn; intros sX trX sY trY [= <- <-].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_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_stuttering_embedding_finite_trace_project
       transition_item_project trX)
    by apply VLSM_weak_stuttering_embedding_finite_valid_trace_from.
Qed.

Lemma VLSM_weak_stuttering_embedding_valid_state :
  forall sX,
    valid_state_prop X sX -> valid_state_prop Y (state_project sX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
  by intro sX; eapply VLSM_weak_partial_projection_valid_state;
    [apply VLSM_weak_partial_projection_from_stuttering_embedding |].
Qed.

Lemma VLSM_weak_stuttering_embedding_finite_valid_trace_from_to :
  forall sX s'X trX,
    finite_valid_trace_from_to X sX s'X trX ->
      finite_valid_trace_from_to Y (state_project sX) (state_project s'X)
        (VLSM_weak_stuttering_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX s'X : state X) (trX : list transition_item),
  finite_valid_trace_from_to X sX s'X trX
  → finite_valid_trace_from_to Y (state_project sX)
      (state_project s'X)
      (VLSM_weak_stuttering_embedding_finite_trace_project
         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (sX s'X : state X) (trX : list transition_item),
  finite_valid_trace_from_to X sX s'X trX
  → finite_valid_trace_from_to Y (state_project sX)
      (state_project s'X)
      (VLSM_weak_stuttering_embedding_finite_trace_project
         Hsimul trX)
  intros sX s'X trX HtrX.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
finite_valid_trace_from_to Y (state_project sX)
  (state_project s'X)
  (VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul trX)
  apply valid_trace_add_last.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
finite_valid_trace_from Y (state_project sX)
  (VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul trX)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
finite_trace_last (state_project sX)
  (VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul trX) = state_project s'X
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
finite_valid_trace_from Y (state_project sX)
  (VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul trX) eapply VLSM_weak_partial_projection_finite_valid_trace_from.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
VLSM_weak_partial_projection ?X Y ?trace_project
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
?trace_project (?sX, ?trX) =
Some
  (state_project sX,
   VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul trX)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
finite_valid_trace_from ?X ?sX ?trX
    +message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
VLSM_weak_partial_projection ?X Y ?trace_project by apply VLSM_weak_partial_projection_from_stuttering_embedding.
    +message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
VLSM_partial_trace_project_from_stuttering_embedding
  state_project transition_item_project (?sX, ?trX) =
Some
  (state_project sX,
   VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul trX) done.
    +message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
finite_valid_trace_from X sX trX by eapply valid_trace_forget_last.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
finite_trace_last (state_project sX)
  (VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul trX) = state_project s'X rewrite VLSM_weak_stuttering_embedding_finite_trace_last
      by (eapply valid_trace_forget_last; done).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
state_project (finite_trace_last sX trX) =
state_project s'X
    by erewrite finite_valid_trace_from_to_last.
Qed.

Lemma VLSM_weak_stuttering_embedding_in_futures :
  forall s1 s2,
    in_futures X s1 s2 -> in_futures Y (state_project s1) (state_project s2).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_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
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ s1 s2 : state X,
  in_futures X s1 s2
  → in_futures Y (state_project s1) (state_project s2)
  intros s1 s2 [tr Htr].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
s1, s2: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X s1 s2 tr
in_futures Y (state_project s1) (state_project s2)
  exists (VLSM_weak_stuttering_embedding_finite_trace_project Hsimul tr).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
s1, s2: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X s1 s2 tr
finite_valid_trace_from_to Y (state_project s1)
  (state_project s2)
  (VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul tr)
  by revert Htr; apply VLSM_weak_stuttering_embedding_finite_valid_trace_from_to.
Qed.

Lemma VLSM_weak_stuttering_embedding_input_valid_transition_item :
  forall s item,
    input_valid_transition_item X s item ->
    finite_valid_trace_from_to Y (state_project s)
      (state_project (destination item)) (transition_item_project item).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (s : state X) (item : transition_item),
  input_valid_transition_item X s item
  → finite_valid_trace_from_to Y (state_project s)
      (state_project (destination item))
      (transition_item_project item)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
∀ (s : state X) (item : transition_item),
  input_valid_transition_item X s item
  → finite_valid_trace_from_to Y (state_project s)
      (state_project (destination item))
      (transition_item_project item)
  intros.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
s: state X
item: transition_item
H: input_valid_transition_item X s item
finite_valid_trace_from_to Y (state_project s)
  (state_project (destination item))
  (transition_item_project item)
  replace (transition_item_project item)
    with (VLSM_weak_stuttering_embedding_finite_trace_project Hsimul [item])
    by apply app_nil_r.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
s: state X
item: transition_item
H: input_valid_transition_item X s item
finite_valid_trace_from_to Y (state_project s)
  (state_project (destination item))
  (VLSM_weak_stuttering_embedding_finite_trace_project
     Hsimul [item])
  apply VLSM_weak_stuttering_embedding_finite_valid_trace_from_to.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
s: state X
item: transition_item
H: input_valid_transition_item X s item
finite_valid_trace_from_to X s (destination item)
  [item]
  by destruct item; apply finite_valid_trace_from_to_singleton.
Qed.

End sec_weak_stuttering_embedding_properties.

Section sec_stuttering_embedding_properties.

Context
  {message : Type}
  {X Y : VLSM message}
  {state_project : state X -> state Y}
  {transition_item_project : transition_item X -> list (transition_item Y)}
  .

Section sec_stuttering_embedding_trace_projection_redefinitions.

Here we restate the pre_ definitions above to depend on VLSM_stuttering_embedding and have their state and transition item projection functions implicit.

Definition VLSM_stuttering_embedding_finite_trace_project
  (Hsimul : VLSM_stuttering_embedding X Y state_project transition_item_project)
  : list (transition_item X) -> list (transition_item Y)
  := pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project.

Lemma elem_of_VLSM_stuttering_embedding :
  VLSM_stuttering_embedding X Y state_project transition_item_project ->
  forall (trX : list transition_item) (itemY : transition_item),
    itemY ∈ pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project trX
      <->
    exists itemX : transition_item,
      itemY ∈ transition_item_project itemX /\ itemX ∈ trX.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
VLSM_stuttering_embedding X Y state_project
  transition_item_project
→ ∀ (trX : list transition_item) (itemY : transition_item),
    itemY
    ∈ pre_VLSM_stuttering_embedding_finite_trace_project
        transition_item_project trX
    ↔ (∃ itemX : transition_item,
         itemY ∈ transition_item_project itemX
         ∧ itemX ∈ trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
VLSM_stuttering_embedding X Y state_project
  transition_item_project
→ ∀ (trX : list transition_item) (itemY : transition_item),
    itemY
    ∈ pre_VLSM_stuttering_embedding_finite_trace_project
        transition_item_project trX
    ↔ (∃ itemX : transition_item,
         itemY ∈ transition_item_project itemX
         ∧ itemX ∈ trX)
  exact (fun _ => elem_of_pre_VLSM_stuttering_embedding_finite_trace_project
    transition_item_project).
Qed.

Definition VLSM_stuttering_embedding_infinite_trace_project
  (Hsimul : VLSM_stuttering_embedding X Y state_project transition_item_project)
  (s : Streams.Stream (transition_item X))
  (Hinf : InfinitelyOften (fun item => transition_item_project item <> []) s)
  : Streams.Stream (transition_item Y)
  := pre_VLSM_stuttering_embedding_infinite_trace_project transition_item_project s Hinf.

Definition VLSM_stuttering_embedding_infinite_finite_trace_project
  (Hsimul : VLSM_stuttering_embedding X Y state_project transition_item_project)
  (s : Streams.Stream (transition_item X))
  (Hfin : FinitelyManyBound (fun item => transition_item_project item <> []) s)
  : list (transition_item Y)
  := pre_VLSM_stuttering_embedding_infinite_finite_trace_project transition_item_project s Hfin.

End sec_stuttering_embedding_trace_projection_redefinitions.

While for the above section, the VLSM_stuttering_embedding was necessary to be mentioned explicitly, in the following we make it part of the context.

Context
  (Hsimul : VLSM_stuttering_embedding X Y state_project transition_item_project).

Lemma VLSM_stuttering_embedding_finite_trace_project_app :
  forall l1 l2,
    VLSM_stuttering_embedding_finite_trace_project Hsimul (l1 ++ l2)
      =
    VLSM_stuttering_embedding_finite_trace_project Hsimul l1
      ++ VLSM_stuttering_embedding_finite_trace_project Hsimul l2.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ l1 l2 : list transition_item,
  VLSM_stuttering_embedding_finite_trace_project
    Hsimul (l1 ++ l2) =
  VLSM_stuttering_embedding_finite_trace_project
    Hsimul l1 ++
  VLSM_stuttering_embedding_finite_trace_project
    Hsimul l2
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ l1 l2 : list transition_item,
  VLSM_stuttering_embedding_finite_trace_project
    Hsimul (l1 ++ l2) =
  VLSM_stuttering_embedding_finite_trace_project
    Hsimul l1 ++
  VLSM_stuttering_embedding_finite_trace_project
    Hsimul l2
  exact (pre_VLSM_stuttering_embedding_finite_trace_project_app transition_item_project).
Qed.

Lemma VLSM_stuttering_embedding_finite_trace_last :
  forall sX trX,
    finite_valid_trace_from X sX trX ->
    finite_trace_last (state_project sX) (VLSM_stuttering_embedding_finite_trace_project Hsimul trX)
      =
    state_project (finite_trace_last sX trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_trace_last (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX) =
    state_project (finite_trace_last sX trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_trace_last (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX) =
    state_project (finite_trace_last sX trX)
  exact (pre_VLSM_stuttering_embedding_finite_trace_last _ _ _ _ Hsimul).
Qed.

Lemma VLSM_stuttering_embedding_finite_valid_trace :
  forall sX trX,
    finite_valid_trace X sX trX -> finite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
  exact (stuttering_embedding_preserves_valid_trace _ _ _ _ Hsimul).
Qed.

Any VLSM_stuttering_embedding determines a VLSM_partial_projection, allowing us to lift to stuttering embeddings the generic results proved about partial projections.

Lemma VLSM_partial_projection_from_stuttering_embedding :
  VLSM_partial_projection X Y
    (VLSM_partial_trace_project_from_stuttering_embedding state_project transition_item_project).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
  split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_stuttering_embedding
    state_project transition_item_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace X sX trX
    → finite_valid_trace Y sY trY
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_stuttering_embedding
     state_project transition_item_project) by apply VLSM_partial_projection_type_from_stuttering_embedding, Hsimul.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  VLSM_partial_trace_project_from_stuttering_embedding
    state_project transition_item_project (sX, trX) =
  Some (sY, trY)
  → finite_valid_trace X sX trX
    → finite_valid_trace Y sY trY intros sX trX sY trY [= <- <-].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: list transition_item
finite_valid_trace X sX trX
→ finite_valid_trace Y (state_project sX)
    (pre_VLSM_stuttering_embedding_finite_trace_project
       transition_item_project trX)
    by apply VLSM_stuttering_embedding_finite_valid_trace.
Qed.

Lemma VLSM_stuttering_embedding_finite_valid_trace_from :
  forall sX trX,
    finite_valid_trace_from X sX trX ->
    finite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
  by intros; eapply VLSM_partial_projection_finite_valid_trace_from;
    [apply VLSM_partial_projection_from_stuttering_embedding | ..].
Qed.

Definition VLSM_stuttering_embedding_weaken :
  VLSM_weak_stuttering_embedding X Y state_project transition_item_project :=
{|
  weak_stuttering_embedding_type := stuttering_embedding_type _ _ _ _ Hsimul;
  weak_stuttering_embedding_preserves_valid_trace :=
    VLSM_stuttering_embedding_finite_valid_trace_from;
|}.

Lemma VLSM_stuttering_embedding_valid_state :
  forall sX,
    valid_state_prop X sX -> valid_state_prop Y (state_project sX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
  exact (VLSM_weak_stuttering_embedding_valid_state VLSM_stuttering_embedding_weaken).
Qed.

Lemma VLSM_stuttering_embedding_input_valid_transition_item :
  forall s item,
    input_valid_transition_item X s item ->
    finite_valid_trace_from_to Y (state_project s) (state_project (destination item))
      (transition_item_project item).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (s : state X) (item : transition_item),
  input_valid_transition_item X s item
  → finite_valid_trace_from_to Y (state_project s)
      (state_project (destination item))
      (transition_item_project item)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (s : state X) (item : transition_item),
  input_valid_transition_item X s item
  → finite_valid_trace_from_to Y (state_project s)
      (state_project (destination item))
      (transition_item_project item)
  exact (VLSM_weak_stuttering_embedding_input_valid_transition_item
    VLSM_stuttering_embedding_weaken).
Qed.

Lemma VLSM_stuttering_embedding_finite_valid_trace_from_to :
  forall sX s'X trX,
    finite_valid_trace_from_to X sX s'X trX ->
    finite_valid_trace_from_to Y (state_project sX) (state_project s'X)
      (VLSM_stuttering_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX s'X : state X) (trX : list transition_item),
  finite_valid_trace_from_to X sX s'X trX
  → finite_valid_trace_from_to Y (state_project sX)
      (state_project s'X)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX s'X : state X) (trX : list transition_item),
  finite_valid_trace_from_to X sX s'X trX
  → finite_valid_trace_from_to Y (state_project sX)
      (state_project s'X)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
  exact (VLSM_weak_stuttering_embedding_finite_valid_trace_from_to
    VLSM_stuttering_embedding_weaken).
Qed.

Lemma VLSM_stuttering_embedding_in_futures :
  forall s1 s2,
    in_futures X s1 s2 -> in_futures Y (state_project s1) (state_project s2).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_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
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ s1 s2 : state X,
  in_futures X s1 s2
  → in_futures Y (state_project s1) (state_project s2)
  exact (VLSM_weak_stuttering_embedding_in_futures VLSM_stuttering_embedding_weaken).
Qed.

Lemma VLSM_stuttering_embedding_infinite_valid_trace_from :
  forall sX trX (Hinf : InfinitelyOften _ trX),
    infinite_valid_trace_from X sX trX ->
    infinite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_trace_project Hsimul trX Hinf).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_trace_project
         Hsimul trX Hinf)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_trace_project
         Hsimul trX Hinf)
  exact (VLSM_weak_stuttering_embedding_infinite_valid_trace_from
    VLSM_stuttering_embedding_weaken).
Qed.

Lemma VLSM_stuttering_embedding_infinite_finite_valid_trace_from :
  forall sX trX (Hfin : FinitelyManyBound _ trX),
    infinite_valid_trace_from X sX trX ->
    finite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_finite_trace_project Hsimul trX Hfin).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_finite_trace_project
         Hsimul trX Hfin)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_finite_trace_project
         Hsimul trX Hfin)
  exact (VLSM_weak_stuttering_embedding_infinite_finite_valid_trace_from
    VLSM_stuttering_embedding_weaken).
Qed.

Lemma VLSM_stuttering_embedding_initial_state :
  forall sX, initial_state_prop X sX -> initial_state_prop Y (state_project sX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ sX : state X,
  initial_state_prop sX
  → initial_state_prop (state_project sX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ sX : state X,
  initial_state_prop sX
  → initial_state_prop (state_project sX)
  by intros; eapply VLSM_partial_projection_initial_state;
    [apply VLSM_partial_projection_from_stuttering_embedding | ..].
Qed.

Lemma VLSM_stuttering_embedding_finite_valid_trace_init_to :
  forall sX s'X trX,
    finite_valid_trace_init_to X sX s'X trX ->
    finite_valid_trace_init_to Y (state_project sX) (state_project s'X)
      (VLSM_stuttering_embedding_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX s'X : state X) (trX : list transition_item),
  finite_valid_trace_init_to X sX s'X trX
  → finite_valid_trace_init_to Y (state_project sX)
      (state_project s'X)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX s'X : state X) (trX : list transition_item),
  finite_valid_trace_init_to X sX s'X trX
  → finite_valid_trace_init_to Y (state_project sX)
      (state_project s'X)
      (VLSM_stuttering_embedding_finite_trace_project
         Hsimul trX)
  intros * []; split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
H0: initial_state_prop sX
finite_valid_trace_from_to Y (state_project sX)
  (state_project s'X)
  (VLSM_stuttering_embedding_finite_trace_project
     Hsimul trX)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
H0: initial_state_prop sX
initial_state_prop (state_project sX)
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
H0: initial_state_prop sX
finite_valid_trace_from_to Y (state_project sX)
  (state_project s'X)
  (VLSM_stuttering_embedding_finite_trace_project
     Hsimul trX) by apply VLSM_stuttering_embedding_finite_valid_trace_from_to.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
H0: initial_state_prop sX
initial_state_prop (state_project sX) by apply VLSM_stuttering_embedding_initial_state.
Qed.

Lemma VLSM_stuttering_embedding_infinite_valid_trace :
  forall sX trX (Hinf : InfinitelyOften _ trX),
    infinite_valid_trace X sX trX ->
    infinite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_trace_project Hsimul trX Hinf).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace X sX trX
  → infinite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_trace_project
         Hsimul trX Hinf)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace X sX trX
  → infinite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_trace_project
         Hsimul trX Hinf)
  intros sX trX Hinf [HtrX HsX].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
infinite_valid_trace Y (state_project sX)
  (VLSM_stuttering_embedding_infinite_trace_project
     Hsimul trX Hinf)
  split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
infinite_valid_trace_from Y (state_project sX)
  (VLSM_stuttering_embedding_infinite_trace_project
     Hsimul trX Hinf)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX)
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
infinite_valid_trace_from Y (state_project sX)
  (VLSM_stuttering_embedding_infinite_trace_project
     Hsimul trX Hinf) by apply VLSM_stuttering_embedding_infinite_valid_trace_from.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX) by apply VLSM_stuttering_embedding_initial_state.
Qed.

Lemma VLSM_stuttering_embedding_infinite_finite_valid_trace :
  forall sX trX (Hfin : FinitelyManyBound _ trX),
    infinite_valid_trace X sX trX ->
    finite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_finite_trace_project Hsimul trX Hfin).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_finite_trace_project
         Hsimul trX Hfin)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (λ item : transition_item,
               transition_item_project item ≠ []) trX),
  infinite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_stuttering_embedding_infinite_finite_trace_project
         Hsimul trX Hfin)
  intros sX trX Hfin [HtrX HsX].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace Y (state_project sX)
  (VLSM_stuttering_embedding_infinite_finite_trace_project
     Hsimul trX Hfin)
  split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (VLSM_stuttering_embedding_infinite_finite_trace_project
     Hsimul trX Hfin)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX)
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (VLSM_stuttering_embedding_infinite_finite_trace_project
     Hsimul trX Hfin) by apply VLSM_stuttering_embedding_infinite_finite_valid_trace_from.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (λ item : transition_item,
     transition_item_project item ≠ []) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX) by apply VLSM_stuttering_embedding_initial_state.
Qed.

Stuttering embedding friendliness

A stuttering embedding is friendly if all the valid traces of the destination VLSM are prefixes of translations of the valid traces of the source VLSM.

Section sec_stuttering_embedding_friendliness.

We axiomatize stuttering embedding friendliness as the converse of VLSM_stuttering_embedding_finite_valid_trace. However, since a transition in the source corresponds to possibly multiple transitions in the destination, we'll ask that any valid trace in the destination is the prefix of a translation of a valid trace from the source.

Definition stuttering_embedding_friendly_prop : Prop :=
  forall
    (sY : state Y)
    (trY : list (transition_item Y))
    (HtrY : finite_valid_trace Y sY trY),
  exists (sX : state X) (trX : list (transition_item X)),
    finite_valid_trace X sX trX
    /\ state_project sX = sY
    /\ trY `prefix_of` VLSM_stuttering_embedding_finite_trace_project Hsimul trX.

Lemma stuttering_embedding_friendly_finite_valid_trace_from_to
  (Hfr : stuttering_embedding_friendly_prop)
  (sY1 sY2 : state Y) (trY : list (transition_item Y))
  (HtrY : finite_valid_trace_from_to Y sY1 sY2 trY)
  : exists (sX1 sX2 : state X) (trX : list (transition_item X))
      (preY sufY : list (transition_item Y)),
      finite_valid_trace_from_to X sX1 sX2 trX /\
      VLSM_stuttering_embedding_finite_trace_project Hsimul trX = preY ++ trY ++ sufY.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
HtrY: finite_valid_trace_from_to Y sY1 sY2 trY
∃ (sX1 sX2 : state X) (trX preY
                       sufY : list transition_item),
  finite_valid_trace_from_to X sX1 sX2 trX
  ∧ VLSM_stuttering_embedding_finite_trace_project
      Hsimul trX = preY ++ trY ++ sufY
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
HtrY: finite_valid_trace_from_to Y sY1 sY2 trY
∃ (sX1 sX2 : state X) (trX preY
                       sufY : list transition_item),
  finite_valid_trace_from_to X sX1 sX2 trX
  ∧ VLSM_stuttering_embedding_finite_trace_project
      Hsimul trX = preY ++ trY ++ sufY
  apply finite_valid_trace_from_to_complete_left in HtrY
    as (is & tr_s1 & Htr & _).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
is: state Y
tr_s1: list transition_item
Htr: finite_valid_trace_init_to Y is sY2
  (tr_s1 ++ trY)
∃ (sX1 sX2 : state X) (trX preY
                       sufY : list transition_item),
  finite_valid_trace_from_to X sX1 sX2 trX
  ∧ VLSM_stuttering_embedding_finite_trace_project
      Hsimul trX = preY ++ trY ++ sufY
  apply valid_trace_forget_last, Hfr in Htr as [isX [trX [[Htr _] [His [suf Htr_pr]]]]].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace_from X isX trX
His: state_project isX = is
suf: list transition_item
Htr_pr: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = (tr_s1 ++ trY) ++ suf
∃ (sX1 sX2 : state X) (trX preY
                       sufY : list transition_item),
  finite_valid_trace_from_to X sX1 sX2 trX
  ∧ VLSM_stuttering_embedding_finite_trace_project
      Hsimul trX = preY ++ trY ++ sufY
  exists isX, (finite_trace_last isX trX), trX, tr_s1, suf.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace_from X isX trX
His: state_project isX = is
suf: list transition_item
Htr_pr: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = (tr_s1 ++ trY) ++ suf
finite_valid_trace_from_to X isX
  (finite_trace_last isX trX) trX
∧ VLSM_stuttering_embedding_finite_trace_project
    Hsimul trX = tr_s1 ++ trY ++ suf
  split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace_from X isX trX
His: state_project isX = is
suf: list transition_item
Htr_pr: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = (tr_s1 ++ trY) ++ suf
finite_valid_trace_from_to X isX
  (finite_trace_last isX trX) trX
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace_from X isX trX
His: state_project isX = is
suf: list transition_item
Htr_pr: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = (tr_s1 ++ trY) ++ suf
VLSM_stuttering_embedding_finite_trace_project Hsimul
  trX = tr_s1 ++ trY ++ suf
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace_from X isX trX
His: state_project isX = is
suf: list transition_item
Htr_pr: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = (tr_s1 ++ trY) ++ suf
finite_valid_trace_from_to X isX
  (finite_trace_last isX trX) trX by apply valid_trace_add_default_last.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfr: stuttering_embedding_friendly_prop
sY1, sY2: state Y
trY: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace_from X isX trX
His: state_project isX = is
suf: list transition_item
Htr_pr: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = (tr_s1 ++ trY) ++ suf
VLSM_stuttering_embedding_finite_trace_project Hsimul
  trX = tr_s1 ++ trY ++ suf by rewrite app_assoc.
Qed.

A consequence of the stuttering_embedding_friendly_property is that the valid traces of the target VLSM are precisely prefixes of translations of all the valid traces of the source VLSM.

Lemma stuttering_embedding_friendly_trace_char
  (Hfriendly : stuttering_embedding_friendly_prop)
  : forall sY trY, finite_valid_trace Y sY trY <->
    exists (sX : state X) (trX : list (transition_item X)),
    finite_valid_trace X sX trX
    /\ state_project sX = sY
    /\ trY `prefix_of` VLSM_stuttering_embedding_finite_trace_project Hsimul trX.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfriendly: stuttering_embedding_friendly_prop
∀ (sY : state Y) (trY : list transition_item),
  finite_valid_trace Y sY trY
  ↔ (∃ (sX : state X) (trX : list transition_item),
       finite_valid_trace X sX trX
       ∧ state_project sX = sY
         ∧ trY
           `prefix_of` VLSM_stuttering_embedding_finite_trace_project
                         Hsimul trX)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfriendly: stuttering_embedding_friendly_prop
∀ (sY : state Y) (trY : list transition_item),
  finite_valid_trace Y sY trY
  ↔ (∃ (sX : state X) (trX : list transition_item),
       finite_valid_trace X sX trX
       ∧ state_project sX = sY
         ∧ trY
           `prefix_of` VLSM_stuttering_embedding_finite_trace_project
                         Hsimul trX)
  split; [by apply Hfriendly |].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfriendly: stuttering_embedding_friendly_prop
sY: state Y
trY: list transition_item
(∃ (sX : state X) (trX : list transition_item),
   finite_valid_trace X sX trX
   ∧ state_project sX = sY
     ∧ trY
       `prefix_of` VLSM_stuttering_embedding_finite_trace_project
                     Hsimul trX)
→ finite_valid_trace Y sY trY
  intros (sX & trX & HtrX & <- & sufY & HtrY).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfriendly: stuttering_embedding_friendly_prop
trY: list transition_item
sX: state X
trX: list transition_item
HtrX: finite_valid_trace X sX trX
sufY: list transition_item
HtrY: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = trY ++ sufY
finite_valid_trace Y (state_project sX) trY
  apply VLSM_stuttering_embedding_finite_valid_trace in HtrX as [HtrX].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfriendly: stuttering_embedding_friendly_prop
trY: list transition_item
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from Y 
  (state_project sX)
  (VLSM_stuttering_embedding_finite_trace_project
     Hsimul trX)
H: initial_state_prop (state_project sX)
sufY: list transition_item
HtrY: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = trY ++ sufY
finite_valid_trace Y (state_project sX) trY
  split; [| done].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfriendly: stuttering_embedding_friendly_prop
trY: list transition_item
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from Y 
  (state_project sX)
  (VLSM_stuttering_embedding_finite_trace_project
     Hsimul trX)
H: initial_state_prop (state_project sX)
sufY: list transition_item
HtrY: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = trY ++ sufY
finite_valid_trace_from Y (state_project sX) trY
  eapply finite_valid_trace_from_app_iff.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Hsimul: VLSM_stuttering_embedding X Y state_project
  transition_item_project
Hfriendly: stuttering_embedding_friendly_prop
trY: list transition_item
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from Y 
  (state_project sX)
  (VLSM_stuttering_embedding_finite_trace_project
     Hsimul trX)
H: initial_state_prop (state_project sX)
sufY: list transition_item
HtrY: VLSM_stuttering_embedding_finite_trace_project
  Hsimul trX = trY ++ sufY
finite_valid_trace_from Y (state_project sX)
  (trY ++ ?ls')
  by rewrite <- HtrY.
Qed.

End sec_stuttering_embedding_friendliness.

End sec_stuttering_embedding_properties.

To establish a stuttering embedding from VLSM X to VLSM Y, the following set of conditions is sufficient:

X's initial_states project to Y's initial states
Every input-valid transition translates to a valid trace from the translation of the source of the transition to the translation of the destination of the transition

Section sec_basic_VLSM_stuttering_embedding.

Section sec_strong_VLSM_stuttering_embedding_type.

Context
  {message : Type}
  (X : VLSM message)
  (TY : VLSMType message)
  (state_project : state X -> state TY)
  (transition_item_project : transition_item X -> list (transition_item TY))
  .

Lemma strong_VLSM_stuttering_embedding_type
  (Htransition : strong_transition_item_project_consistency state_project transition_item_project)
  : VLSM_stuttering_embedding_type X TY state_project transition_item_project.message: Type
X: VLSM message
TY: VLSMType message
state_project: state X → state TY
transition_item_project: transition_item
→ list transition_item
Htransition: strong_transition_item_project_consistency
  state_project transition_item_project
VLSM_stuttering_embedding_type X TY state_project
  transition_item_project
Proof.message: Type
X: VLSM message
TY: VLSMType message
state_project: state X → state TY
transition_item_project: transition_item
→ list transition_item
Htransition: strong_transition_item_project_consistency
  state_project transition_item_project
VLSM_stuttering_embedding_type X TY state_project
  transition_item_project by constructor; intros ? [] []; apply Htransition. Qed.

End sec_strong_VLSM_stuttering_embedding_type.

Context
  {message : Type}
  (X Y : VLSM message)
  (state_project : state X -> state Y)
  (transition_item_project : transition_item X -> list (transition_item Y))
  (Htransition : stuttering_embedding_input_valid_transition_item_validity
    X Y state_project transition_item_project)
  .

Lemma basic_VLSM_stuttering_embedding_type :
  VLSM_stuttering_embedding_type X Y state_project transition_item_project.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
VLSM_stuttering_embedding_type X Y state_project
  transition_item_project
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
VLSM_stuttering_embedding_type X Y state_project
  transition_item_project
  constructor; intros.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
sX: state X
itemX: transition_item
H: input_valid_transition_item X sX itemX
finite_trace_last (state_project sX)
  (transition_item_project itemX) =
state_project (destination itemX)
  by eapply finite_valid_trace_from_to_last, Htransition.
Qed.

Section sec_weak_stuttering_embedding.

Context
  (Hstate : weak_stuttering_embedding_initial_state_preservation X Y state_project)
  .

#[local] Lemma basic_VLSM_stuttering_embedding_finite_valid_trace_init_to
  is s tr
  (Htr : finite_valid_trace_init_to X is s tr)
  : finite_valid_trace_from_to Y (state_project is) (state_project s)
      (pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project tr).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
is, s: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X is s tr
finite_valid_trace_from_to Y (state_project is)
  (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
is, s: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X is s tr
finite_valid_trace_from_to Y (state_project is)
  (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr)
  induction Htr using finite_valid_trace_init_to_rev_ind; [by constructor; apply Hstate |].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: finite_valid_trace_from_to Y
  (state_project si) (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr)
finite_valid_trace_from_to Y (state_project si)
  (state_project sf)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project
     (tr ++
      [{|
         l := l;
         input := iom;
         destination := sf;
         output := oom
       |}]))
  rewrite pre_VLSM_stuttering_embedding_finite_trace_project_app.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: finite_valid_trace_from_to Y
  (state_project si) (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr)
finite_valid_trace_from_to Y (state_project si)
  (state_project sf)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr ++
   pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project
     [{|
        l := l;
        input := iom;
        destination := sf;
        output := oom
      |}])
  apply finite_valid_trace_from_to_app with (state_project s); [done |].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: finite_valid_trace_from_to Y
  (state_project si) (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr)
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project
     [{|
        l := l;
        input := iom;
        destination := sf;
        output := oom
      |}])
  cbn; rewrite app_nil_r.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: finite_valid_trace_from_to Y
  (state_project si) (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr)
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  (transition_item_project
     {|
       l := l;
       input := iom;
       destination := sf;
       output := oom
     |})
  remember {| l := _ |} as itemX; replace sf with (destination itemX) by (subst; done).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: finite_valid_trace_from_to Y
  (state_project si) (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr)
itemX: transition_item
HeqitemX: itemX =
{|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}
finite_valid_trace_from_to Y (state_project s)
  (state_project (destination itemX))
  (transition_item_project itemX)
  by apply Htransition; subst.
Qed.

#[local] Lemma basic_VLSM_stuttering_embedding_finite_valid_trace_from
  (s : state X)
  (ls : list transition_item)
  (Hpxt : finite_valid_trace_from X s ls)
  : finite_valid_trace_from Y (state_project s)
      (pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project ls).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from X s ls
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project ls)
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from X s ls
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project ls)
  apply valid_trace_add_default_last,
    finite_valid_trace_from_to_complete_left
    in Hpxt as (is_s & tr_s & Htr & Heqs).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project ls)
  replace (state_project s) with
    (finite_trace_last (state_project is_s)
      (pre_VLSM_stuttering_embedding_finite_trace_project transition_item_project tr_s)).message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from Y
  (finite_trace_last (state_project is_s)
     (pre_VLSM_stuttering_embedding_finite_trace_project
        transition_item_project tr_s))
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project ls)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Heqs: finite_trace_last is_s tr_s = s
finite_trace_last (state_project is_s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr_s) = 
state_project s
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from Y
  (finite_trace_last (state_project is_s)
     (pre_VLSM_stuttering_embedding_finite_trace_project
        transition_item_project tr_s))
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project ls) eapply valid_trace_forget_last, finite_valid_trace_from_to_app_split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from_to Y (state_project is_s) 
  ?f
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr_s ++
   pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project ls)
    rewrite <- pre_VLSM_stuttering_embedding_finite_trace_project_app.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from_to Y (state_project is_s) 
  ?f
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project (tr_s ++ ls))
    by apply basic_VLSM_stuttering_embedding_finite_valid_trace_init_to.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
s: state X
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Heqs: finite_trace_last is_s tr_s = s
finite_trace_last (state_project is_s)
  (pre_VLSM_stuttering_embedding_finite_trace_project
     transition_item_project tr_s) = state_project s subst s; apply pre_VLSM_stuttering_embedding_finite_trace_last.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last
     (finite_trace_last is_s tr_s) ls)
  (tr_s ++ ls)
VLSM_stuttering_embedding_type X Y state_project
  transition_item_project
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last
     (finite_trace_last is_s tr_s) ls)
  (tr_s ++ ls)
finite_valid_trace_from X is_s tr_s
    +message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last
     (finite_trace_last is_s tr_s) ls)
  (tr_s ++ ls)
VLSM_stuttering_embedding_type X Y state_project
  transition_item_project by apply basic_VLSM_stuttering_embedding_type.
    +message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
ls: list transition_item
is_s: state X
tr_s: list transition_item
Htr: finite_valid_trace_init_to X is_s
  (finite_trace_last
     (finite_trace_last is_s tr_s) ls)
  (tr_s ++ ls)
finite_valid_trace_from X is_s tr_s by eapply valid_trace_forget_last, finite_valid_trace_from_to_app_split, Htr.
Qed.

Lemma basic_VLSM_weak_stuttering_embedding :
  VLSM_weak_stuttering_embedding X Y state_project transition_item_project.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_weak_stuttering_embedding X Y state_project
  transition_item_project
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_weak_stuttering_embedding X Y state_project
  transition_item_project
  constructor.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_stuttering_embedding_type X Y state_project
  transition_item_project
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y 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_stuttering_embedding_finite_trace_project
         transition_item_project trX)
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_stuttering_embedding_type X Y state_project
  transition_item_project by apply basic_VLSM_stuttering_embedding_type.
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: weak_stuttering_embedding_initial_state_preservation
  X Y 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_stuttering_embedding_finite_trace_project
         transition_item_project trX) by apply basic_VLSM_stuttering_embedding_finite_valid_trace_from.
Qed.

End sec_weak_stuttering_embedding.

Lemma basic_VLSM_weak_stuttering_embedding_strengthen
  (Hweak : VLSM_weak_stuttering_embedding X Y state_project transition_item_project)
  (Hstate : strong_stuttering_embedding_initial_state_preservation X Y state_project)
  : VLSM_stuttering_embedding X Y state_project transition_item_project.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_stuttering_embedding X Y state_project
  transition_item_project
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_stuttering_embedding X Y state_project
  transition_item_project
  constructor; [by apply Hweak |].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_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_stuttering_embedding_finite_trace_project
         transition_item_project trX)
  intros sX trX [HtrX HsX].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_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_stuttering_embedding_finite_trace_project
     transition_item_project trX)
  split.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_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_stuttering_embedding_finite_trace_project
     transition_item_project trX)
message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_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
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_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_stuttering_embedding_finite_trace_project
     transition_item_project trX) by apply (VLSM_weak_stuttering_embedding_finite_valid_trace_from Hweak).
  -message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hweak: VLSM_weak_stuttering_embedding X Y
  state_project transition_item_project
Hstate: strong_stuttering_embedding_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_stuttering_embedding
  (Hstate : strong_stuttering_embedding_initial_state_preservation X Y state_project)
  : VLSM_stuttering_embedding X Y state_project transition_item_project.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: strong_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_stuttering_embedding X Y state_project
  transition_item_project
Proof.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: strong_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_stuttering_embedding X Y state_project
  transition_item_project
  apply basic_VLSM_weak_stuttering_embedding_strengthen; [| done].message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: strong_stuttering_embedding_initial_state_preservation
  X Y state_project
VLSM_weak_stuttering_embedding X Y state_project
  transition_item_project
  apply basic_VLSM_weak_stuttering_embedding.message: Type
X, Y: VLSM message
state_project: state X → state Y
transition_item_project: transition_item
→ list transition_item
Htransition: stuttering_embedding_input_valid_transition_item_validity
  X Y state_project
  transition_item_project
Hstate: strong_stuttering_embedding_initial_state_preservation
  X Y state_project
weak_stuttering_embedding_initial_state_preservation X
  Y state_project
  by apply strong_stuttering_embedding_initial_state_preservation_weaken.
Qed.

End sec_basic_VLSM_stuttering_embedding.