From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.
From VLSM.Lib Require Import Preamble ListExtras StreamExtras StreamFilters StdppExtras.
From VLSM.Core Require Import VLSM VLSMProjections.VLSMPartialProjection.

Core: VLSM Total Projections

A VLSM projection guaranteeing the existence of projection for all states and traces. We say that VLSM X projects to VLSM Y (sharing the same messages) if there exists maps state_project taking X-states to Y-states, and trace_project, taking list of transitions from X to Y, such that:

state and trace_project_preserves_valid_traces
trace_project_app: trace projection commutes with concatenation of traces
final_state_project: state projection commutes with finite_trace_last

Proper examples of total projections (which are not VLSM_embeddings) are projections in which some of transitions might be dropped, such as the projection of a composition to one of the components (component_projection) or the projection of the compositions of equivocators to the composition of regular components using the particular MachineDescriptor which select the first (original) component instance for each equivocator (e.g., equivocators_no_equivocations_vlsm_X_vlsm_projection).

Section sec_VLSM_projection.

Section sec_pre_definitions.

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

Definition pre_VLSM_projection_in_projection
  (item : transition_item TX)
  : Prop :=
  is_Some (label_project (l item)).

Definition pre_VLSM_projection_transition_item_project
  (item : transition_item TX)
  : option (transition_item TY)
  :=
  match label_project (l item) with
  | None => None
  | Some lY =>
    Some {| l := lY; input := input item; destination := state_project (destination item);
            output := output item |}
  end.

Lemma pre_VLSM_projection_transition_item_project_is_Some
  (item : transition_item TX)
  : pre_VLSM_projection_in_projection item ->
    is_Some (pre_VLSM_projection_transition_item_project item).message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item: transition_item
pre_VLSM_projection_in_projection item
→ is_Some
    (pre_VLSM_projection_transition_item_project item)
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item: transition_item
pre_VLSM_projection_in_projection item
→ is_Some
    (pre_VLSM_projection_transition_item_project item)
  intros [lY HlY].message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item: transition_item
lY: label TY
HlY: label_project (l item) = Some lY
is_Some
  (pre_VLSM_projection_transition_item_project item)
  unfold pre_VLSM_projection_transition_item_project.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item: transition_item
lY: label TY
HlY: label_project (l item) = Some lY
is_Some
  match label_project (l item) with
  | Some lY =>
      Some
        {|
          l := lY;
          input := input item;
          destination :=
            state_project (destination item);
          output := output item
        |}
  | None => None
  end
  rewrite HlY.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item: transition_item
lY: label TY
HlY: label_project (l item) = Some lY
is_Some
  (Some
     {|
       l := lY;
       input := input item;
       destination := state_project (destination item);
       output := output item
     |})
  by eexists.
Qed.

Lemma pre_VLSM_projection_transition_item_project_is_Some_rev
  (item : transition_item TX)
  : is_Some (pre_VLSM_projection_transition_item_project item) ->
    pre_VLSM_projection_in_projection item.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item: transition_item
is_Some
  (pre_VLSM_projection_transition_item_project item)
→ pre_VLSM_projection_in_projection item
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item: transition_item
is_Some
  (pre_VLSM_projection_transition_item_project item)
→ pre_VLSM_projection_in_projection item
  intros [itemY HitemY].message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item, itemY: transition_item
HitemY: pre_VLSM_projection_transition_item_project
  item = Some itemY
pre_VLSM_projection_in_projection item
  unfold pre_VLSM_projection_transition_item_project in HitemY.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item, itemY: transition_item
HitemY: match label_project (l item) with
| Some lY =>
    Some
      {|
        l := lY;
        input := input item;
        destination :=
          state_project (destination item);
        output := output item
      |}
| None => None
end = Some itemY
pre_VLSM_projection_in_projection item
  destruct (label_project (l item)) as [lY |] eqn: HlY; [| by congruence].message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
item, itemY: transition_item
lY: label TY
HlY: label_project (l item) = Some lY
HitemY: Some
  {|
    l := lY;
    input := input item;
    destination :=
      state_project (destination item);
    output := output item
  |} = Some itemY
pre_VLSM_projection_in_projection item
  by exists lY.
Qed.

Lemma pre_VLSM_projection_transition_item_project_infinitely_often
  (s : Streams.Stream (transition_item TX))
  : InfinitelyOften pre_VLSM_projection_in_projection s ->
    InfinitelyOften (is_Some ∘ pre_VLSM_projection_transition_item_project) s.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
InfinitelyOften pre_VLSM_projection_in_projection s
→ InfinitelyOften
    (is_Some
     ∘ pre_VLSM_projection_transition_item_project) s
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
InfinitelyOften pre_VLSM_projection_in_projection s
→ InfinitelyOften
    (is_Some
     ∘ pre_VLSM_projection_transition_item_project) s
  apply InfinitelyOften_impl.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
∀ a : transition_item,
  pre_VLSM_projection_in_projection a
  → (is_Some
     ∘ pre_VLSM_projection_transition_item_project) a
  intro item.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
item: transition_item
pre_VLSM_projection_in_projection item
→ (is_Some
   ∘ pre_VLSM_projection_transition_item_project) item
  by apply pre_VLSM_projection_transition_item_project_is_Some.
Qed.

Lemma pre_VLSM_projection_transition_item_project_finitely_many
  (s : Streams.Stream (transition_item TX))
  : FinitelyManyBound pre_VLSM_projection_in_projection s ->
    FinitelyManyBound (is_Some ∘ pre_VLSM_projection_transition_item_project) s.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
FinitelyManyBound pre_VLSM_projection_in_projection s
→ FinitelyManyBound
    (is_Some
     ∘ pre_VLSM_projection_transition_item_project) s
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
FinitelyManyBound pre_VLSM_projection_in_projection s
→ FinitelyManyBound
    (is_Some
     ∘ pre_VLSM_projection_transition_item_project) s
  apply FinitelyManyBound_impl_rev.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
∀ a : transition_item,
  (is_Some
   ∘ pre_VLSM_projection_transition_item_project) a
  → pre_VLSM_projection_in_projection a
  intro item.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
s: Streams.Stream transition_item
item: transition_item
(is_Some ∘ pre_VLSM_projection_transition_item_project)
  item → pre_VLSM_projection_in_projection item
  by apply pre_VLSM_projection_transition_item_project_is_Some_rev.
Qed.

Definition pre_VLSM_projection_finite_trace_project
  : list (transition_item TX) -> list (transition_item TY)
  :=
  omap pre_VLSM_projection_transition_item_project.

Definition pre_VLSM_projection_infinite_trace_project
  (s : Streams.Stream (transition_item TX))
  (Hs : InfinitelyOften  pre_VLSM_projection_in_projection s)
  : Streams.Stream (transition_item TY) :=
  stream_map_option pre_VLSM_projection_transition_item_project s
    (pre_VLSM_projection_transition_item_project_infinitely_often _ Hs).

Definition pre_VLSM_projection_infinite_finite_trace_project
  (s : Streams.Stream (transition_item TX))
  (Hs : FinitelyManyBound pre_VLSM_projection_in_projection s)
  : list (transition_item TY) :=
  pre_VLSM_projection_finite_trace_project (stream_prefix s (proj1_sig Hs)).

Lemma pre_VLSM_projection_finite_trace_project_app :
  forall l1 l2, pre_VLSM_projection_finite_trace_project (l1 ++ l2) =
    pre_VLSM_projection_finite_trace_project l1 ++ pre_VLSM_projection_finite_trace_project l2.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ l1 l2 : list transition_item,
  pre_VLSM_projection_finite_trace_project (l1 ++ l2) =
  pre_VLSM_projection_finite_trace_project l1 ++
  pre_VLSM_projection_finite_trace_project l2
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ l1 l2 : list transition_item,
  pre_VLSM_projection_finite_trace_project (l1 ++ l2) =
  pre_VLSM_projection_finite_trace_project l1 ++
  pre_VLSM_projection_finite_trace_project l2
  exact (omap_app _).
Qed.

Lemma pre_VLSM_projection_finite_trace_project_app_rev :
  forall l l1' l2', pre_VLSM_projection_finite_trace_project l = l1' ++ l2' ->
    exists l1 l2, l = l1 ++ l2 /\
      pre_VLSM_projection_finite_trace_project l1 = l1' /\
      pre_VLSM_projection_finite_trace_project l2 = l2'.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ l l1' l2' : list transition_item,
  pre_VLSM_projection_finite_trace_project l =
  l1' ++ l2'
  → ∃ l1 l2 : list transition_item,
      l = l1 ++ l2
      ∧ pre_VLSM_projection_finite_trace_project l1 =
        l1'
        ∧ pre_VLSM_projection_finite_trace_project l2 =
          l2'
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ l l1' l2' : list transition_item,
  pre_VLSM_projection_finite_trace_project l =
  l1' ++ l2'
  → ∃ l1 l2 : list transition_item,
      l = l1 ++ l2
      ∧ pre_VLSM_projection_finite_trace_project l1 =
        l1'
        ∧ pre_VLSM_projection_finite_trace_project l2 =
          l2'
  exact (omap_app_rev _).
Qed.

Lemma pre_VLSM_projection_finite_trace_project_elem_of_iff :
  forall trX itemY, itemY ∈ pre_VLSM_projection_finite_trace_project trX <->
    exists itemX, itemX ∈ trX /\ pre_VLSM_projection_transition_item_project itemX = Some itemY.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ (trX : list transition_item) (itemY : transition_item),
  itemY ∈ pre_VLSM_projection_finite_trace_project trX
  ↔ (∃ itemX : transition_item,
       itemX ∈ trX
       ∧ pre_VLSM_projection_transition_item_project
           itemX = Some itemY)
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ (trX : list transition_item) (itemY : transition_item),
  itemY ∈ pre_VLSM_projection_finite_trace_project trX
  ↔ (∃ itemX : transition_item,
       itemX ∈ trX
       ∧ pre_VLSM_projection_transition_item_project
           itemX = Some itemY)
  exact (elem_of_list_omap _).
Qed.

Lemma elem_of_pre_VLSM_projection_finite_trace_project :
  forall trX itemY, itemY ∈ pre_VLSM_projection_finite_trace_project trX <->
    exists itemX, itemX ∈ trX /\ pre_VLSM_projection_transition_item_project itemX = Some itemY.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ (trX : list transition_item) (itemY : transition_item),
  itemY ∈ pre_VLSM_projection_finite_trace_project trX
  ↔ (∃ itemX : transition_item,
       itemX ∈ trX
       ∧ pre_VLSM_projection_transition_item_project
           itemX = Some itemY)
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ (trX : list transition_item) (itemY : transition_item),
  itemY ∈ pre_VLSM_projection_finite_trace_project trX
  ↔ (∃ itemX : transition_item,
       itemX ∈ trX
       ∧ pre_VLSM_projection_transition_item_project
           itemX = Some itemY)
  exact (elem_of_list_omap _).
Qed.

Lemma pre_VLSM_projection_finite_trace_project_elem_of :
  forall itemX itemY,
    pre_VLSM_projection_transition_item_project itemX = Some itemY ->
  forall trX,
    itemX ∈ trX -> itemY ∈ pre_VLSM_projection_finite_trace_project trX.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ itemX itemY : transition_item,
  pre_VLSM_projection_transition_item_project itemX =
  Some itemY
  → ∀ trX : list transition_item,
      itemX ∈ trX
      → itemY
        ∈ pre_VLSM_projection_finite_trace_project trX
Proof.message: Type
TX, TY: VLSMType message
label_project: label TX → option (label TY)
state_project: state TX → state TY
∀ itemX itemY : transition_item,
  pre_VLSM_projection_transition_item_project itemX =
  Some itemY
  → ∀ trX : list transition_item,
      itemX ∈ trX
      → itemY
        ∈ pre_VLSM_projection_finite_trace_project trX
  by intros; apply elem_of_list_omap; exists itemX.
Qed.

End sec_pre_definitions.

Record VLSM_projection_type
  {message : Type}
  (X : VLSM message)
  (TY : VLSMType message)
  (label_project : label X -> option (label TY))
  (state_project : state X -> state TY)
  (trace_project := pre_VLSM_projection_finite_trace_project X TY label_project state_project)
  : Prop :=
{
  final_state_project :
    forall sX trX,
      finite_valid_trace_from X sX trX ->
        state_project (finite_trace_last sX trX) =
        finite_trace_last (state_project sX) (trace_project trX);
}.

Projection definitions and properties

Section sec_projection_type_properties.

Definition VLSM_partial_trace_project_from_projection
  {message : Type}
  {X : VLSM message}
  {TY : VLSMType message}
  (label_project : label X -> option (label TY))
  (state_project : state X -> state TY)
  (trace_project := pre_VLSM_projection_finite_trace_project _ _ label_project state_project)
  := fun str : state X * list (transition_item X) =>
      let (s, tr) := str in Some (state_project s, trace_project tr).

Context
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (trace_project := pre_VLSM_projection_finite_trace_project _ _ label_project state_project)
  (Hsimul : VLSM_projection_type X Y label_project state_project)
  .

Any VLSM_projection_type determines a VLSM_partial_projection_type, allowing us to lift to VLSM projection the generic results proved about VLSM partial projections.

Lemma VLSM_partial_projection_type_from_projection :
  VLSM_partial_projection_type X Y
    (VLSM_partial_trace_project_from_projection label_project state_project).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
  split; intros; inversion H; subst; clear H.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
∃ (s'Y : state Y) (preY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (s'X, preX ++ trX) =
  Some
    (s'Y,
     preY ++
     pre_VLSM_projection_finite_trace_project X Y
       label_project state_project trX)
  ∧ finite_trace_last s'Y preY =
    state_project (finite_trace_last s'X preX)
  exists (state_project s'X), (trace_project preX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
VLSM_partial_trace_project_from_projection
  label_project state_project (s'X, preX ++ trX) =
Some
  (state_project s'X,
   trace_project preX ++
   pre_VLSM_projection_finite_trace_project X Y
     label_project state_project trX)
∧ finite_trace_last (state_project s'X)
    (trace_project preX) =
  state_project (finite_trace_last s'X preX)  split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
VLSM_partial_trace_project_from_projection
  label_project state_project (s'X, preX ++ trX) =
Some
  (state_project s'X,
   trace_project preX ++
   pre_VLSM_projection_finite_trace_project X Y
     label_project state_project trX)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
finite_trace_last (state_project s'X)
  (trace_project preX) =
state_project (finite_trace_last s'X preX)
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
VLSM_partial_trace_project_from_projection
  label_project state_project (s'X, preX ++ trX) =
Some
  (state_project s'X,
   trace_project preX ++
   pre_VLSM_projection_finite_trace_project X Y
     label_project state_project trX) by cbn; rewrite pre_VLSM_projection_finite_trace_project_app.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
finite_trace_last (state_project s'X)
  (trace_project preX) =
state_project (finite_trace_last s'X preX) symmetry.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
state_project (finite_trace_last s'X preX) =
finite_trace_last (state_project s'X)
  (trace_project preX) apply (final_state_project _ _ _ _ Hsimul).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hsimul: VLSM_projection_type X Y label_project
  state_project
trX: list transition_item
s'X: state X
preX: list transition_item
H1: finite_valid_trace_from X s'X (preX ++ trX)
finite_valid_trace_from X s'X preX
    by apply (finite_valid_trace_from_app_iff  X) in H1; apply H1.
Qed.

End sec_projection_type_properties.

Section sec_projection_transition_consistency_None.

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

When a label cannot be projected, and thus the transition will not be preserved by the projection, the state projections of the states between and after the transition must coincide.

Definition weak_projection_transition_consistency_None : Prop :=
  forall lX, label_project lX = None ->
  forall s om s' om', input_valid_transition X lX (s, om) (s', om') ->
      state_project s' = state_project s.

Definition strong_projection_transition_consistency_None : Prop :=
  forall lX, label_project lX = None ->
  forall s om s' om', transition X lX (s, om) = (s', om') ->
    state_project s' = state_project s.

Lemma strong_projection_transition_consistency_None_weaken
  : strong_projection_transition_consistency_None ->
    weak_projection_transition_consistency_None.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
strong_projection_transition_consistency_None
→ weak_projection_transition_consistency_None
Proof.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
strong_projection_transition_consistency_None
→ weak_projection_transition_consistency_None
  intros Hstrong lX Hl s om s' om' Ht.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Hstrong: strong_projection_transition_consistency_None
lX: label X
Hl: label_project lX = None
s: state X
om: option message
s': state X
om': option message
Ht: input_valid_transition X lX (s, om) (s', om')
state_project s' = state_project s
  by apply (Hstrong lX Hl _ _ _ _ (proj2 Ht)).
Qed.

End sec_projection_transition_consistency_None.

Section sec_VLSM_projection_definitions.

Context
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> option (label Y))
  (state_project : state X -> state Y)
  (trace_project := pre_VLSM_projection_finite_trace_project _ _ label_project state_project)
  .

Similarly to the VLSM_partial_projection case we distinguish two types of projections: VLSM_weak_projection and VLSM_projection, distinguished by the fact that the weak projections are not required to preserve initial states.

Although we don't have proper examples of VLSM_weak_projections, they are a support base for VLSM_weak_embeddings for which we have proper examples.

Record VLSM_weak_projection : Prop :=
{
  weak_projection_type :> VLSM_projection_type X Y label_project state_project;
  weak_trace_project_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_projection : Prop :=
{
  projection_type :> VLSM_projection_type X Y label_project state_project;
  trace_project_preserves_valid_trace :
    forall sX trX,
      finite_valid_trace X sX trX -> finite_valid_trace Y (state_project sX) (trace_project trX);
}.

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

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

Lemma strong_projection_initial_state_preservation_weaken
  : strong_projection_initial_state_preservation ->
    weak_projection_initial_state_preservation.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_initial_state_preservation
→ weak_projection_initial_state_preservation
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_initial_state_preservation
→ weak_projection_initial_state_preservation
  intros Hstrong s Hs.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hstrong: strong_projection_initial_state_preservation
s: state X
Hs: initial_state_prop s
valid_state_prop Y (state_project s) apply Hstrong in Hs.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hstrong: strong_projection_initial_state_preservation
s: state X
Hs: initial_state_prop (state_project s)
valid_state_prop Y (state_project s)
  by apply initial_state_is_valid.
Qed.

Definition weak_projection_valid_preservation : Prop :=
  forall lX lY (HlX : label_project lX = Some lY),
  forall s om
    (Hv : input_valid X lX (s, om))
    (HsY : valid_state_prop Y (state_project s))
    (HomY : option_valid_message_prop Y om),
    valid Y lY ((state_project s), om).

Definition strong_projection_valid_preservation : Prop :=
  forall lX lY, label_project lX = Some lY ->
  forall s om,
  valid X lX (s, om) -> valid Y lY ((state_project s), om).

Lemma strong_projection_valid_preservation_weaken
  : strong_projection_valid_preservation ->
    weak_projection_valid_preservation.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_valid_preservation
→ weak_projection_valid_preservation
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_valid_preservation
→ weak_projection_valid_preservation
  intros Hstrong lX lY Hl s om Hpv Hs Hom.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hstrong: strong_projection_valid_preservation
lX: label X
lY: label Y
Hl: label_project lX = Some lY
s: state X
om: option message
Hpv: input_valid X lX (s, om)
Hs: valid_state_prop Y (state_project s)
Hom: option_valid_message_prop Y om
valid lY (state_project s, om)
  by apply (Hstrong lX lY Hl), Hpv.
Qed.

Definition weak_projection_transition_preservation_Some : Prop :=
  forall lX lY, label_project lX = Some lY ->
  forall s om s' om', input_valid_transition X lX (s, om) (s', om') ->
    transition Y lY (state_project s, om) = (state_project s', om').

Definition strong_projection_transition_preservation_Some : Prop :=
  forall lX lY, label_project lX = Some lY ->
  forall s om s' om', transition X lX (s, om) = (s', om') ->
    transition Y lY (state_project s, om) = (state_project s', om').

Lemma strong_projection_transition_preservation_Some_weaken
  : strong_projection_transition_preservation_Some ->
    weak_projection_transition_preservation_Some.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_transition_preservation_Some
→ weak_projection_transition_preservation_Some
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_transition_preservation_Some
→ weak_projection_transition_preservation_Some
  intros Hstrong lX lY Hl s om s' om' Ht.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
Hstrong: strong_projection_transition_preservation_Some
lX: label X
lY: label Y
Hl: label_project lX = Some lY
s: state X
om: option message
s': state X
om': option message
Ht: input_valid_transition X lX (s, om) (s', om')
transition lY (state_project s, om) =
(state_project s', om')
  by apply (Hstrong lX lY Hl), Ht.
Qed.

Definition weak_projection_valid_message_preservation : Prop :=
  forall lX lY (HlX : label_project lX = Some lY),
  forall s m
    (Hv : input_valid X lX (s, Some m))
    (HsY : valid_state_prop Y (state_project s)),
    valid_message_prop Y m.

Definition strong_projection_valid_message_preservation : Prop :=
  forall m : message,
    valid_message_prop X m -> valid_message_prop Y m.

Lemma strong_projection_valid_message_preservation_weaken
  : strong_projection_valid_message_preservation ->
    weak_projection_valid_message_preservation.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_valid_message_preservation
→ weak_projection_valid_message_preservation
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
trace_project:= pre_VLSM_projection_finite_trace_project
  X Y label_project state_project: list transition_item
→ list transition_item
strong_projection_valid_message_preservation
→ weak_projection_valid_message_preservation
  by intros Hstrong lX lY Hl  s m [_ [Hm%Hstrong _]] HsY.
Qed.

End sec_VLSM_projection_definitions.

Section sec_weak_projection_properties.

Definition VLSM_weak_projection_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_weak_projection X Y label_project state_project)
  : list (transition_item X) -> list (transition_item Y)
  := pre_VLSM_projection_finite_trace_project _ _ label_project state_project.

Definition VLSM_weak_projection_in
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_weak_projection X Y label_project state_project)
  := pre_VLSM_projection_in_projection _ _ label_project.

Definition VLSM_weak_projection_infinite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_weak_projection X Y label_project state_project)
  (s : Streams.Stream (transition_item X))
  (Hinf : InfinitelyOften (VLSM_weak_projection_in Hsimul) s)
  : Streams.Stream (transition_item Y)
  := pre_VLSM_projection_infinite_trace_project _ _ label_project state_project s Hinf.

Definition VLSM_weak_projection_infinite_finite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_weak_projection X Y label_project state_project)
  (s : Streams.Stream (transition_item X))
  (Hfin : FinitelyManyBound (VLSM_weak_projection_in Hsimul) s)
  : list (transition_item Y)
  := pre_VLSM_projection_infinite_finite_trace_project _ _ label_project state_project s Hfin.

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

Lemma VLSM_weak_projection_trace_project_app :
  forall l1 l2,
    VLSM_weak_projection_trace_project Hsimul (l1 ++ l2) =
    VLSM_weak_projection_trace_project Hsimul l1 ++ VLSM_weak_projection_trace_project Hsimul l2.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ l1 l2 : list transition_item,
  VLSM_weak_projection_trace_project Hsimul (l1 ++ l2) =
  VLSM_weak_projection_trace_project Hsimul l1 ++
  VLSM_weak_projection_trace_project Hsimul l2
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ l1 l2 : list transition_item,
  VLSM_weak_projection_trace_project Hsimul (l1 ++ l2) =
  VLSM_weak_projection_trace_project Hsimul l1 ++
  VLSM_weak_projection_trace_project Hsimul l2
  exact (pre_VLSM_projection_finite_trace_project_app _ _ label_project state_project).
Qed.

Lemma VLSM_weak_projection_trace_project_app_rev :
  forall l l1' l2', VLSM_weak_projection_trace_project Hsimul l = l1' ++ l2' ->
    exists l1 l2, l = l1 ++ l2 /\
      VLSM_weak_projection_trace_project Hsimul l1 = l1' /\
      VLSM_weak_projection_trace_project Hsimul l2 = l2'.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ l l1' l2' : list transition_item,
  VLSM_weak_projection_trace_project Hsimul l =
  l1' ++ l2'
  → ∃ l1 l2 : list transition_item,
      l = l1 ++ l2
      ∧ VLSM_weak_projection_trace_project Hsimul l1 =
        l1'
        ∧ VLSM_weak_projection_trace_project Hsimul l2 =
          l2'
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ l l1' l2' : list transition_item,
  VLSM_weak_projection_trace_project Hsimul l =
  l1' ++ l2'
  → ∃ l1 l2 : list transition_item,
      l = l1 ++ l2
      ∧ VLSM_weak_projection_trace_project Hsimul l1 =
        l1'
        ∧ VLSM_weak_projection_trace_project Hsimul l2 =
          l2'
  exact (pre_VLSM_projection_finite_trace_project_app_rev _ _ label_project state_project).
Qed.

Lemma VLSM_weak_projection_finite_trace_last :
  forall sX trX,
    finite_valid_trace_from X sX trX ->
      state_project (finite_trace_last sX trX) =
      finite_trace_last (state_project sX) (VLSM_weak_projection_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → state_project (finite_trace_last sX trX) =
    finite_trace_last (state_project sX)
      (VLSM_weak_projection_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → state_project (finite_trace_last sX trX) =
    finite_trace_last (state_project sX)
      (VLSM_weak_projection_trace_project Hsimul trX)
  exact (final_state_project _ _ _ _ Hsimul).
Qed.

Lemma VLSM_weak_projection_finite_valid_trace_from :
  forall sX trX,
    finite_valid_trace_from X sX trX ->
      finite_valid_trace_from Y (state_project sX) (VLSM_weak_projection_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_trace_project Hsimul trX)
  exact (weak_trace_project_preserves_valid_trace _ _ _ _ Hsimul).
Qed.

Lemma VLSM_weak_projection_infinite_valid_trace_from
  : forall sX trX (Hinf : InfinitelyOften (VLSM_weak_projection_in Hsimul) trX),
    infinite_valid_trace_from X sX trX ->
    infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_infinite_trace_project Hsimul trX Hinf).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (VLSM_weak_projection_in Hsimul) trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_infinite_trace_project
         Hsimul trX Hinf)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften
            (VLSM_weak_projection_in Hsimul) trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_infinite_trace_project
         Hsimul trX Hinf)
  intros sX trX Hinf HtrX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (VLSM_weak_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
infinite_valid_trace_from Y (state_project sX)
  (VLSM_weak_projection_infinite_trace_project Hsimul
     trX Hinf)
  apply infinite_valid_trace_from_prefix_rev.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (VLSM_weak_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
∀ n : nat,
  finite_valid_trace_from Y (state_project sX)
    (stream_prefix
       (VLSM_weak_projection_infinite_trace_project
          Hsimul trX Hinf) n)
  intros n.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (VLSM_weak_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
n: nat
finite_valid_trace_from Y (state_project sX)
  (stream_prefix
     (VLSM_weak_projection_infinite_trace_project
        Hsimul trX Hinf) n)
  specialize
    (stream_map_option_prefix_ex (pre_VLSM_projection_transition_item_project _ _
      label_project state_project) trX
    (pre_VLSM_projection_transition_item_project_infinitely_often _ _
      label_project state_project trX Hinf)
    n)
    as [m Hrew].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (VLSM_weak_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
n, m: nat
Hrew: stream_prefix
  (stream_map_option
     (pre_VLSM_projection_transition_item_project
        X Y label_project state_project) trX
     (pre_VLSM_projection_transition_item_project_infinitely_often
        X Y label_project state_project trX
        Hinf)) n =
omap
  (pre_VLSM_projection_transition_item_project
     X Y label_project state_project)
  (stream_prefix trX m)
finite_valid_trace_from Y (state_project sX)
  (stream_prefix
     (VLSM_weak_projection_infinite_trace_project
        Hsimul trX Hinf) n)
  unfold VLSM_weak_projection_infinite_trace_project, pre_VLSM_projection_infinite_trace_project.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (VLSM_weak_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
n, m: nat
Hrew: stream_prefix
  (stream_map_option
     (pre_VLSM_projection_transition_item_project
        X Y label_project state_project) trX
     (pre_VLSM_projection_transition_item_project_infinitely_often
        X Y label_project state_project trX
        Hinf)) n =
omap
  (pre_VLSM_projection_transition_item_project
     X Y label_project state_project)
  (stream_prefix trX m)
finite_valid_trace_from Y (state_project sX)
  (stream_prefix
     (stream_map_option
        (pre_VLSM_projection_transition_item_project X
           Y label_project state_project) trX
        (pre_VLSM_projection_transition_item_project_infinitely_often
           X Y label_project state_project trX Hinf))
     n)
  replace (stream_prefix _ _) with (VLSM_weak_projection_trace_project Hsimul (stream_prefix trX m)).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften
  (VLSM_weak_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
n, m: nat
Hrew: stream_prefix
  (stream_map_option
     (pre_VLSM_projection_transition_item_project
        X Y label_project state_project) trX
     (pre_VLSM_projection_transition_item_project_infinitely_often
        X Y label_project state_project trX
        Hinf)) n =
omap
  (pre_VLSM_projection_transition_item_project
     X Y label_project state_project)
  (stream_prefix trX m)
finite_valid_trace_from Y (state_project sX)
  (VLSM_weak_projection_trace_project Hsimul
     (stream_prefix trX m))
  by apply VLSM_weak_projection_finite_valid_trace_from, infinite_valid_trace_from_prefix.
Qed.

Lemma VLSM_weak_projection_infinite_finite_valid_trace_from
  : forall sX trX (Hfin : FinitelyManyBound (VLSM_weak_projection_in Hsimul) trX),
    infinite_valid_trace_from X sX trX ->
    finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_infinite_finite_trace_project Hsimul trX Hfin).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (VLSM_weak_projection_in Hsimul) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_infinite_finite_trace_project
         Hsimul trX Hfin)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (VLSM_weak_projection_in Hsimul) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_weak_projection_infinite_finite_trace_project
         Hsimul trX Hfin)
  intros sX trX Hfin HtrX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (VLSM_weak_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
finite_valid_trace_from Y (state_project sX)
  (VLSM_weak_projection_infinite_finite_trace_project
     Hsimul trX Hfin)
  apply VLSM_weak_projection_finite_valid_trace_from.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound
  (VLSM_weak_projection_in Hsimul) 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_projection determines a VLSM_partial_projection, allowing us to lift to VLSM projection the generic results proved about VLSM partial projections.

Lemma VLSM_weak_partial_projection_from_projection :
  VLSM_weak_partial_projection X Y
    (VLSM_partial_trace_project_from_projection label_project state_project).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
  split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_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
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project) by apply VLSM_partial_projection_type_from_projection, Hsimul.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_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
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
sX: state X
trX: list transition_item
finite_valid_trace_from X sX trX
→ finite_valid_trace_from Y (state_project sX)
    (pre_VLSM_projection_finite_trace_project X Y
       label_project state_project trX)
    by apply VLSM_weak_projection_finite_valid_trace_from.
Qed.

Lemma VLSM_weak_projection_valid_state
  : forall sX,
    valid_state_prop X sX -> valid_state_prop Y (state_project sX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
  specialize VLSM_weak_partial_projection_from_projection as Hpart_simul.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
  specialize (VLSM_weak_partial_projection_valid_state Hpart_simul) as Hps.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Hps: ∀ (sX : state X) (sY : state Y) 
  (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, []) = Some (sY, trY)
  → valid_state_prop X sX
    → valid_state_prop Y sY
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
  by intro sX; eapply Hps.
Qed.

Lemma VLSM_weak_projection_input_valid_transition
  : forall lX lY, label_project lX = Some lY ->
    forall s im s' om,
    input_valid_transition X lX (s, im) (s', om) ->
    input_valid_transition Y lY (state_project s, im) (state_project s', om).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message) (s' : state
                                                 X) 
      (om : option message),
      input_valid_transition X lX (s, im) (s', om)
      → input_valid_transition Y lY
          (state_project s, im) (state_project s', om)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message) (s' : state
                                                 X) 
      (om : option message),
      input_valid_transition X lX (s, im) (s', om)
      → input_valid_transition Y lY
          (state_project s, im) (state_project s', om)
  specialize VLSM_weak_partial_projection_from_projection as Hpart_simul.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message) (s' : state
                                                 X) 
      (om : option message),
      input_valid_transition X lX (s, im) (s', om)
      → input_valid_transition Y lY
          (state_project s, im) (state_project s', om)
  specialize (VLSM_weak_partial_projection_input_valid_transition Hpart_simul) as Hivt.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Hivt: ∀ (sX : state X) (itemX : transition_item) 
  (sY : state Y) (itemY : transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, [itemX]) = Some (sY, [itemY])
  → input_valid_transition X 
      (l itemX) (sX, input itemX)
      (destination itemX, output itemX)
    → input_valid_transition Y 
        (l itemY) (sY, input itemY)
        (destination itemY, output itemY)
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message) (s' : state
                                                 X) 
      (om : option message),
      input_valid_transition X lX (s, im) (s', om)
      → input_valid_transition Y lY
          (state_project s, im) (state_project s', om)
  intros.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Hivt: ∀ (sX : state X) (itemX : transition_item) 
  (sY : state Y) (itemY : transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, [itemX]) = Some (sY, [itemY])
  → input_valid_transition X 
      (l itemX) (sX, input itemX)
      (destination itemX, output itemX)
    → input_valid_transition Y 
        (l itemY) (sY, input itemY)
        (destination itemY, output itemY)
lX: label X
lY: label Y
H: label_project lX = Some lY
s: state X
im: option message
s': state X
om: option message
H0: input_valid_transition X lX (s, im) (s', om)
input_valid_transition Y lY (state_project s, im)
  (state_project s', om)
  apply
    (Hivt s {| l := lX; input := im; destination := s'; output := om |}
      (state_project s) {| l := lY; input := im; destination := state_project s'; output := om |})
  ; [| done].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Hivt: ∀ (sX : state X) (itemX : transition_item) 
  (sY : state Y) (itemY : transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, [itemX]) = Some (sY, [itemY])
  → input_valid_transition X 
      (l itemX) (sX, input itemX)
      (destination itemX, output itemX)
    → input_valid_transition Y 
        (l itemY) (sY, input itemY)
        (destination itemY, output itemY)
lX: label X
lY: label Y
H: label_project lX = Some lY
s: state X
im: option message
s': state X
om: option message
H0: input_valid_transition X lX (s, im) (s', om)
VLSM_partial_trace_project_from_projection
  label_project state_project
  (s,
   [{|
      l := lX;
      input := im;
      destination := s';
      output := om
    |}]) =
Some
  (state_project s,
   [{|
      l := lY;
      input := im;
      destination := state_project s';
      output := om
    |}])
  by cbn; unfold pre_VLSM_projection_transition_item_project; cbn; rewrite H.
Qed.

Lemma VLSM_weak_projection_input_valid
  : forall lX lY, label_project lX = Some lY ->
    forall s im, input_valid X lX (s, im) -> input_valid Y lY (state_project s, im).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message),
      input_valid X lX (s, im)
      → input_valid Y lY (state_project s, im)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message),
      input_valid X lX (s, im)
      → input_valid Y lY (state_project s, im)
  intros lX lY Hpr sX im HvX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
lX: label X
lY: label Y
Hpr: label_project lX = Some lY
sX: state X
im: option message
HvX: input_valid X lX (sX, im)
input_valid Y lY (state_project sX, im)
  destruct (transition X lX (sX, im)) eqn: HtX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
lX: label X
lY: label Y
Hpr: label_project lX = Some lY
sX: state X
im: option message
HvX: input_valid X lX (sX, im)
s: state X
o: option message
HtX: transition lX (sX, im) = (s, o)
input_valid Y lY (state_project sX, im)
  by eapply VLSM_weak_projection_input_valid_transition, input_valid_can_transition.
Qed.

Lemma VLSM_weak_projection_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_projection_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_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_projection_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_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_projection_trace_project Hsimul trX)
  specialize VLSM_weak_partial_projection_from_projection as Hpart_simul.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_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_projection_trace_project Hsimul trX)
  specialize (VLSM_weak_partial_projection_finite_valid_trace_from Hpart_simul) as Htr.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Htr: ∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
∀ (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_projection_trace_project Hsimul trX)
  intros sX s'X trX HtrX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Htr: ∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
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_projection_trace_project Hsimul trX)
  apply valid_trace_get_last in HtrX as Hs'X.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Htr: ∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from_to X sX s'X trX
Hs'X: finite_trace_last sX trX = s'X
finite_valid_trace_from_to Y (state_project sX)
  (state_project s'X)
  (VLSM_weak_projection_trace_project Hsimul trX)
  apply valid_trace_forget_last in HtrX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Htr: ∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
sX, s'X: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
Hs'X: finite_trace_last sX trX = s'X
finite_valid_trace_from_to Y (state_project sX)
  (state_project s'X)
  (VLSM_weak_projection_trace_project Hsimul trX) subst.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Htr: ∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
finite_valid_trace_from_to Y (state_project sX)
  (state_project (finite_trace_last sX trX))
  (VLSM_weak_projection_trace_project Hsimul trX)
  rewrite (final_state_project _ _ _ _ Hsimul); [| done].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
Hpart_simul: VLSM_weak_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Htr: ∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
finite_valid_trace_from_to Y (state_project sX)
  (finite_trace_last (state_project sX)
     (pre_VLSM_projection_finite_trace_project X Y
        label_project state_project trX))
  (VLSM_weak_projection_trace_project Hsimul trX)
  by apply valid_trace_add_default_last; eauto.
Qed.

Lemma VLSM_weak_projection_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
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_project
∀ s1 s2 : state X,
  in_futures X s1 s2
  → in_futures Y (state_project s1) (state_project s2)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_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
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_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_projection_trace_project Hsimul tr).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_weak_projection X Y label_project
  state_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_projection_trace_project Hsimul tr)
  by apply VLSM_weak_projection_finite_valid_trace_from_to.
Qed.

End sec_weak_projection_properties.

Section sec_projection_properties.

Definition VLSM_projection_finite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_projection X Y label_project state_project)
  : list (transition_item X) -> list (transition_item Y)
  := pre_VLSM_projection_finite_trace_project _ _ label_project state_project.

Definition VLSM_projection_in
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_projection X Y label_project state_project)
  := pre_VLSM_projection_in_projection _ _ label_project.

Definition VLSM_projection_infinite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_projection X Y label_project state_project)
  (s : Streams.Stream (transition_item X))
  (Hinf : InfinitelyOften (VLSM_projection_in Hsimul) s)
  : Streams.Stream (transition_item Y)
  := pre_VLSM_projection_infinite_trace_project _ _ label_project state_project s Hinf.

Definition VLSM_projection_infinite_finite_trace_project
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (Hsimul : VLSM_projection X Y label_project state_project)
  (s : Streams.Stream (transition_item X))
  (Hfin : FinitelyManyBound (VLSM_projection_in Hsimul) s)
  : list (transition_item Y)
  := pre_VLSM_projection_infinite_finite_trace_project _ _ label_project state_project s Hfin.

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

Lemma VLSM_projection_finite_trace_project_app :
  forall l1 l2,
    VLSM_projection_finite_trace_project Hsimul (l1 ++ l2) =
    VLSM_projection_finite_trace_project Hsimul l1 ++ VLSM_projection_finite_trace_project Hsimul l2.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ l1 l2 : list transition_item,
  VLSM_projection_finite_trace_project Hsimul
    (l1 ++ l2) =
  VLSM_projection_finite_trace_project Hsimul l1 ++
  VLSM_projection_finite_trace_project Hsimul l2
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ l1 l2 : list transition_item,
  VLSM_projection_finite_trace_project Hsimul
    (l1 ++ l2) =
  VLSM_projection_finite_trace_project Hsimul l1 ++
  VLSM_projection_finite_trace_project Hsimul l2
  exact (pre_VLSM_projection_finite_trace_project_app _ _ label_project state_project).
Qed.

Lemma VLSM_projection_finite_trace_project_app_rev :
  forall l l1' l2',
    VLSM_projection_finite_trace_project Hsimul l = l1' ++ l2' ->
    exists l1 l2,
      l = l1 ++ l2 /\
      VLSM_projection_finite_trace_project Hsimul l1 = l1' /\
      VLSM_projection_finite_trace_project Hsimul l2 = l2'.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ l l1' l2' : list transition_item,
  VLSM_projection_finite_trace_project Hsimul l =
  l1' ++ l2'
  → ∃ l1 l2 : list transition_item,
      l = l1 ++ l2
      ∧ VLSM_projection_finite_trace_project Hsimul l1 =
        l1'
        ∧ VLSM_projection_finite_trace_project Hsimul
            l2 = l2'
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ l l1' l2' : list transition_item,
  VLSM_projection_finite_trace_project Hsimul l =
  l1' ++ l2'
  → ∃ l1 l2 : list transition_item,
      l = l1 ++ l2
      ∧ VLSM_projection_finite_trace_project Hsimul l1 =
        l1'
        ∧ VLSM_projection_finite_trace_project Hsimul
            l2 = l2'
  exact (pre_VLSM_projection_finite_trace_project_app_rev _ _ label_project state_project).
Qed.

Lemma VLSM_projection_finite_trace_project_in :
  forall itemX itemY,
    pre_VLSM_projection_transition_item_project
      _ _ label_project state_project itemX = Some itemY ->
  forall trX,
    itemX ∈ trX -> itemY ∈ VLSM_projection_finite_trace_project Hsimul trX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ itemX itemY : transition_item,
  pre_VLSM_projection_transition_item_project X Y
    label_project state_project itemX = Some itemY
  → ∀ trX : list transition_item,
      itemX ∈ trX
      → itemY
        ∈ VLSM_projection_finite_trace_project Hsimul
            trX
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ itemX itemY : transition_item,
  pre_VLSM_projection_transition_item_project X Y
    label_project state_project itemX = Some itemY
  → ∀ trX : list transition_item,
      itemX ∈ trX
      → itemY
        ∈ VLSM_projection_finite_trace_project Hsimul
            trX
  exact (pre_VLSM_projection_finite_trace_project_elem_of _ _ label_project state_project).
Qed.

Lemma VLSM_projection_finite_trace_last :
  forall (sX : state X) (trX : list (transition_item X)),
    finite_valid_trace_from X sX trX ->
      state_project (finite_trace_last sX trX) =
      finite_trace_last (state_project sX) (VLSM_projection_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → state_project (finite_trace_last sX trX) =
    finite_trace_last (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → state_project (finite_trace_last sX trX) =
    finite_trace_last (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
  exact (final_state_project _ _ _ _ Hsimul).
Qed.

Lemma VLSM_projection_finite_valid_trace :
  forall (sX : state X) (trX : list (transition_item X)),
    finite_valid_trace X sX trX ->
      finite_valid_trace Y (state_project sX) (VLSM_projection_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
  exact (trace_project_preserves_valid_trace _ _ _ _ Hsimul).
Qed.

Any VLSM_projection determines a VLSM_partial_projection, allowing us to lift to VLSM projection the generic results proved about VLSM partial projections.

Lemma VLSM_partial_projection_from_projection :
  VLSM_partial_projection X Y
    (VLSM_partial_trace_project_from_projection label_project state_project).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
  split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace X sX trX
    → finite_valid_trace Y sY trY
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
VLSM_partial_projection_type X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project) by apply VLSM_partial_projection_type_from_projection, Hsimul.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (sX, trX) =
  Some (sY, trY)
  → finite_valid_trace X sX trX
    → finite_valid_trace Y sY trY cbn; intros sX trX sY trY [= <- <-].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: list transition_item
finite_valid_trace X sX trX
→ finite_valid_trace Y (state_project sX)
    (pre_VLSM_projection_finite_trace_project X Y
       label_project state_project trX)
    by apply VLSM_projection_finite_valid_trace.
Qed.

Lemma VLSM_projection_finite_valid_trace_from
  : forall sX trX,
      finite_valid_trace_from X sX trX ->
      finite_valid_trace_from Y (state_project sX) (VLSM_projection_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
  specialize VLSM_partial_projection_from_projection as Hpart_simul.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hpart_simul: VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
  specialize (VLSM_partial_projection_finite_valid_trace_from Hpart_simul) as Hivt.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hpart_simul: VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
Hivt: ∀ (sX : state X) (trX : list transition_item) 
  (sY : state Y) (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_projection_finite_trace_project Hsimul trX)
  by intros sX trX; apply Hivt.
Qed.

Definition VLSM_projection_weaken : VLSM_weak_projection X Y label_project state_project :=
  {| weak_projection_type := projection_type _ _ _ _ Hsimul
  ;  weak_trace_project_preserves_valid_trace := VLSM_projection_finite_valid_trace_from
  |}.

Lemma VLSM_projection_valid_state :
  forall sX : state X,
    valid_state_prop X sX -> valid_state_prop Y (state_project sX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ sX : state X,
  valid_state_prop X sX
  → valid_state_prop Y (state_project sX)
  exact (VLSM_weak_projection_valid_state VLSM_projection_weaken).
Qed.

Lemma VLSM_projection_input_valid_transition :
  forall lX lY,
    label_project lX = Some lY ->
  forall s im s' om,
    input_valid_transition X lX (s, im) (s', om) ->
    input_valid_transition Y lY (state_project s, im) (state_project s', om).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message) (s' : state
                                                 X) 
      (om : option message),
      input_valid_transition X lX (s, im) (s', om)
      → input_valid_transition Y lY
          (state_project s, im) (state_project s', om)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message) (s' : state
                                                 X) 
      (om : option message),
      input_valid_transition X lX (s, im) (s', om)
      → input_valid_transition Y lY
          (state_project s, im) (state_project s', om)
  exact (VLSM_weak_projection_input_valid_transition VLSM_projection_weaken).
Qed.

Lemma VLSM_projection_input_valid :
  forall (lX : label X) (lY : label Y),
    label_project lX = Some lY ->
  forall (s : state X) (im : option message),
    input_valid X lX (s, im) -> input_valid Y lY (state_project s, im).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message),
      input_valid X lX (s, im)
      → input_valid Y lY (state_project s, im)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (lX : label X) (lY : label Y),
  label_project lX = Some lY
  → ∀ (s : state X) (im : option message),
      input_valid X lX (s, im)
      → input_valid Y lY (state_project s, im)
  exact (VLSM_weak_projection_input_valid VLSM_projection_weaken).
Qed.

Lemma VLSM_projection_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_projection_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_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_projection_finite_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_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_projection_finite_trace_project Hsimul trX)
  exact (VLSM_weak_projection_finite_valid_trace_from_to VLSM_projection_weaken).
Qed.

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

Lemma VLSM_projection_infinite_valid_trace_from :
  forall sX trX (Hinf : InfinitelyOften (VLSM_projection_in Hsimul) trX),
    infinite_valid_trace_from X sX trX ->
    infinite_valid_trace_from Y (state_project sX)
      (VLSM_projection_infinite_trace_project Hsimul trX Hinf).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften (VLSM_projection_in Hsimul)
            trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_projection_infinite_trace_project Hsimul
         trX Hinf)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften (VLSM_projection_in Hsimul)
            trX),
  infinite_valid_trace_from X sX trX
  → infinite_valid_trace_from Y (state_project sX)
      (VLSM_projection_infinite_trace_project Hsimul
         trX Hinf)
  exact (VLSM_weak_projection_infinite_valid_trace_from VLSM_projection_weaken).
Qed.

Lemma VLSM_projection_infinite_finite_valid_trace_from :
  forall sX trX (Hfin : FinitelyManyBound (VLSM_projection_in Hsimul) trX),
    infinite_valid_trace_from X sX trX ->
    finite_valid_trace_from Y (state_project sX)
      (VLSM_projection_infinite_finite_trace_project Hsimul trX Hfin).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (VLSM_projection_in Hsimul) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_projection_infinite_finite_trace_project
         Hsimul trX Hfin)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (VLSM_projection_in Hsimul) trX),
  infinite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (VLSM_projection_infinite_finite_trace_project
         Hsimul trX Hfin)
  exact (VLSM_weak_projection_infinite_finite_valid_trace_from VLSM_projection_weaken).
Qed.

Lemma VLSM_projection_initial_state
  : forall sX, initial_state_prop X sX -> initial_state_prop Y (state_project sX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ sX : state X,
  initial_state_prop sX
  → initial_state_prop (state_project sX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ sX : state X,
  initial_state_prop sX
  → initial_state_prop (state_project sX)
  specialize VLSM_partial_projection_from_projection as Hpart_simul.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hpart_simul: VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
∀ sX : state X,
  initial_state_prop sX
  → initial_state_prop (state_project sX)
  specialize (VLSM_partial_projection_initial_state Hpart_simul) as His.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hpart_simul: VLSM_partial_projection X Y
  (VLSM_partial_trace_project_from_projection
     label_project state_project)
His: ∀ (sX : state X) (sY : state Y) 
  (trY : list transition_item),
  VLSM_partial_trace_project_from_projection
    label_project state_project (
    sX, []) = Some (sY, trY)
  → initial_state_prop sX
    → initial_state_prop sY
∀ sX : state X,
  initial_state_prop sX
  → initial_state_prop (state_project sX)
  by intro sX; eapply His.
Qed.

Lemma VLSM_projection_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_projection_finite_trace_project Hsimul trX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_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_projection_finite_trace_project Hsimul trX)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_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_projection_finite_trace_project Hsimul trX)
  intros.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_init_to X sX s'X trX
finite_valid_trace_init_to Y (state_project sX)
  (state_project s'X)
  (VLSM_projection_finite_trace_project Hsimul trX) destruct H as [H Hinit].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
Hinit: initial_state_prop sX
finite_valid_trace_init_to Y (state_project sX)
  (state_project s'X)
  (VLSM_projection_finite_trace_project Hsimul trX) split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
Hinit: initial_state_prop sX
finite_valid_trace_from_to Y (state_project sX)
  (state_project s'X)
  (VLSM_projection_finite_trace_project Hsimul trX)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
Hinit: initial_state_prop sX
initial_state_prop (state_project sX)
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
Hinit: initial_state_prop sX
finite_valid_trace_from_to Y (state_project sX)
  (state_project s'X)
  (VLSM_projection_finite_trace_project Hsimul trX) by apply VLSM_projection_finite_valid_trace_from_to.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX, s'X: state X
trX: list transition_item
H: finite_valid_trace_from_to X sX s'X trX
Hinit: initial_state_prop sX
initial_state_prop (state_project sX) by apply VLSM_projection_initial_state.
Qed.

Lemma VLSM_projection_infinite_valid_trace
  : forall sX trX (Hinf : InfinitelyOften (VLSM_projection_in Hsimul) trX),
    infinite_valid_trace X sX trX ->
    infinite_valid_trace Y (state_project sX)
      (VLSM_projection_infinite_trace_project Hsimul trX Hinf).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften (VLSM_projection_in Hsimul)
            trX),
  infinite_valid_trace X sX trX
  → infinite_valid_trace Y (state_project sX)
      (VLSM_projection_infinite_trace_project Hsimul
         trX Hinf)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hinf : InfinitelyOften (VLSM_projection_in Hsimul)
            trX),
  infinite_valid_trace X sX trX
  → infinite_valid_trace Y (state_project sX)
      (VLSM_projection_infinite_trace_project Hsimul
         trX Hinf)
  intros sX trX Hinf [HtrX HsX].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften (VLSM_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
infinite_valid_trace Y (state_project sX)
  (VLSM_projection_infinite_trace_project Hsimul trX
     Hinf)
  split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften (VLSM_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
infinite_valid_trace_from Y (state_project sX)
  (VLSM_projection_infinite_trace_project Hsimul trX
     Hinf)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften (VLSM_projection_in Hsimul) 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
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften (VLSM_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
infinite_valid_trace_from Y (state_project sX)
  (VLSM_projection_infinite_trace_project Hsimul trX
     Hinf) by apply VLSM_projection_infinite_valid_trace_from.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hinf: InfinitelyOften (VLSM_projection_in Hsimul) trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX) by apply VLSM_projection_initial_state.
Qed.

Lemma VLSM_projection_infinite_finite_valid_trace
  : forall sX trX (Hfin : FinitelyManyBound (VLSM_projection_in Hsimul) trX),
    infinite_valid_trace X sX trX ->
    finite_valid_trace Y (state_project sX)
      (VLSM_projection_infinite_finite_trace_project Hsimul trX Hfin).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (VLSM_projection_in Hsimul) trX),
  infinite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_projection_infinite_finite_trace_project
         Hsimul trX Hfin)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
∀ (sX : state X) (trX : Streams.Stream transition_item) 
  (Hfin : FinitelyManyBound
            (VLSM_projection_in Hsimul) trX),
  infinite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (VLSM_projection_infinite_finite_trace_project
         Hsimul trX Hfin)
  intros sX trX Hfin [HtrX HsX].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound (VLSM_projection_in Hsimul)
  trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace Y (state_project sX)
  (VLSM_projection_infinite_finite_trace_project
     Hsimul trX Hfin)
  split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound (VLSM_projection_in Hsimul)
  trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (VLSM_projection_infinite_finite_trace_project
     Hsimul trX Hfin)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound (VLSM_projection_in Hsimul)
  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
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound (VLSM_projection_in Hsimul)
  trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (VLSM_projection_infinite_finite_trace_project
     Hsimul trX Hfin) by apply VLSM_projection_infinite_finite_valid_trace_from.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
sX: state X
trX: Streams.Stream transition_item
Hfin: FinitelyManyBound (VLSM_projection_in Hsimul)
  trX
HtrX: infinite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX) by apply VLSM_projection_initial_state.
Qed.

Projection friendliness

A projection is friendly if all the valid traces of the projection are projections of the valid traces of the source VLSM.

Section sec_projection_friendliness.

We axiomatize projection friendliness as the converse of VLSM_projection_finite_valid_trace

Definition projection_friendly_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
      /\ VLSM_projection_finite_trace_project Hsimul trX = trY.

Lemma projection_friendly_in_futures
  (Hfr : projection_friendly_prop)
  (s1 s2 : state Y)
  (Hfuture : in_futures Y s1 s2)
  : exists (sX1 sX2 : state X),
    state_project sX1 = s1 /\ state_project sX2 = s2 /\ in_futures X sX1 sX2.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
Hfuture: in_futures Y s1 s2
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
Hfuture: in_futures Y s1 s2
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
  destruct Hfuture as [tr_s2 Hfuture].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
tr_s2: list transition_item
Hfuture: finite_valid_trace_from_to Y s1 s2 tr_s2
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
  apply finite_valid_trace_from_to_complete_left in Hfuture
    as [is [tr_s1 [Htr Heq_s1]]].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
tr_s2: list transition_item
is: state Y
tr_s1: list transition_item
Htr: finite_valid_trace_init_to Y is s2
  (tr_s1 ++ tr_s2)
Heq_s1: finite_trace_last is tr_s1 = s1
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
  apply valid_trace_get_last in Htr as Heq_s2.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
tr_s2: list transition_item
is: state Y
tr_s1: list transition_item
Htr: finite_valid_trace_init_to Y is s2
  (tr_s1 ++ tr_s2)
Heq_s1: finite_trace_last is tr_s1 = s1
Heq_s2: finite_trace_last is (tr_s1 ++ tr_s2) = s2
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
  apply valid_trace_forget_last in Htr.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
tr_s2: list transition_item
is: state Y
tr_s1: list transition_item
Htr: finite_valid_trace Y is (tr_s1 ++ tr_s2)
Heq_s1: finite_trace_last is tr_s1 = s1
Heq_s2: finite_trace_last is (tr_s1 ++ tr_s2) = s2
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
  apply Hfr in Htr as [isX [trX [Htr [His Htr_pr]]]].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
tr_s2: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace X isX trX
His: state_project isX = is
Htr_pr: VLSM_projection_finite_trace_project Hsimul
  trX = tr_s1 ++ tr_s2
Heq_s1: finite_trace_last is tr_s1 = s1
Heq_s2: finite_trace_last is (tr_s1 ++ tr_s2) = s2
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
  apply VLSM_projection_finite_trace_project_app_rev in Htr_pr
    as (trX_s1 & trX_s2 & HeqtrX & Htr_s1_pr & Htr_s2_pr).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
s1, s2: state Y
tr_s2: list transition_item
is: state Y
tr_s1: list transition_item
isX: state X
trX: list transition_item
Htr: finite_valid_trace X isX trX
His: state_project isX = is
trX_s1, trX_s2: list transition_item
HeqtrX: trX = trX_s1 ++ trX_s2
Htr_s1_pr: VLSM_projection_finite_trace_project
  Hsimul trX_s1 = tr_s1
Htr_s2_pr: VLSM_projection_finite_trace_project
  Hsimul trX_s2 = tr_s2
Heq_s1: finite_trace_last is tr_s1 = s1
Heq_s2: finite_trace_last is (tr_s1 ++ tr_s2) = s2
∃ sX1 sX2 : state X,
  state_project sX1 = s1
  ∧ state_project sX2 = s2 ∧ in_futures X sX1 sX2
  subst.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
Htr: finite_valid_trace X isX (trX_s1 ++ trX_s2)
∃ sX1 sX2 : state X,
  state_project sX1 =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1)
  ∧ state_project sX2 =
    finite_trace_last (state_project isX)
      (VLSM_projection_finite_trace_project Hsimul
         trX_s1 ++
       VLSM_projection_finite_trace_project Hsimul
         trX_s2) ∧ in_futures X sX1 sX2
  destruct Htr as [HtrX HisX].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
∃ sX1 sX2 : state X,
  state_project sX1 =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1)
  ∧ state_project sX2 =
    finite_trace_last (state_project isX)
      (VLSM_projection_finite_trace_project Hsimul
         trX_s1 ++
       VLSM_projection_finite_trace_project Hsimul
         trX_s2) ∧ in_futures X sX1 sX2
  apply finite_valid_trace_from_app_iff in HtrX as HtrX12.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
HtrX12: finite_valid_trace_from X isX trX_s1
∧ finite_valid_trace_from X
    (finite_trace_last isX trX_s1) trX_s2
∃ sX1 sX2 : state X,
  state_project sX1 =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1)
  ∧ state_project sX2 =
    finite_trace_last (state_project isX)
      (VLSM_projection_finite_trace_project Hsimul
         trX_s1 ++
       VLSM_projection_finite_trace_project Hsimul
         trX_s2) ∧ in_futures X sX1 sX2
  destruct HtrX12 as [HtrX1 HtrX2].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
HtrX1: finite_valid_trace_from X isX trX_s1
HtrX2: finite_valid_trace_from X
  (finite_trace_last isX trX_s1) trX_s2
∃ sX1 sX2 : state X,
  state_project sX1 =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1)
  ∧ state_project sX2 =
    finite_trace_last (state_project isX)
      (VLSM_projection_finite_trace_project Hsimul
         trX_s1 ++
       VLSM_projection_finite_trace_project Hsimul
         trX_s2) ∧ in_futures X sX1 sX2
  apply valid_trace_add_default_last in HtrX2.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
HtrX1: finite_valid_trace_from X isX trX_s1
HtrX2: finite_valid_trace_from_to X
  (finite_trace_last isX trX_s1)
  (finite_trace_last
     (finite_trace_last isX trX_s1) trX_s2)
  trX_s2
∃ sX1 sX2 : state X,
  state_project sX1 =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1)
  ∧ state_project sX2 =
    finite_trace_last (state_project isX)
      (VLSM_projection_finite_trace_project Hsimul
         trX_s1 ++
       VLSM_projection_finite_trace_project Hsimul
         trX_s2) ∧ in_futures X sX1 sX2
  exists (finite_trace_last isX trX_s1).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
HtrX1: finite_valid_trace_from X isX trX_s1
HtrX2: finite_valid_trace_from_to X
  (finite_trace_last isX trX_s1)
  (finite_trace_last
     (finite_trace_last isX trX_s1) trX_s2)
  trX_s2
∃ sX2 : state X,
  state_project (finite_trace_last isX trX_s1) =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1)
  ∧ state_project sX2 =
    finite_trace_last (state_project isX)
      (VLSM_projection_finite_trace_project Hsimul
         trX_s1 ++
       VLSM_projection_finite_trace_project Hsimul
         trX_s2)
    ∧ in_futures X (finite_trace_last isX trX_s1) sX2
  exists (finite_trace_last isX  (trX_s1 ++ trX_s2)).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
HtrX1: finite_valid_trace_from X isX trX_s1
HtrX2: finite_valid_trace_from_to X
  (finite_trace_last isX trX_s1)
  (finite_trace_last
     (finite_trace_last isX trX_s1) trX_s2)
  trX_s2
state_project (finite_trace_last isX trX_s1) =
finite_trace_last (state_project isX)
  (VLSM_projection_finite_trace_project Hsimul trX_s1)
∧ state_project
    (finite_trace_last isX (trX_s1 ++ trX_s2)) =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1 ++
     VLSM_projection_finite_trace_project Hsimul
       trX_s2)
  ∧ in_futures X (finite_trace_last isX trX_s1)
      (finite_trace_last isX (trX_s1 ++ trX_s2))
  rewrite !VLSM_projection_finite_trace_last,
    VLSM_projection_finite_trace_project_app; [| done | done].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
HtrX1: finite_valid_trace_from X isX trX_s1
HtrX2: finite_valid_trace_from_to X
  (finite_trace_last isX trX_s1)
  (finite_trace_last
     (finite_trace_last isX trX_s1) trX_s2)
  trX_s2
finite_trace_last (state_project isX)
  (VLSM_projection_finite_trace_project Hsimul trX_s1) =
finite_trace_last (state_project isX)
  (VLSM_projection_finite_trace_project Hsimul trX_s1)
∧ finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1 ++
     VLSM_projection_finite_trace_project Hsimul
       trX_s2) =
  finite_trace_last (state_project isX)
    (VLSM_projection_finite_trace_project Hsimul
       trX_s1 ++
     VLSM_projection_finite_trace_project Hsimul
       trX_s2)
  ∧ in_futures X (finite_trace_last isX trX_s1)
      (finite_trace_last isX (trX_s1 ++ trX_s2))
  repeat split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfr: projection_friendly_prop
isX: state X
trX_s1, trX_s2: list transition_item
HtrX: finite_valid_trace_from X isX
  (trX_s1 ++ trX_s2)
HisX: initial_state_prop isX
HtrX1: finite_valid_trace_from X isX trX_s1
HtrX2: finite_valid_trace_from_to X
  (finite_trace_last isX trX_s1)
  (finite_trace_last
     (finite_trace_last isX trX_s1) trX_s2)
  trX_s2
in_futures X (finite_trace_last isX trX_s1)
  (finite_trace_last isX (trX_s1 ++ trX_s2))
  by rewrite finite_trace_last_app; eexists.
Qed.

A consequence of the projection_friendly_property is that the valid traces of the projection are precisely the projections of all the valid traces of the source VLSM.

Lemma projection_friendly_trace_char
  (Hfriendly : projection_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
      /\ VLSM_projection_finite_trace_project Hsimul trX = trY.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfriendly: projection_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
         ∧ VLSM_projection_finite_trace_project Hsimul
             trX = trY)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfriendly: projection_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
         ∧ VLSM_projection_finite_trace_project Hsimul
             trX = trY)
  split; [by apply Hfriendly |].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfriendly: projection_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
     ∧ VLSM_projection_finite_trace_project Hsimul trX =
       trY) → finite_valid_trace Y sY trY
  intros [sX [trX [HtrX [<- <-]]]].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection X Y label_project
  state_project
Hfriendly: projection_friendly_prop
sX: state X
trX: list transition_item
HtrX: finite_valid_trace X sX trX
finite_valid_trace Y (state_project sX)
  (VLSM_projection_finite_trace_project Hsimul trX)
  by apply VLSM_projection_finite_valid_trace.
Qed.

End sec_projection_friendliness.

End sec_projection_properties.

End sec_VLSM_projection.

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

X's initial_states project to Y's initial states
Every message m (including the empty one) which can be input to a projectable input_valid transition in X, is a valid_message in Y
X's input_valid is included in Y's valid.
For all projectable input_valid inputs (in X), Y's transition acts like X's transition.
All non-projectable transitions preserve the projected state

Section sec_basic_VLSM_projection.

Section sec_basic_VLSM_projection_type.

Context
  {message : Type}
  (X : VLSM message)
  (TY : VLSMType message)
  (label_project : label X -> option (label TY))
  (state_project : state X -> state TY)
  (Htransition_None : weak_projection_transition_consistency_None X TY label_project state_project)
  .

Lemma basic_VLSM_projection_type
  : VLSM_projection_type X TY label_project state_project.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
VLSM_projection_type X TY label_project state_project
Proof.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
VLSM_projection_type X TY label_project state_project
  constructor.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → state_project (finite_trace_last sX trX) =
    finite_trace_last (state_project sX)
      (pre_VLSM_projection_finite_trace_project X TY
         label_project state_project trX)
  intros is tr Htr.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
is: state X
tr: list transition_item
Htr: finite_valid_trace_from X is tr
state_project (finite_trace_last is tr) =
finite_trace_last (state_project is)
  (pre_VLSM_projection_finite_trace_project X TY
     label_project state_project tr)
  induction Htr using finite_valid_trace_from_rev_ind
  ; [done |].message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
IHHtr: state_project (finite_trace_last s tr) =
finite_trace_last (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     TY label_project state_project tr)
state_project (finite_trace_last s (tr ++ [x])) =
finite_trace_last (state_project s)
  (pre_VLSM_projection_finite_trace_project X TY
     label_project state_project (tr ++ [x]))
  rewrite (pre_VLSM_projection_finite_trace_project_app _ _ label_project state_project).message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
IHHtr: state_project (finite_trace_last s tr) =
finite_trace_last (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     TY label_project state_project tr)
state_project (finite_trace_last s (tr ++ [x])) =
finite_trace_last (state_project s)
  (pre_VLSM_projection_finite_trace_project X TY
     label_project state_project tr ++
   pre_VLSM_projection_finite_trace_project X TY
     label_project state_project [x])
  rewrite finite_trace_last_is_last.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
IHHtr: state_project (finite_trace_last s tr) =
finite_trace_last (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     TY label_project state_project tr)
state_project (destination x) =
finite_trace_last (state_project s)
  (pre_VLSM_projection_finite_trace_project X TY
     label_project state_project tr ++
   pre_VLSM_projection_finite_trace_project X TY
     label_project state_project [x])
  rewrite finite_trace_last_app, <- IHHtr.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
IHHtr: state_project (finite_trace_last s tr) =
finite_trace_last (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     TY label_project state_project tr)
state_project (destination x) =
finite_trace_last
  (state_project (finite_trace_last s tr))
  (pre_VLSM_projection_finite_trace_project X TY
     label_project state_project [x])
  clear IHHtr.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
state_project (destination x) =
finite_trace_last
  (state_project (finite_trace_last s tr))
  (pre_VLSM_projection_finite_trace_project X TY
     label_project state_project [x])
  simpl.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
state_project sf =
finite_trace_last
  (state_project (finite_trace_last s tr))
  match
    pre_VLSM_projection_transition_item_project X TY
      label_project state_project x
  with
  | Some y => [y]
  | None => []
  end
  unfold pre_VLSM_projection_transition_item_project.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
state_project sf =
finite_trace_last
  (state_project (finite_trace_last s tr))
  match
    match label_project (VLSM.l x) with
    | Some lY =>
        Some
          {|
            l := lY;
            input := input x;
            destination :=
              state_project (destination x);
            output := output x
          |}
    | None => None
    end
  with
  | Some y => [y]
  | None => []
  end
  destruct (label_project _) as [lY |] eqn: Hl; [done |].message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: 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
Hl: label_project (VLSM.l x) = None
state_project sf =
finite_trace_last
  (state_project (finite_trace_last s tr)) []
  apply (Htransition_None _ Hl) in Hx.message: Type
X: VLSM message
TY: VLSMType message
label_project: label X → option (label TY)
state_project: state X → state TY
Htransition_None: weak_projection_transition_consistency_None
  X TY label_project state_project
s: state X
tr: list transition_item
Htr: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: state_project sf =
state_project (finite_trace_last s tr)
x:= {|
  l := l;
  input := iom;
  destination := sf;
  output := oom
|}: transition_item
Hl: label_project (VLSM.l x) = None
state_project sf =
finite_trace_last
  (state_project (finite_trace_last s tr)) []
  by rewrite Hx.
Qed.

End sec_basic_VLSM_projection_type.

Context
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> option (label Y))
  (state_project : state X -> state Y)
  (Hvalid : weak_projection_valid_preservation X Y label_project state_project)
  (Htransition_Some : weak_projection_transition_preservation_Some X Y label_project state_project)
  (Htransition_None : weak_projection_transition_consistency_None _ _ label_project state_project)
  (Htype : VLSM_projection_type X Y label_project state_project :=
    basic_VLSM_projection_type X Y label_project state_project Htransition_None)
  .

Section sec_weak_projection.

Context
  (Hstate : weak_projection_initial_state_preservation X Y state_project)
  (Hmessage : weak_projection_valid_message_preservation X Y label_project state_project)
  .

#[local] Lemma basic_VLSM_projection_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_projection_finite_trace_project _ _ label_project state_project tr).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project 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_projection_finite_trace_project X Y
     label_project state_project tr)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project 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_projection_finite_trace_project X Y
     label_project state_project tr)
  induction Htr using finite_valid_trace_init_to_rev_strong_ind; [by constructor; apply Hstate |].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: finite_valid_trace_from_to Y
  (state_project is) (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project tr)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project is)
  (state_project sf)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project
     (tr ++
      [{|
         l := l;
         input := iom;
         destination := sf;
         output := oom
       |}]))
  unfold pre_VLSM_projection_finite_trace_project.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: finite_valid_trace_from_to Y
  (state_project is) (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project tr)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project is)
  (state_project sf)
  (omap
     (pre_VLSM_projection_transition_item_project X Y
        label_project state_project)
     (tr ++
      [{|
         l := l;
         input := iom;
         destination := sf;
         output := oom
       |}]))
  rewrite omap_app.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: finite_valid_trace_from_to Y
  (state_project is) (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project tr)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project is)
  (state_project sf)
  (omap
     (pre_VLSM_projection_transition_item_project X Y
        label_project state_project) tr ++
   omap
     (pre_VLSM_projection_transition_item_project X Y
        label_project state_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
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: finite_valid_trace_from_to Y
  (state_project is) (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project tr)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  (omap
     (pre_VLSM_projection_transition_item_project X Y
        label_project state_project)
     [{|
        l := l;
        input := iom;
        destination := sf;
        output := oom
      |}])
  simpl.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: finite_valid_trace_from_to Y
  (state_project is) (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project tr)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  match
    pre_VLSM_projection_transition_item_project X Y
      label_project state_project
      {|
        l := l;
        input := iom;
        destination := sf;
        output := oom
      |}
  with
  | Some y => [y]
  | None => []
  end unfold pre_VLSM_projection_transition_item_project.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: finite_valid_trace_from_to Y
  (state_project is) (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project tr)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  match
    match
      label_project
        (VLSM.l
           {|
             l := l;
             input := iom;
             destination := sf;
             output := oom
           |})
    with
    | Some lY =>
        Some
          {|
            l := lY;
            input :=
              input
                {|
                  l := l;
                  input := iom;
                  destination := sf;
                  output := oom
                |};
            destination :=
              state_project
                (destination
                   {|
                     l := l;
                     input := iom;
                     destination := sf;
                     output := oom
                   |});
            output :=
              output
                {|
                  l := l;
                  input := iom;
                  destination := sf;
                  output := oom
                |}
          |}
    | None => None
    end
  with
  | Some y => [y]
  | None => []
  end
  simpl.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: finite_valid_trace_from_to Y
  (state_project is) (state_project s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project tr)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  match
    match label_project l with
    | Some lY =>
        Some
          {|
            l := lY;
            input := iom;
            destination := state_project sf;
            output := oom
          |}
    | None => None
    end
  with
  | Some y => [y]
  | None => []
  end
  apply valid_trace_last_pstate in IHHtr1.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  match
    match label_project l with
    | Some lY =>
        Some
          {|
            l := lY;
            input := iom;
            destination := state_project sf;
            output := oom
          |}
    | None => None
    end
  with
  | Some y => [y]
  | None => []
  end
  destruct (label_project l) as [lY |] eqn: Hl; cycle 1.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
Hl: label_project l = None
finite_valid_trace_from_to Y (state_project s)
  (state_project sf) []
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
finite_valid_trace_from_to Y 
  (state_project s) (state_project sf)
  [{|
     l := lY;
     input := iom;
     destination := state_project sf;
     output := oom
   |}]
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
Hl: label_project l = None
finite_valid_trace_from_to Y (state_project s)
  (state_project sf) [] by apply (Htransition_None _ Hl) in Ht; rewrite Ht; constructor.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
finite_valid_trace_from_to Y (state_project s)
  (state_project sf)
  [{|
     l := lY;
     input := iom;
     destination := state_project sf;
     output := oom
   |}] apply finite_valid_trace_from_to_singleton.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
input_valid_transition Y lY (state_project s, iom)
  (state_project sf, oom)
    assert (Hiom : option_valid_message_prop Y iom).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
option_valid_message_prop Y iom
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
Hiom: option_valid_message_prop Y iom
input_valid_transition Y lY (
  state_project s, iom) (
  state_project sf, oom)
    {message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
option_valid_message_prop Y iom
      destruct iom as [im |]; [| by apply option_valid_message_None].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
im: message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr (Some im)
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, Some im) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
option_valid_message_prop Y (Some im)
      by apply (Hmessage _ _ Hl _ _ (proj1 Ht)).
    }message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
lY: label Y
Hl: label_project l = Some lY
Hiom: option_valid_message_prop Y iom
input_valid_transition Y lY (state_project s, iom)
  (state_project sf, oom)
    specialize (Hvalid _ _ Hl _ _ (proj1 Ht) IHHtr1 Hiom).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
s: state X
iom: option message
lY: label Y
Hvalid: valid lY (state_project s, iom)
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
is: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom_si, iom_s: state X
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output X
  iom_tr iom
Htr2: finite_valid_trace_init_to X iom_si iom_s
  iom_tr
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr1: valid_state_prop Y (state_project s)
IHHtr2: finite_valid_trace_from_to Y
  (state_project iom_si)
  (state_project iom_s)
  (pre_VLSM_projection_finite_trace_project X
     Y label_project state_project iom_tr)
Hl: label_project l = Some lY
Hiom: option_valid_message_prop Y iom
input_valid_transition Y lY (state_project s, iom)
  (state_project sf, oom)
    by apply (Htransition_Some _ _ Hl) in Ht.
Qed.

#[local] Lemma basic_VLSM_projection_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_projection_finite_trace_project _ _ label_project state_project ls).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project 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_projection_finite_trace_project X Y
     label_project state_project ls)
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project 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_projection_finite_trace_project X Y
     label_project state_project ls)
  apply valid_trace_add_default_last in Hpxt.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  apply valid_trace_first_pstate in Hpxt as Hs.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
Hs: valid_state_prop X s
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  apply valid_state_has_trace in Hs as [is_s [tr_s Hs]].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_init_to X is_s s tr_s
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  specialize (finite_valid_trace_from_to_app X _ _ _ _ _ (proj1 Hs) Hpxt) as Happ.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_init_to X is_s s tr_s
Happ: finite_valid_trace_from_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  specialize (basic_VLSM_projection_finite_valid_trace_init_to _ _ _ (conj Happ (proj2 Hs)))
    as Happ_pr.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_init_to X is_s s tr_s
Happ: finite_valid_trace_from_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Happ_pr: finite_valid_trace_from_to Y
  (state_project is_s)
  (state_project (finite_trace_last s ls))
  (pre_VLSM_projection_finite_trace_project
     X Y label_project state_project
     (tr_s ++ ls))
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  rewrite (pre_VLSM_projection_finite_trace_project_app _ _ label_project state_project) in Happ_pr.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_init_to X is_s s tr_s
Happ: finite_valid_trace_from_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Happ_pr: finite_valid_trace_from_to Y
  (state_project is_s)
  (state_project (finite_trace_last s ls))
  (pre_VLSM_projection_finite_trace_project
     X Y label_project state_project tr_s ++
   pre_VLSM_projection_finite_trace_project
     X Y label_project state_project ls)
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  apply finite_valid_trace_from_to_app_split, proj2 in Happ_pr.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_init_to X is_s s tr_s
Happ: finite_valid_trace_from_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Happ_pr: finite_valid_trace_from_to Y
  (finite_trace_last (state_project is_s)
     (pre_VLSM_projection_finite_trace_project
        X Y label_project state_project tr_s))
  (state_project (finite_trace_last s ls))
  (pre_VLSM_projection_finite_trace_project
     X Y label_project state_project ls)
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  apply valid_trace_get_last in Hs as Heqs.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_init_to X is_s s tr_s
Happ: finite_valid_trace_from_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Happ_pr: finite_valid_trace_from_to Y
  (finite_trace_last (state_project is_s)
     (pre_VLSM_projection_finite_trace_project
        X Y label_project state_project tr_s))
  (state_project (finite_trace_last s ls))
  (pre_VLSM_projection_finite_trace_project
     X Y label_project state_project ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  apply valid_trace_forget_last, proj1 in Hs.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_from X is_s tr_s
Happ: finite_valid_trace_from_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Happ_pr: finite_valid_trace_from_to Y
  (finite_trace_last (state_project is_s)
     (pre_VLSM_projection_finite_trace_project
        X Y label_project state_project tr_s))
  (state_project (finite_trace_last s ls))
  (pre_VLSM_projection_finite_trace_project
     X Y label_project state_project ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  rewrite <- (final_state_project X Y label_project state_project Htype)
    in Happ_pr by done.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
s: state X
ls: list transition_item
Hpxt: finite_valid_trace_from_to X s
  (finite_trace_last s ls) ls
is_s: state X
tr_s: list transition_item
Hs: finite_valid_trace_from X is_s tr_s
Happ: finite_valid_trace_from_to X is_s
  (finite_trace_last s ls) 
  (tr_s ++ ls)
Happ_pr: finite_valid_trace_from_to Y
  (state_project
     (finite_trace_last is_s tr_s))
  (state_project (finite_trace_last s ls))
  (pre_VLSM_projection_finite_trace_project
     X Y label_project state_project ls)
Heqs: finite_trace_last is_s tr_s = s
finite_valid_trace_from Y (state_project s)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project ls)
  by apply valid_trace_forget_last in Happ_pr; subst.
Qed.

Lemma basic_VLSM_weak_projection
  : VLSM_weak_projection X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
VLSM_weak_projection X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
VLSM_weak_projection X Y label_project state_project
  constructor; [done |].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: weak_projection_initial_state_preservation X
  Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace_from X sX trX
  → finite_valid_trace_from Y (state_project sX)
      (pre_VLSM_projection_finite_trace_project X Y
         label_project state_project trX)
  apply basic_VLSM_projection_finite_valid_trace_from.
Qed.

End sec_weak_projection.

Lemma basic_VLSM_weak_projection_strengthen
  (Hweak : VLSM_weak_projection X Y label_project state_project)
  (Hstate : strong_projection_initial_state_preservation X Y state_project)
  : VLSM_projection X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hweak: VLSM_weak_projection X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
VLSM_projection X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hweak: VLSM_weak_projection X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
VLSM_projection X Y label_project state_project
  constructor; [by apply Hweak |].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hweak: VLSM_weak_projection X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
∀ (sX : state X) (trX : list transition_item),
  finite_valid_trace X sX trX
  → finite_valid_trace Y (state_project sX)
      (pre_VLSM_projection_finite_trace_project X Y
         label_project state_project trX)
  intros sX trX [HtrX HsX]; split.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hweak: VLSM_weak_projection X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project trX)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hweak: VLSM_weak_projection X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX)
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hweak: VLSM_weak_projection X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
finite_valid_trace_from Y (state_project sX)
  (pre_VLSM_projection_finite_trace_project X Y
     label_project state_project trX) by apply (VLSM_weak_projection_finite_valid_trace_from Hweak).
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hweak: VLSM_weak_projection X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
HsX: initial_state_prop sX
initial_state_prop (state_project sX) by apply Hstate.
Qed.

Lemma basic_VLSM_projection
  (Hstate : strong_projection_initial_state_preservation X Y state_project)
  (Hmessage : weak_projection_valid_message_preservation X Y label_project state_project)
  : VLSM_projection X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
VLSM_projection X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
VLSM_projection X Y label_project state_project
  apply basic_VLSM_weak_projection_strengthen; [| done].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
VLSM_weak_projection X Y label_project state_project
  apply basic_VLSM_weak_projection; [| done].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: weak_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: weak_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: weak_projection_transition_consistency_None
  X Y label_project state_project
Htype:= basic_VLSM_projection_type X Y label_project
  state_project Htransition_None: VLSM_projection_type X Y label_project
  state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: weak_projection_valid_message_preservation
  X Y label_project state_project
weak_projection_initial_state_preservation X Y
  state_project
  by apply strong_projection_initial_state_preservation_weaken.
Qed.

End sec_basic_VLSM_projection.

Lemma basic_VLSM_strong_projection
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> option (label Y))
  (state_project : state X -> state Y)
  (Hvalid : strong_projection_valid_preservation X Y label_project state_project)
  (Htransition_Some : strong_projection_transition_preservation_Some X Y label_project state_project)
  (Htransition_None : strong_projection_transition_consistency_None _ _ label_project state_project)
  (Hstate : strong_projection_initial_state_preservation X Y state_project)
  (Hmessage : strong_projection_valid_message_preservation X Y)
  : VLSM_projection X Y label_project state_project.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
VLSM_projection X Y label_project state_project
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
VLSM_projection X Y label_project state_project
  apply basic_VLSM_projection.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_valid_preservation X Y label_project
  state_project
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_transition_preservation_Some X Y
  label_project state_project
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_transition_consistency_None X Y
  label_project state_project
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
strong_projection_initial_state_preservation X Y
  state_project
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_valid_message_preservation X Y
  label_project state_project
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_valid_preservation X Y label_project
  state_project by apply strong_projection_valid_preservation_weaken.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_transition_preservation_Some X Y
  label_project state_project by apply strong_projection_transition_preservation_Some_weaken.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_transition_consistency_None X Y
  label_project state_project by apply strong_projection_transition_consistency_None_weaken.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
strong_projection_initial_state_preservation X Y
  state_project done.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hvalid: strong_projection_valid_preservation X Y
  label_project state_project
Htransition_Some: strong_projection_transition_preservation_Some
  X Y label_project state_project
Htransition_None: strong_projection_transition_consistency_None
  X Y label_project state_project
Hstate: strong_projection_initial_state_preservation
  X Y state_project
Hmessage: strong_projection_valid_message_preservation
  X Y
weak_projection_valid_message_preservation X Y
  label_project state_project by apply strong_projection_valid_message_preservation_weaken.
Qed.