Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[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. From VLSM.Core Require Import VLSM VLSMProjections.

Core: Preloaded VLSMs

Given a VLSM X, we can preload it with some messages, i.e. construct an identical VLSM, except that these messages are now considered initial. In particular, we can preload X with all messages, i.e. make a copy of X in which all messages are initial. The high degree of freedom allowed by the preloaded version lets it experience everything experienced by X but also other kinds of behavior, including Byzantine behavior, which makes it a useful concept in Byzantine fault tolerance analysis.
Definition preloaded_vlsm_machine
  `(X : VLSM message) (initial : message -> Prop) : VLSMMachine X :=
{|
  initial_state_prop := @initial_state_prop _ _ X;
  initial_message_prop := fun m => @initial_message_prop _ _ X  m \/ initial m;
  s0 := @s0 _ _ X;
  transition := @transition _ _ X;
  valid := @valid _ _ X;
|}.

Definition preloaded_vlsm `(X : VLSM message) (initial : message -> Prop) : VLSM message :=
  mk_vlsm (preloaded_vlsm_machine X initial).

Definition preloaded_with_all_messages_vlsm `(X : VLSM message) : VLSM message :=
  preloaded_vlsm X (fun _ => True).

Constrained traces, states and messages

We will use the word "constrained" to denote concepts which correspond to validity in the VLSM preloaded with all messages.
Section sec_constrained_defs.

Context
  `(X : VLSM message)
  .

Definition input_constrained :=
  input_valid (preloaded_with_all_messages_vlsm X).

Definition input_constrained_transition :=
  input_valid_transition (preloaded_with_all_messages_vlsm X).

Definition input_constrained_transition_to :=
  input_valid_transition_to (preloaded_with_all_messages_vlsm X).

Definition input_constrained_transition_item :=
  input_valid_transition_item (preloaded_with_all_messages_vlsm X).

Definition finite_constrained_trace_from_to :=
  finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X).

Definition finite_constrained_trace_from :=
  finite_valid_trace_from (preloaded_with_all_messages_vlsm X).

Definition finite_constrained_trace_init_to :=
  finite_valid_trace_init_to (preloaded_with_all_messages_vlsm X).

Definition finite_constrained_trace :=
  finite_valid_trace (preloaded_with_all_messages_vlsm X).

Definition constrained_trace_from_prop :=
  valid_trace_from_prop (preloaded_with_all_messages_vlsm X).

Definition constrained_trace_prop :=
  valid_trace_prop (preloaded_with_all_messages_vlsm X).

Definition constrained_state_prop :=
  valid_state_prop (preloaded_with_all_messages_vlsm X).

Definition constrained_message_prop :=
  can_emit (preloaded_with_all_messages_vlsm X).

Definition constrained_state_message_prop :=
  valid_state_message_prop (preloaded_with_all_messages_vlsm X).

End sec_constrained_defs.

Basic properties of preloaded VLSMs

Section sec_preloaded_with_all_messages_vlsm.

Context
  `(X : VLSM message)
  .
A message which can be emitted during a protocol run of the preloaded_with_all_messages_vlsm is called a byzantine_message, because as shown by byzantine_preloaded_with_all_messages and preloaded_with_all_messages_alt_eq, byzantine traces for a VLSM are precisely the valid traces of the preloaded_with_all_messages_vlsm, hence a byzantine message is any message which a byzantine trace can_emit.
Definition byzantine_message_prop (m : message) : Prop :=
  can_emit (preloaded_with_all_messages_vlsm X) m.

Definition byzantine_message : Type :=
  {m : message | byzantine_message_prop m}.

message: Type
X: VLSM message

om : option message, constrained_state_message_prop X (`(vs0 X)) om
message: Type
X: VLSM message

om : option message, constrained_state_message_prop X (`(vs0 X)) om
by intros; apply valid_initial_state_message; [apply proj2_sig | destruct om]; cbn; [right |]. Qed.
message: Type
X: VLSM message

(s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s om
message: Type
X: VLSM message

(s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s om
message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X om

constrained_state_message_prop X s om
message: Type
X: VLSM message
s: state X
_om: option message
H: valid_state_message_prop X s _om
_s: state X
om: option message
H0: valid_state_message_prop X _s om
l: label X
Hv: valid l (s, om)
s': state X
om': option message
Ht: transition l (s, om) = (s', om')
IHvalid_state_message_prop1: constrained_state_message_prop X s _om
IHvalid_state_message_prop2: constrained_state_message_prop X _s om
constrained_state_message_prop X s' om'
message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X om

constrained_state_message_prop X s om
message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X om

option_initial_message_prop (preloaded_vlsm_machine X (λ _ : message, True)) om
by destruct om; cbn; [right |].
message: Type
X: VLSM message
s: state X
_om: option message
H: valid_state_message_prop X s _om
_s: state X
om: option message
H0: valid_state_message_prop X _s om
l: label X
Hv: valid l (s, om)
s': state X
om': option message
Ht: transition l (s, om) = (s', om')
IHvalid_state_message_prop1: constrained_state_message_prop X s _om
IHvalid_state_message_prop2: constrained_state_message_prop X _s om

constrained_state_message_prop X s' om'
by eapply valid_generated_state_message; cycle 2. Qed.
message: Type
X: VLSM message

s : state X, valid_state_prop X s → constrained_state_prop X s
message: Type
X: VLSM message

s : state X, valid_state_prop X s → constrained_state_prop X s
message: Type
X: VLSM message
s: state X
om: option message
Hvsp: valid_state_message_prop X s om

constrained_state_prop X s
message: Type
X: VLSM message
s: state X
om: option message
Hvsp: valid_state_message_prop X s om

valid_state_message_prop (preloaded_with_all_messages_vlsm X) s om
by apply preloaded_with_all_messages_valid_state_message_preservation. Qed.
message: Type
X: VLSM message

om : option message, option_valid_message_prop (preloaded_with_all_messages_vlsm X) om
message: Type
X: VLSM message

om : option message, option_valid_message_prop (preloaded_with_all_messages_vlsm X) om
by eexists; apply preloaded_with_all_messages_message_valid_initial_state_message. Qed.
message: Type
X: VLSM message

(s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s om
message: Type
X: VLSM message

(s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s om
message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X om

constrained_state_message_prop X s om
message: Type
X: VLSM message
s: state X
_om: option message
H: valid_state_message_prop X s _om
_s: state X
om: option message
H0: valid_state_message_prop X _s om
l: label X
Hv: valid l (s, om)
s': state X
om': option message
Ht: transition l (s, om) = (s', om')
IHvalid_state_message_prop1: constrained_state_message_prop X s _om
IHvalid_state_message_prop2: constrained_state_message_prop X _s om
constrained_state_message_prop X s' om'
message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X om

constrained_state_message_prop X s om
message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X om

option_initial_message_prop (preloaded_with_all_messages_vlsm X) om
by destruct om; cbn; [right |].
message: Type
X: VLSM message
s: state X
_om: option message
H: valid_state_message_prop X s _om
_s: state X
om: option message
H0: valid_state_message_prop X _s om
l: label X
Hv: valid l (s, om)
s': state X
om': option message
Ht: transition l (s, om) = (s', om')
IHvalid_state_message_prop1: constrained_state_message_prop X s _om
IHvalid_state_message_prop2: constrained_state_message_prop X _s om

constrained_state_message_prop X s' om'
by eapply valid_generated_state_message; cycle 2. Qed.
message: Type
X: VLSM message

(l : label X) (s : state X) (om : option message) (s' : state X) (om' : option message), input_valid_transition X l (s, om) (s', om') → input_constrained_transition X l (s, om) (s', om')
message: Type
X: VLSM message

(l : label X) (s : state X) (om : option message) (s' : state X) (om' : option message), input_valid_transition X l (s, om) (s', om') → input_constrained_transition X l (s, om) (s', om')
message: Type
X: VLSM message

(l : label X) (s : state X) (om : option message) (s' : state X) (om' : option message), (valid_state_prop X s ∧ option_valid_message_prop X om ∧ valid l (s, om)) ∧ transition l (s, om) = (s', om') → (valid_state_prop (preloaded_with_all_messages_vlsm X) s ∧ option_valid_message_prop (preloaded_with_all_messages_vlsm X) om ∧ valid l (s, om)) ∧ transition l (s, om) = (s', om')
message: Type
X: VLSM message
l: label X
s: state X
om: option message
s': state X
om', _om: option message
valid_s: valid_state_message_prop X s _om
Hvalid: valid l (s, om)
Htrans: transition l (s, om) = (s', om')

(valid_state_prop (preloaded_with_all_messages_vlsm X) s ∧ option_valid_message_prop (preloaded_with_all_messages_vlsm X) om ∧ valid l (s, om)) ∧ transition l (s, om) = (s', om')
message: Type
X: VLSM message
l: label X
s: state X
om: option message
s': state X
om', _om: option message
valid_s: valid_state_message_prop X s _om
Hvalid: valid l (s, om)
Htrans: transition l (s, om) = (s', om')

valid_state_prop (preloaded_with_all_messages_vlsm X) s
message: Type
X: VLSM message
l: label X
s: state X
om: option message
s': state X
om', _om: option message
valid_s: valid_state_message_prop X s _om
Hvalid: valid l (s, om)
Htrans: transition l (s, om) = (s', om')
option_valid_message_prop (preloaded_with_all_messages_vlsm X) om
message: Type
X: VLSM message
l: label X
s: state X
om: option message
s': state X
om', _om: option message
valid_s: valid_state_message_prop X s _om
Hvalid: valid l (s, om)
Htrans: transition l (s, om) = (s', om')

valid_state_prop (preloaded_with_all_messages_vlsm X) s
by exists _om; apply preloaded_weaken_valid_state_message_prop.
message: Type
X: VLSM message
l: label X
s: state X
om: option message
s': state X
om', _om: option message
valid_s: valid_state_message_prop X s _om
Hvalid: valid l (s, om)
Htrans: transition l (s, om) = (s', om')

option_valid_message_prop (preloaded_with_all_messages_vlsm X) om
by apply any_message_is_valid_in_preloaded. Qed.
message: Type
X: VLSM message

(s : state X) (tr : list transition_item), finite_valid_trace_from X s tr → finite_constrained_trace_from X s tr
message: Type
X: VLSM message

(s : state X) (tr : list transition_item), finite_valid_trace_from X s tr → finite_constrained_trace_from X s tr
message: Type
X: VLSM message
s: state X
H: valid_state_prop X s

finite_constrained_trace_from X s []
message: Type
X: VLSM message
s: state X
tr: list transition_item
H: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: input_valid_transition X l (finite_trace_last s tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHfinite_valid_trace_from: finite_constrained_trace_from X s tr
finite_constrained_trace_from X s (tr ++ [x])
message: Type
X: VLSM message
s: state X
H: valid_state_prop X s

finite_constrained_trace_from X s []
message: Type
X: VLSM message
s: state X
H: valid_state_prop X s

valid_state_prop (preloaded_with_all_messages_vlsm X) s
message: Type
X: VLSM message
s: state X
om: option message
H: valid_state_message_prop X s om

valid_state_prop (preloaded_with_all_messages_vlsm X) s
message: Type
X: VLSM message
s: state X
om: option message
H: valid_state_message_prop X s om

valid_state_message_prop (preloaded_with_all_messages_vlsm X) s om
by apply preloaded_weaken_valid_state_message_prop.
message: Type
X: VLSM message
s: state X
tr: list transition_item
H: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: input_valid_transition X l (finite_trace_last s tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHfinite_valid_trace_from: finite_constrained_trace_from X s tr

finite_constrained_trace_from X s (tr ++ [x])
message: Type
X: VLSM message
s: state X
tr: list transition_item
H: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: input_valid_transition X l (finite_trace_last s tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHfinite_valid_trace_from: finite_constrained_trace_from X s tr

finite_valid_trace_from (preloaded_with_all_messages_vlsm X) s tr ∧ finite_valid_trace_from (preloaded_with_all_messages_vlsm X) (finite_trace_last s tr) [x]
message: Type
X: VLSM message
s: state X
tr: list transition_item
H: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: input_valid_transition X l (finite_trace_last s tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHfinite_valid_trace_from: finite_constrained_trace_from X s tr

finite_valid_trace_from (preloaded_with_all_messages_vlsm X) (finite_trace_last s tr) [x]
message: Type
X: VLSM message
s: state X
tr: list transition_item
H: finite_valid_trace_from X s tr
sf: state X
iom, oom: option message
l: label X
Hx: input_valid_transition X l (finite_trace_last s tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHfinite_valid_trace_from: finite_constrained_trace_from X s tr

input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last s tr, iom) (sf, oom)
by apply preloaded_weaken_input_valid_transition. Qed.
message: Type
X: VLSM message

(s f : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item), finite_constrained_trace_from_to X s f tr → valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr → finite_valid_trace_from_to X s f tr
message: Type
X: VLSM message

(s f : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item), finite_constrained_trace_from_to X s f tr → valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr → finite_valid_trace_from_to X s f tr
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_constrained_trace_from_to X s f tr

valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr → finite_valid_trace_from_to X s f tr
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl

valid_state_prop X s' → Forall (λ item : transition_item, option_valid_message_prop X (input item)) ({| l := l; input := iom; destination := s; output := oom |} :: tl) → finite_valid_trace_from_to X s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl

finite_valid_trace_from_to X s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl

input_valid_transition X l (s', iom) (s, oom) → finite_valid_trace_from_to X s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl
input_valid_transition X l (s', iom) (s, oom)
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl

input_valid_transition X l (s', iom) (s, oom) → finite_valid_trace_from_to X s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl
H1: input_valid_transition X l (s', iom) (s, oom)

finite_valid_trace_from_to X s f tl
by apply IHHtr; [eapply input_valid_transition_destination |].
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl

input_valid_transition X l (s', iom) (s, oom)
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (s', iom)
Ht: transition l (s', iom) = (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl

input_valid_transition X l (s', iom) (s, oom)
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (s', iom)
Ht: transition l (s', iom) = (s, oom)
IHHtr: valid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl → finite_valid_trace_from_to X s f tl
Hs: valid_state_prop X s'
H: option_valid_message_prop X (input {| l := l; input := iom; destination := s; output := oom |})
H0: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tl

option_valid_message_prop X iom
by destruct iom; [| apply option_valid_message_None]. Qed.
message: Type
X: VLSM message

(s f : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item), finite_constrained_trace_init_to X s f tr → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr → finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message

(s f : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item), finite_constrained_trace_init_to X s f tr → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr → finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
Hinit: initial_state_prop s
Hobs: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr

finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
Hinit: initial_state_prop s
Hobs: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr

finite_valid_trace_from_to X s f tr
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
Hinit: initial_state_prop s
Hobs: Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr

valid_state_prop X s
by apply initial_state_is_valid. Qed. End sec_preloaded_with_all_messages_vlsm. Section sec_preloaded_valid_transition. Context `(X : VLSM message) .
message: Type
X: VLSM message

(l : label X) (s1 : state X) (iom : option message) (s2 : state X) (oom : option message), valid_transition X l s1 iom s2 oom ↔ valid_transition (preloaded_with_all_messages_vlsm X) l s1 iom s2 oom
message: Type
X: VLSM message

(l : label X) (s1 : state X) (iom : option message) (s2 : state X) (oom : option message), valid_transition X l s1 iom s2 oom ↔ valid_transition (preloaded_with_all_messages_vlsm X) l s1 iom s2 oom
by firstorder. Qed.
message: Type
X: VLSM message

s1 s2 : state X, valid_transition_next X s1 s2 ↔ valid_transition_next (preloaded_with_all_messages_vlsm X) s1 s2
message: Type
X: VLSM message

s1 s2 : state X, valid_transition_next X s1 s2 ↔ valid_transition_next (preloaded_with_all_messages_vlsm X) s1 s2
by split; intros []; econstructor; apply valid_transition_preloaded_iff. Qed. End sec_preloaded_valid_transition. Section sec_preloaded_vlsm_total_projection. Context {message : Type} (X Y : VLSM message) (P Q : message -> Prop) (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 : weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) .
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

(sX : state (preloaded_with_all_messages_vlsm X)) (trX : list transition_item), finite_valid_trace_from (preloaded_with_all_messages_vlsm X) sX trX → state_project (finite_trace_last sX trX) = finite_trace_last (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) Y label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_with_all_messages_vlsm X) is tr

state_project (finite_trace_last is tr) = finite_trace_last (state_project is) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) Y label_project state_project tr)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_with_all_messages_vlsm X) s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm 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 (preloaded_with_all_messages_vlsm X) Y 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 (preloaded_with_all_messages_vlsm X) Y label_project state_project (tr ++ [x]))
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_with_all_messages_vlsm X) s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm 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 (preloaded_with_all_messages_vlsm X) Y label_project state_project tr)

state_project sf = List.last (map destination match pre_VLSM_projection_transition_item_project X Y label_project state_project x with | Some y => [y] | None => [] end) (state_project (finite_trace_last s tr))
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_with_all_messages_vlsm X) s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm 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 (preloaded_with_all_messages_vlsm X) Y label_project state_project tr)

state_project sf = List.last (map destination 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) (state_project (finite_trace_last s tr))
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_with_all_messages_vlsm X) s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm 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 (preloaded_with_all_messages_vlsm X) Y label_project state_project tr)
Hl: label_project (VLSM.l x) = None

state_project sf = state_project (finite_trace_last s tr)
by rewrite Htransition_None; [.. | apply Hx]. Qed.
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project

VLSM_projection (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project

(sX : state (preloaded_with_all_messages_vlsm X)) (trX : list transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) sX trX → finite_valid_trace (preloaded_with_all_messages_vlsm Y) (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
sX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) sX trX

finite_valid_trace (preloaded_with_all_messages_vlsm Y) (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
sX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) sX trX

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project (tr ++ [x]))
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr ++ pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr) ∧ finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr))

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr)) (pre_VLSM_projection_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr)) 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
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr)) [{| l := lY; input := iom; destination := state_project sf; output := oom |}]
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

input_valid_transition (preloaded_with_all_messages_vlsm Y) lY (state_project (finite_trace_last si tr), iom) (state_project sf, oom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

input_valid_transition (preloaded_with_all_messages_vlsm Y) lY (state_project (finite_trace_last si tr), iom) (state_project sf, oom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

option_valid_message_prop (preloaded_with_all_messages_vlsm Y) iom
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY
valid lY (state_project (finite_trace_last si tr), iom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY
transition lY (state_project (finite_trace_last si tr), iom) = (state_project sf, oom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

option_valid_message_prop (preloaded_with_all_messages_vlsm Y) iom
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
m: message
oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, Some m)
Ht: transition l (finite_trace_last si tr, Some m) = (sf, oom)
x:= {| l := l; input := Some m; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

option_valid_message_prop (preloaded_with_all_messages_vlsm Y) (Some m)
by apply any_message_is_valid_in_preloaded.
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

valid lY (state_project (finite_trace_last si tr), iom)
by eapply Hvalid.
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_project
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_with_all_messages_vlsm Y) (state_project (finite_trace_last si tr))
lY: label Y
Hl: label_project l = Some lY

transition lY (state_project (finite_trace_last si tr), iom) = (state_project sf, oom)
by eapply Htransition_Some. Qed.
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

(sX : state (preloaded_vlsm X P)) (trX : list transition_item), finite_valid_trace_from (preloaded_vlsm X P) sX trX → state_project (finite_trace_last sX trX) = finite_trace_last (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) Y label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
is: state (preloaded_vlsm X P)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_vlsm X P) is tr

state_project (finite_trace_last is tr) = finite_trace_last (state_project is) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) Y label_project state_project tr)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_vlsm X P)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_vlsm X P) s tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) 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 (preloaded_vlsm X P) Y 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 (preloaded_vlsm X P) Y label_project state_project (tr ++ [x]))
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_vlsm X P)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_vlsm X P) s tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) 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 (preloaded_vlsm X P) Y 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 (preloaded_vlsm X P) Y label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_vlsm X P)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_vlsm X P) s tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) 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 (preloaded_vlsm X P) Y label_project state_project tr)

state_project sf = List.last (map destination 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) (state_project (finite_trace_last s tr))
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
s: state (preloaded_vlsm X P)
tr: list transition_item
Htr: finite_valid_trace_from (preloaded_vlsm X P) s tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) 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 (preloaded_vlsm X P) Y label_project state_project tr)
Hl: label_project (VLSM.l x) = None

state_project sf = List.last (map destination []) (state_project (finite_trace_last s tr))
by rewrite Htransition_None; [.. | apply Hx]. Qed.
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project

VLSM_projection (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project

VLSM_projection (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project

(sX : state (preloaded_vlsm X P)) (trX : list transition_item), finite_valid_trace (preloaded_vlsm X P) sX trX → finite_valid_trace (preloaded_vlsm Y Q) (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
sX: state (preloaded_vlsm X P)
trX: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) sX trX

finite_valid_trace (preloaded_vlsm Y Q) (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
sX: state (preloaded_vlsm X P)
trX: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) sX trX

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project sX) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project (tr ++ [x]))
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr ++ pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr) ∧ finite_valid_trace_from (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr))

finite_valid_trace_from (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hx: input_valid_transition (preloaded_vlsm X P) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)

finite_valid_trace_from (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)

finite_valid_trace_from (preloaded_vlsm Y Q) (finite_trace_last (state_project si) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr)) (pre_VLSM_projection_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr)) 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
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr)) [{| l := lY; input := iom; destination := state_project sf; output := oom |}]
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY

input_valid_transition (preloaded_vlsm Y Q) lY (state_project (finite_trace_last si tr), iom) (state_project sf, oom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY

option_valid_message_prop (preloaded_vlsm Y Q) iom
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY
valid lY (state_project (finite_trace_last si tr), iom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY
transition lY (state_project (finite_trace_last si tr), iom) = (state_project sf, oom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY

option_valid_message_prop (preloaded_vlsm Y Q) iom
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
m: message
oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, Some m)
Ht: transition l (finite_trace_last si tr, Some m) = (sf, oom)
x:= {| l := l; input := Some m; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, Some m)
lY: label Y
Hl: label_project l = Some lY

option_valid_message_prop (preloaded_vlsm Y Q) (Some m)
by eapply Hmessage.
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY

valid lY (state_project (finite_trace_last si tr), iom)
by eapply Hvalid.
message: Type
X, Y: VLSM message
P, Q: message → Prop
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: weak_projection_valid_message_preservation (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
Htype: VLSM_projection_type (preloaded_vlsm X P) Y label_project state_project
si: state (preloaded_vlsm X P)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) si tr
sf: state (preloaded_vlsm X P)
iom, oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: valid_state_prop (preloaded_vlsm Y Q) (state_project (finite_trace_last si tr))
Hpv: input_valid (preloaded_vlsm X P) l (finite_trace_last si tr, iom)
lY: label Y
Hl: label_project l = Some lY

transition lY (state_project (finite_trace_last si tr), iom) = (state_project sf, oom)
by eapply Htransition_Some. Qed. End sec_preloaded_vlsm_total_projection. Section sec_preloaded_vlsm_embedding. Context {message : Type} (X Y : VLSM message) (P Q : message -> Prop) (PimpliesQ : forall m : message, P m -> Q m) (label_project : label X -> label Y) (state_project : state X -> state Y) (Hvalid : strong_embedding_valid_preservation X Y label_project state_project) (Htransition : strong_embedding_transition_preservation X Y label_project state_project) (Hstate : strong_projection_initial_state_preservation X Y state_project) (Hmessage : strong_embedding_initial_message_preservation X Y) .
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y

VLSM_embedding (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y

VLSM_embedding (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y

(sX : state (preloaded_with_all_messages_vlsm X)) (trX : list transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) sX trX → finite_valid_trace (preloaded_with_all_messages_vlsm Y) (state_project sX) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
sX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) sX trX

finite_valid_trace (preloaded_with_all_messages_vlsm Y) (state_project sX) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
sX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) sX trX

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project sX) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project (tr ++ [x]))
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (map (pre_VLSM_embedding_transition_item_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project) tr ++ map (pre_VLSM_embedding_transition_item_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project) [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (map (pre_VLSM_embedding_transition_item_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project) tr) ∧ finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project) tr)) (map (pre_VLSM_embedding_transition_item_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project) [x])
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr)) [pre_VLSM_embedding_transition_item_project X Y label_project state_project x]
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hx: input_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last si tr, iom) ( sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

input_valid_transition (preloaded_with_all_messages_vlsm Y) (label_project (VLSM.l x)) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input x) (state_project (destination x), output x)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (finite_trace_last si tr, iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

input_valid_transition (preloaded_with_all_messages_vlsm Y) (label_project (VLSM.l x)) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input x) (state_project (destination x), output x)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid (label_project l) (state_project (finite_trace_last si tr), iom)
Ht: transition l (finite_trace_last si tr, iom) = (sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

input_valid_transition (preloaded_with_all_messages_vlsm Y) (label_project (VLSM.l x)) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input x) (state_project (destination x), output x)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid (label_project l) (state_project (finite_trace_last si tr), iom)
Ht: transition (label_project l) (state_project (finite_trace_last si tr), iom) = (state_project sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

input_valid_transition (preloaded_with_all_messages_vlsm Y) (label_project (VLSM.l x)) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input x) (state_project (destination x), output x)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom)
Ht: transition (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom) = (state_project sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

input_valid_transition (preloaded_with_all_messages_vlsm Y) (label_project (VLSM.l x)) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input x) (state_project (destination x), output x)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom)
Ht: transition (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom) = (state_project sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

valid_state_prop (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr))
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom)
Ht: transition (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom) = (state_project sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)
option_valid_message_prop (preloaded_with_all_messages_vlsm Y) (input x)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom)
Ht: transition (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom) = (state_project sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

valid_state_prop (preloaded_with_all_messages_vlsm Y) (finite_trace_last (state_project si) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr))
by apply finite_valid_trace_last_pstate in IHHtrX.
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
HtrX: finite_valid_trace (preloaded_with_all_messages_vlsm X) si tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom)
Ht: transition (label_project l) (finite_trace_last (state_project si) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom) = (state_project sf, oom)
x:= {| l := l; input := iom; destination := sf; output := oom |}: transition_item
IHHtrX: finite_valid_trace_from (preloaded_with_all_messages_vlsm Y) (state_project si) (pre_VLSM_embedding_finite_trace_project (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_project tr)

option_valid_message_prop (preloaded_with_all_messages_vlsm Y) (input x)
by apply any_message_is_valid_in_preloaded. Qed.
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y

VLSM_embedding (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y

VLSM_embedding (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y

(sX : state (preloaded_vlsm X P)) (trX : list transition_item), finite_valid_trace (preloaded_vlsm X P) sX trX → finite_valid_trace (preloaded_vlsm Y Q) (state_project sX) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
sX: state (preloaded_vlsm X P)
trX: list transition_item
HtrX: finite_valid_trace (preloaded_vlsm X P) sX trX

finite_valid_trace (preloaded_vlsm Y Q) (state_project sX) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
sX: state (preloaded_vlsm X P)
trX: list transition_item
HtrX: finite_valid_trace_init_to (preloaded_vlsm X P) sX (finite_trace_last sX trX) trX

finite_valid_trace (preloaded_vlsm Y Q) (state_project sX) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
sX: state (preloaded_vlsm X P)
trX: list transition_item
HtrX: finite_valid_trace_init_to (preloaded_vlsm X P) sX (finite_trace_last sX trX) trX

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project sX) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project trX)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: input_valid_transition (preloaded_vlsm X P) l ( s, iom) (sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}]))
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: input_valid_transition (preloaded_vlsm X P) l ( s, iom) (sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (map (pre_VLSM_embedding_transition_item_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) tr ++ map (pre_VLSM_embedding_transition_item_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: input_valid_transition (preloaded_vlsm X P) l ( s, iom) (sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (map (pre_VLSM_embedding_transition_item_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) tr) ∧ finite_valid_trace_from (preloaded_vlsm Y Q) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) tr)) (map (pre_VLSM_embedding_transition_item_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: input_valid_transition (preloaded_vlsm X P) l ( s, iom) (sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

finite_valid_trace_from (preloaded_vlsm Y Q) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr)) [pre_VLSM_embedding_transition_item_project X Y label_project state_project {| l := l; input := iom; destination := sf; output := oom |}]
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: input_valid_transition (preloaded_vlsm X P) l ( s, iom) (sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

input_valid_transition (preloaded_vlsm Y Q) (label_project (VLSM.l {| l := l; input := iom; destination := sf; output := oom |})) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input {| l := l; input := iom; destination := sf; output := oom |}) (state_project (destination {| l := l; input := iom; destination := sf; output := oom |}), output {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Hv: valid l (s, iom)
Ht: transition l (s, iom) = (sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

input_valid_transition (preloaded_vlsm Y Q) (label_project (VLSM.l {| l := l; input := iom; destination := sf; output := oom |})) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input {| l := l; input := iom; destination := sf; output := oom |}) (state_project (destination {| l := l; input := iom; destination := sf; output := oom |}), output {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Hv: valid (label_project l) (state_project s, iom)
Ht: transition l (s, iom) = (sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

input_valid_transition (preloaded_vlsm Y Q) (label_project (VLSM.l {| l := l; input := iom; destination := sf; output := oom |})) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input {| l := l; input := iom; destination := sf; output := oom |}) (state_project (destination {| l := l; input := iom; destination := sf; output := oom |}), output {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_valid_trace_init_to (preloaded_vlsm X P) is s tr
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Hv: valid (label_project l) (state_project s, iom)
Ht: transition (label_project l) (state_project s, iom) = (state_project sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

input_valid_transition (preloaded_vlsm Y Q) (label_project (VLSM.l {| l := l; input := iom; destination := sf; output := oom |})) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input {| l := l; input := iom; destination := sf; output := oom |}) (state_project (destination {| l := l; input := iom; destination := sf; output := oom |}), output {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is, s: state (preloaded_vlsm X P)
tr: list transition_item
HtrX1: finite_trace_last is tr = s
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Hv: valid (label_project l) (state_project s, iom)
Ht: transition (label_project l) (state_project s, iom) = (state_project sf, oom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

input_valid_transition (preloaded_vlsm Y Q) (label_project (VLSM.l {| l := l; input := iom; destination := sf; output := oom |})) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), input {| l := l; input := iom; destination := sf; output := oom |}) (state_project (destination {| l := l; input := iom; destination := sf; output := oom |}), output {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (state_project (finite_trace_last is tr), iom) = (state_project sf, oom)
Hv: valid (label_project l) (state_project (finite_trace_last is tr), iom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

input_valid_transition (preloaded_vlsm Y Q) (label_project l) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), iom) (state_project sf, oom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

input_valid_transition (preloaded_vlsm Y Q) (label_project l) (finite_trace_last (state_project is) (map (pre_VLSM_embedding_transition_item_project X Y label_project state_project) tr), iom) (state_project sf, oom)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
iom: option message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr iom
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), iom)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

option_valid_message_prop (preloaded_vlsm Y Q) iom
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: empty_initial_message_or_final_output (preloaded_vlsm X P) iom_tr (Some m)
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

option_valid_message_prop (preloaded_vlsm Y Q) (Some m)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom: match has_last_or_null iom_tr with | inleft (existT x (x0 ↾ _)) => output x0 = Some m | inright _ => option_initial_message_prop (preloaded_vlsm X P) (Some m) end
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s iom_tr
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project iom_tr)

option_valid_message_prop (preloaded_vlsm Y Q) (Some m)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom_tr: iom_tr = []
Heqiom: option_initial_message_prop (preloaded_vlsm X P) (Some m)
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s []
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [])

option_valid_message_prop (preloaded_vlsm Y Q) (Some m)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr, iom_tr': list transition_item
iom_lst: transition_item
Heqiom_tr: iom_tr = iom_tr' ++ [iom_lst]
Heqiom: output iom_lst = Some m
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s (iom_tr' ++ [iom_lst])
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project (iom_tr' ++ [iom_lst]))
option_valid_message_prop (preloaded_vlsm Y Q) (Some m)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr: list transition_item
Heqiom_tr: iom_tr = []
Heqiom: option_initial_message_prop (preloaded_vlsm X P) (Some m)
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s []
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project [])

option_valid_message_prop (preloaded_vlsm Y Q) (Some m)
by apply option_initial_message_is_valid; destruct Heqiom; cbn; itauto.
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr, iom_tr': list transition_item
iom_lst: transition_item
Heqiom_tr: iom_tr = iom_tr' ++ [iom_lst]
Heqiom: output iom_lst = Some m
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s (iom_tr' ++ [iom_lst])
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project (iom_tr' ++ [iom_lst]))

option_valid_message_prop (preloaded_vlsm Y Q) (Some m)
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr, iom_tr': list transition_item
iom_lst: transition_item
Heqiom_tr: iom_tr = iom_tr' ++ [iom_lst]
Heqiom: output iom_lst = Some m
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s (iom_tr' ++ [iom_lst])
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project (iom_tr' ++ [iom_lst]))

trace_has_message (field_selector output) m (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project (iom_tr' ++ [iom_lst]))
message: Type
X, Y: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
label_project: label X → label Y
state_project: state X → state Y
Hvalid: strong_embedding_valid_preservation X Y label_project state_project
Htransition: strong_embedding_transition_preservation X Y label_project state_project
Hstate: strong_projection_initial_state_preservation X Y state_project
Hmessage: strong_embedding_initial_message_preservation X Y
is: state (preloaded_vlsm X P)
tr: list transition_item
m: message
iom_si, iom_s: state (preloaded_vlsm X P)
iom_tr, iom_tr': list transition_item
iom_lst: transition_item
Heqiom_tr: iom_tr = iom_tr' ++ [iom_lst]
Heqiom: output iom_lst = Some m
HtrX2: finite_valid_trace_init_to (preloaded_vlsm X P) iom_si iom_s (iom_tr' ++ [iom_lst])
sf: state (preloaded_vlsm X P)
oom: option message
l: label (preloaded_vlsm X P)
Ht: transition (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m) = (state_project sf, oom)
Hv: valid (label_project l) (finite_trace_last (state_project is) (pre_VLSM_embedding_finite_trace_project X Y label_project state_project tr), Some m)
IHHtrX1: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project is) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project tr)
IHHtrX2: finite_valid_trace_from (preloaded_vlsm Y Q) (state_project iom_si) (pre_VLSM_embedding_finite_trace_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project (iom_tr' ++ [iom_lst]))

trace_has_message (field_selector output) m (map (pre_VLSM_embedding_transition_item_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) iom_tr' ++ map (pre_VLSM_embedding_transition_item_project (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_project) [iom_lst])
by apply Exists_app; right; left. Qed. End sec_preloaded_vlsm_embedding. Section sec_preloaded_vlsm_inclusion. Context {message : Type} {T : VLSMType message} (MX MY : VLSMMachine T) (X := mk_vlsm MX) (Y := mk_vlsm MY) .
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hinitial_state: strong_incl_initial_state_preservation MX MY
Hvalid: strong_incl_valid_preservation MX MY
Htransition: strong_incl_transition_preservation MX MY

VLSM_incl (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y)
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hinitial_state: strong_incl_initial_state_preservation MX MY
Hvalid: strong_incl_valid_preservation MX MY
Htransition: strong_incl_transition_preservation MX MY

VLSM_incl (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y)
by apply VLSM_incl_embedding_iff, (basic_VLSM_embedding_preloaded X Y id id). Qed.
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
Hvalid: strong_incl_valid_preservation MX MY
Htransition: strong_incl_transition_preservation MX MY
Hstate: strong_incl_initial_state_preservation MX MY
Hmessage: strong_incl_initial_message_preservation MX MY

VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm Y Q)
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
P, Q: message → Prop
PimpliesQ: m : message, P m → Q m
Hvalid: strong_incl_valid_preservation MX MY
Htransition: strong_incl_transition_preservation MX MY
Hstate: strong_incl_initial_state_preservation MX MY
Hmessage: strong_incl_initial_message_preservation MX MY

VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm Y Q)
by apply VLSM_incl_embedding_iff, (basic_VLSM_embedding_preloaded_with X Y _ _ PimpliesQ id id). Qed. End sec_preloaded_vlsm_inclusion. Section sec_VLSM_incl_preloaded_properties. Context `(X : VLSM message) .
message: Type
X: VLSM message

P : message → Prop, VLSM_incl X (preloaded_vlsm X P)
message: Type
X: VLSM message

P : message → Prop, VLSM_incl X (preloaded_vlsm X P)
by intros; apply basic_VLSM_strong_incl; cbv; itauto. Qed.
message: Type
X: VLSM message

VLSM_incl X (preloaded_with_all_messages_vlsm X)
message: Type
X: VLSM message

VLSM_incl X (preloaded_with_all_messages_vlsm X)
by apply vlsm_incl_preloaded. Qed.
message: Type
X: VLSM message

P Q : message → Prop, ( m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m) → VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm X Q)
message: Type
X: VLSM message

P Q : message → Prop, ( m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m) → VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm X Q)
message: Type
X: VLSM message
P, Q: message → Prop
PimpliesQorValid: m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m

VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm X Q)
message: Type
X: VLSM message
P, Q: message → Prop
PimpliesQorValid: m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m

weak_incl_initial_message_preservation (preloaded_vlsm_machine X P) (preloaded_vlsm_machine X Q)
message: Type
X: VLSM message
P, Q: message → Prop
PimpliesQorValid: m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m
m: message
Him: initial_message_prop m

valid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} m
message: Type
X: VLSM message
P, Q: message → Prop
PimpliesQorValid: m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m
m: message
Hp: P m
valid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} m
message: Type
X: VLSM message
P, Q: message → Prop
PimpliesQorValid: m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m
m: message
Him: initial_message_prop m

valid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} m
by apply initial_message_is_valid; left.
message: Type
X: VLSM message
P, Q: message → Prop
PimpliesQorValid: m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m
m: message
Hp: P m

valid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} m
message: Type
X: VLSM message
P, Q: message → Prop
PimpliesQorValid: m : message, P m → Q m ∨ valid_message_prop (preloaded_vlsm X Q) m
m: message
H: Q m

valid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} m
by apply initial_message_is_valid; right. Qed.
message: Type
X: VLSM message

P Q : message → Prop, ( m : message, P m → Q m) → VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm X Q)
message: Type
X: VLSM message

P Q : message → Prop, ( m : message, P m → Q m) → VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm X Q)
by intros; apply preloaded_vlsm_incl_relaxed; itauto. Qed.
message: Type
X: VLSM message

P : message → Prop, VLSM_incl (preloaded_vlsm (preloaded_vlsm X P) P) (preloaded_vlsm X P)
message: Type
X: VLSM message

P : message → Prop, VLSM_incl (preloaded_vlsm (preloaded_vlsm X P) P) (preloaded_vlsm X P)
by intros; apply basic_VLSM_strong_incl; cbv; itauto. Qed.
message: Type
X: VLSM message

P : message → Prop, VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm (preloaded_vlsm X P) P)
message: Type
X: VLSM message

P : message → Prop, VLSM_incl (preloaded_vlsm X P) (preloaded_vlsm (preloaded_vlsm X P) P)
by intros; apply basic_VLSM_incl_preloaded_with; cbv; itauto. Qed.
message: Type
X: VLSM message

P : message → Prop, VLSM_incl (preloaded_vlsm X P) (preloaded_with_all_messages_vlsm X)
message: Type
X: VLSM message

P : message → Prop, VLSM_incl (preloaded_vlsm X P) (preloaded_with_all_messages_vlsm X)
by intros; apply preloaded_vlsm_incl. Qed.
message: Type
X: VLSM message

m : message, can_emit X m → can_emit (preloaded_with_all_messages_vlsm X) m
message: Type
X: VLSM message

m : message, can_emit X m → can_emit (preloaded_with_all_messages_vlsm X) m
message: Type
X: VLSM message
m: message
Hm: can_emit X m

can_emit (preloaded_with_all_messages_vlsm X) m
message: Type
X: VLSM message
m: message
Hm: can_emit X m

can_emit {| vlsm_type := X; vlsm_machine := X |} m
by rewrite mk_vlsm_machine. Qed.
message: Type
X: VLSM message

(from : state X) (tr : list transition_item), finite_valid_trace_from X from tr → finite_constrained_trace_from X from tr
message: Type
X: VLSM message

(from : state X) (tr : list transition_item), finite_valid_trace_from X from tr → finite_constrained_trace_from X from tr
by intros; eapply VLSM_incl_finite_valid_trace_from; [apply vlsm_incl_preloaded_with_all_messages_vlsm | destruct X]. Qed.
message: Type
X: VLSM message

(from to : state X) (tr : list transition_item), finite_valid_trace_from_to X from to tr → finite_constrained_trace_from_to X from to tr
message: Type
X: VLSM message

(from to : state X) (tr : list transition_item), finite_valid_trace_from_to X from to tr → finite_constrained_trace_from_to X from to tr
by intros; eapply VLSM_incl_finite_valid_trace_from_to; [apply vlsm_incl_preloaded_with_all_messages_vlsm | destruct X]. Qed. End sec_VLSM_incl_preloaded_properties. Section sec_VLSM_eq_preloaded_properties. Context `(X : VLSM message) .
message: Type
X: VLSM message

P Q : message → Prop, ( m : message, Q m → valid_message_prop (preloaded_vlsm X P) m) → VLSM_eq (preloaded_vlsm X (λ m : message, P m ∨ Q m)) (preloaded_vlsm X P)
message: Type
X: VLSM message

P Q : message → Prop, ( m : message, Q m → valid_message_prop (preloaded_vlsm X P) m) → VLSM_eq (preloaded_vlsm X (λ m : message, P m ∨ Q m)) (preloaded_vlsm X P)
message: Type
X: VLSM message
P, Q: message → Prop
H: m : message, Q m → valid_message_prop (preloaded_vlsm X P) m

VLSM_incl_part (preloaded_vlsm_machine X (λ m : message, P m ∨ Q m)) (preloaded_vlsm_machine X P)
message: Type
X: VLSM message
P, Q: message → Prop
H: m : message, Q m → valid_message_prop (preloaded_vlsm X P) m
VLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine X (λ m : message, P m ∨ Q m))
message: Type
X: VLSM message
P, Q: message → Prop
H: m : message, Q m → valid_message_prop (preloaded_vlsm X P) m

VLSM_incl_part (preloaded_vlsm_machine X (λ m : message, P m ∨ Q m)) (preloaded_vlsm_machine X P)
by apply preloaded_vlsm_incl_relaxed; itauto.
message: Type
X: VLSM message
P, Q: message → Prop
H: m : message, Q m → valid_message_prop (preloaded_vlsm X P) m

VLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine X (λ m : message, P m ∨ Q m))
by apply preloaded_vlsm_incl; itauto. Qed.
message: Type
X: VLSM message

P : message → Prop, VLSM_eq (preloaded_vlsm (preloaded_vlsm X P) P) (preloaded_vlsm X P)
message: Type
X: VLSM message

P : message → Prop, VLSM_eq (preloaded_vlsm (preloaded_vlsm X P) P) (preloaded_vlsm X P)
message: Type
X: VLSM message
P: message → Prop

VLSM_incl_part (preloaded_vlsm_machine (preloaded_vlsm X P) P) (preloaded_vlsm_machine X P)
message: Type
X: VLSM message
P: message → Prop
VLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine (preloaded_vlsm X P) P)
message: Type
X: VLSM message
P: message → Prop

VLSM_incl_part (preloaded_vlsm_machine (preloaded_vlsm X P) P) (preloaded_vlsm_machine X P)
by apply preloaded_vlsm_idem_l.
message: Type
X: VLSM message
P: message → Prop

VLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine (preloaded_vlsm X P) P)
by apply preloaded_vlsm_idem_r. Qed.
message: Type
X: VLSM message

P : message → Prop, ( (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m) → VLSM_eq (preloaded_with_all_messages_vlsm X) (preloaded_vlsm X P)
message: Type
X: VLSM message

P : message → Prop, ( (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m) → VLSM_eq (preloaded_with_all_messages_vlsm X) (preloaded_vlsm X P)
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m

VLSM_eq (preloaded_with_all_messages_vlsm X) (preloaded_vlsm X P)
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m

VLSM_incl_part (preloaded_vlsm_machine X (λ _ : message, True)) (preloaded_vlsm_machine X P)
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m

strong_incl_initial_state_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m
weak_incl_initial_message_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m
weak_incl_valid_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m
weak_incl_transition_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m

strong_incl_initial_state_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
by intro.
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m

weak_incl_initial_message_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
by intros l s m Hv _ _; eapply Hvalidating.
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m

weak_incl_valid_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
by intros l s om (_ & _ & ?).
message: Type
X: VLSM message
P: message → Prop
Hvalidating: (l : label (preloaded_with_all_messages_vlsm X)) (s : state (preloaded_with_all_messages_vlsm X)) (m : message), input_constrained X l (s, Some m) → valid_message_prop (preloaded_vlsm X P) m

weak_incl_transition_preservation {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ True; transition := transition; valid := valid |} {| initial_state_prop := initial_state_prop; s0 := s0 X X; initial_message_prop := λ m : message, initial_message_prop m ∨ P m; transition := transition; valid := valid |}
by intros l s om s' om' [_ Ht]. Qed.
message: Type
X: VLSM message

VLSM_eq X (preloaded_vlsm X (λ _ : message, False))
message: Type
X: VLSM message

VLSM_eq X (preloaded_vlsm X (λ _ : message, False))
by cbn; split; apply basic_VLSM_strong_incl; cbv; itauto. Qed.
message: Type
X: VLSM message

strong_embedding_initial_message_preservation X (preloaded_vlsm X (λ _ : message, False))
message: Type
X: VLSM message

strong_embedding_initial_message_preservation X (preloaded_vlsm X (λ _ : message, False))
by intros m Hm; left. Qed.
message: Type
X: VLSM message

strong_embedding_initial_message_preservation (preloaded_vlsm X (λ _ : message, False)) X
message: Type
X: VLSM message

strong_embedding_initial_message_preservation (preloaded_vlsm X (λ _ : message, False)) X
by intros m []. Qed.
message: Type
X: VLSM message

(s : state X) (om : option message), valid_state_message_prop X s om ↔ valid_state_message_prop (preloaded_vlsm X (λ _ : message, False)) s om
message: Type
X: VLSM message

(s : state X) (om : option message), valid_state_message_prop X s om ↔ valid_state_message_prop (preloaded_vlsm X (λ _ : message, False)) s om
message: Type
X: VLSM message
Heq1: VLSM_incl {| vlsm_type := X; vlsm_machine := X |} {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (λ _ : message, False) |}
Heq2: VLSM_incl {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (λ _ : message, False) |} {| vlsm_type := X; vlsm_machine := X |}

(s : state X) (om : option message), valid_state_message_prop X s om ↔ valid_state_message_prop (preloaded_vlsm X (λ _ : message, False)) s om
message: Type
X: VLSM message
T: VLSMType message
M: VLSMMachine T
Heq1: VLSM_incl_part M (preloaded_vlsm_machine {| vlsm_type := T; vlsm_machine := M |} (λ _ : message, False))
Heq2: VLSM_incl_part (preloaded_vlsm_machine {| vlsm_type := T; vlsm_machine := M |} (λ _ : message, False)) M

(s : state T) (om : option message), valid_state_message_prop {| vlsm_type := T; vlsm_machine := M |} s om ↔ valid_state_message_prop (preloaded_vlsm {| vlsm_type := T; vlsm_machine := M |} (λ _ : message, False)) s om
by split; (apply VLSM_incl_valid_state_message; [| cbv]); itauto. Qed. End sec_VLSM_eq_preloaded_properties.

Direct definitions of constrained traces, states and messages

In the above formalization, "valid" concepts are defined first, then "constrained" ones are derived from them, expressed as validity within the preloaded_with_all_messages_vlsm.
In this section we state the original mathematical definitions (as presented in the VLSM paper) and we show them equivalent to the ones defined above.
Section sec_constrained_direct_defs.

Context
  `(X : VLSM message)
  .
A sequence of constrained transitions, without any requirements on the starting state.
Inductive constrained_transitions_from_to
  : state X -> state X -> list (transition_item X) -> Prop :=
| ct_empty :
    forall (s : state X),
      constrained_transitions_from_to s s []
| ct_extend :
    forall (s s' f : state X) (om om' : option message) (l : label X) (tr : list transition_item),
      transition X l (s, om) = (s', om') ->
      valid X l (s, om) -> constrained_transitions_from_to s' f tr ->
      constrained_transitions_from_to s f (Build_transition_item l om s' om' :: tr).
A constrained state is a sequence of constrained transitions originating in an initial state.
Definition finite_constrained_trace_init_to_direct
  (s f : state X) (tr : list (transition_item X)) : Prop :=
    constrained_transitions_from_to s f tr /\ initial_state_prop X s.

message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_constrained_trace_init_to X s f tr → finite_constrained_trace_init_to_direct s f tr
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_constrained_trace_init_to X s f tr → finite_constrained_trace_init_to_direct s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
Hinit: initial_state_prop s

finite_constrained_trace_init_to_direct s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr

constrained_transitions_from_to s f tr
message: Type
X: VLSM message
s: state (preloaded_with_all_messages_vlsm X)
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s

constrained_transitions_from_to s s []
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: constrained_transitions_from_to s f tl
constrained_transitions_from_to s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)
message: Type
X: VLSM message
s: state (preloaded_with_all_messages_vlsm X)
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s

constrained_transitions_from_to s s []
by constructor.
message: Type
X: VLSM message
s, f: state (preloaded_with_all_messages_vlsm X)
tl: list transition_item
Htr: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tl
s': state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm X) l (s', iom) (s, oom)
IHHtr: constrained_transitions_from_to s f tl

constrained_transitions_from_to s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)
by constructor; [apply Ht..|]. Qed.
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_constrained_trace_init_to_direct s f tr → finite_constrained_trace_init_to X s f tr
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_constrained_trace_init_to_direct s f tr → finite_constrained_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: constrained_transitions_from_to s f tr
Hs: initial_state_prop s

finite_constrained_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: constrained_transitions_from_to s f tr
Hs: initial_state_prop s

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: constrained_transitions_from_to s f tr
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
message: Type
X: VLSM message
f: state X
Htr: constrained_transitions_from_to f f []
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) f

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) f f []
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr
finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
message: Type
X: VLSM message
f: state X
Htr: constrained_transitions_from_to f f []
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) f

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) f f []
by apply (finite_valid_trace_from_to_empty (preloaded_with_all_messages_vlsm X)).
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr

input_valid_transition (preloaded_with_all_messages_vlsm X) l (s, om) (s', om')
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr
finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s' f tr
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr

input_valid_transition (preloaded_with_all_messages_vlsm X) l (s, om) (s', om')
by repeat split; [| apply any_message_is_valid_in_preloaded | ..].
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s' f tr
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr

valid_state_prop (preloaded_with_all_messages_vlsm X) s'
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr

(l : label (preloaded_with_all_messages_vlsm X)) (som : state (preloaded_with_all_messages_vlsm X) * option message) (om' : option message), input_valid_transition (preloaded_with_all_messages_vlsm X) l som (s', om')
message: Type
X: VLSM message
f: state X
tr: list transition_item
IHtr: s : state X, valid_state_prop (preloaded_with_all_messages_vlsm X) s → constrained_transitions_from_to s f tr → finite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f tr
s: state X
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) s
s': state X
om, om': option message
l: label X
Htr: constrained_transitions_from_to s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)
H1: transition l (s, om) = (s', om')
H4: valid l (s, om)
H5: constrained_transitions_from_to s' f tr

input_valid_transition (preloaded_with_all_messages_vlsm X) l (s, om) (s', om')
by repeat split; [| apply any_message_is_valid_in_preloaded | ..]. Qed.
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_constrained_trace_init_to_direct s f tr ↔ finite_constrained_trace_init_to X s f tr
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_constrained_trace_init_to_direct s f tr ↔ finite_constrained_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item

finite_constrained_trace_init_to_direct s f tr → finite_constrained_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
finite_constrained_trace_init_to X s f tr → finite_constrained_trace_init_to_direct s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item

finite_constrained_trace_init_to_direct s f tr → finite_constrained_trace_init_to X s f tr
by apply finite_constrained_trace_init_to_direct_left_impl.
message: Type
X: VLSM message
s, f: state X
tr: list transition_item

finite_constrained_trace_init_to X s f tr → finite_constrained_trace_init_to_direct s f tr
by apply finite_constrained_trace_init_to_direct_right_impl. Qed.
A constrained state is a state reachable through a constrained trace.
Definition constrained_state_prop_direct (f : state X) : Prop :=
  exists (s : state X) (tr : list (transition_item X)),
    finite_constrained_trace_init_to_direct s f tr.

message: Type
X: VLSM message

s : state X, constrained_state_prop_direct s ↔ constrained_state_prop X s
message: Type
X: VLSM message

s : state X, constrained_state_prop_direct s ↔ constrained_state_prop X s
message: Type
X: VLSM message

s : state X, ( (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to_direct s0 s tr) ↔ constrained_state_prop X s
message: Type
X: VLSM message

s : state X, ( (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to X s0 s tr) ↔ constrained_state_prop X s
message: Type
X: VLSM message
s: state X

( (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to X s0 s tr) → constrained_state_prop X s
message: Type
X: VLSM message
s: state X
constrained_state_prop X s → (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to X s0 s tr
message: Type
X: VLSM message
s: state X

( (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to X s0 s tr) → constrained_state_prop X s
by intros (? & ? & []); eapply finite_valid_trace_from_to_last_pstate.
message: Type
X: VLSM message
s: state X

constrained_state_prop X s → (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to X s0 s tr
by intro Hs; apply valid_state_has_trace in Hs as (? & ? & ?); eexists _, _. Qed.
A constrained message is one which can be emitted by a constrained trace.
Definition constrained_message_prop_direct (m : message) : Prop :=
  exists (s f : state X) (tr : list (transition_item X)) (item : transition_item X),
    finite_constrained_trace_init_to_direct s f (tr ++ [item]) /\ output item = Some m.

message: Type
X: VLSM message

m : message, constrained_message_prop_direct m ↔ constrained_message_prop X m
message: Type
X: VLSM message

m : message, constrained_message_prop_direct m ↔ constrained_message_prop X m
message: Type
X: VLSM message
m: message

constrained_message_prop_direct m ↔ constrained_message_prop X m
message: Type
X: VLSM message
m: message

( (s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to_direct s f (tr ++ [item]) ∧ output item = Some m) ↔ can_emit (preloaded_with_all_messages_vlsm X) m
message: Type
X: VLSM message
m: message

( (s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to_direct s f (tr ++ [item]) ∧ output item = Some m) ↔ ( s : state (preloaded_with_all_messages_vlsm X), can_produce (preloaded_with_all_messages_vlsm X) s m)
message: Type
X: VLSM message
m: message

( (s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m) ↔ ( (s is : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item) (item : transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) is tr ∧ last_error tr = Some item ∧ destination item = s ∧ output item = Some m)
message: Type
X: VLSM message
m: message

( (s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m) → (s is : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item) (item : transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) is tr ∧ last_error tr = Some item ∧ destination item = s ∧ output item = Some m
message: Type
X: VLSM message
m: message
( (s is : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item) (item : transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) is tr ∧ last_error tr = Some item ∧ destination item = s ∧ output item = Some m) → (s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m
message: Type
X: VLSM message
m: message

( (s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m) → (s is : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item) (item : transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) is tr ∧ last_error tr = Some item ∧ destination item = s ∧ output item = Some m
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m

(s is : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item) (item : transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) is tr ∧ last_error tr = Some item ∧ destination item = s ∧ output item = Some m
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m

finite_valid_trace (preloaded_with_all_messages_vlsm X) is (tr ++ [item]) ∧ last_error (tr ++ [item]) = Some item ∧ destination item = s ∧ output item = Some m
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m

finite_valid_trace (preloaded_with_all_messages_vlsm X) is (tr ++ [item])
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m
last_error (tr ++ [item]) = Some item
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m
destination item = s
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m

finite_valid_trace (preloaded_with_all_messages_vlsm X) is (tr ++ [item])
by eapply valid_trace_forget_last.
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m

last_error (tr ++ [item]) = Some item
by apply last_error_is_last.
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_constrained_trace_init_to X is s (tr ++ [item])
Hm: output item = Some m

destination item = s
message: Type
X: VLSM message
m: message
is, s: state X
tr: list transition_item
item: transition_item
Htr: finite_trace_last is (tr ++ [item]) = s
Hm: output item = Some m

destination item = s
by erewrite <- finite_trace_last_is_last.
message: Type
X: VLSM message
m: message

( (s is : state (preloaded_with_all_messages_vlsm X)) (tr : list transition_item) (item : transition_item), finite_valid_trace (preloaded_with_all_messages_vlsm X) is tr ∧ last_error tr = Some item ∧ destination item = s ∧ output item = Some m) → (s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m
message: Type
X: VLSM message
m: message
s, is: state (preloaded_with_all_messages_vlsm X)
tr': list transition_item
item: transition_item
Htr: finite_valid_trace (preloaded_with_all_messages_vlsm X) is tr'
Hlast: last_error tr' = Some item
Hs: destination item = s
Hm: output item = Some m

(s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m
message: Type
X: VLSM message
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
tr: list transition_item
item_: transition_item
Htr: finite_valid_trace (preloaded_with_all_messages_vlsm X) is (tr ++ [item_])
Hlast: last_error (tr ++ [item_]) = Some item
Hm: output item = Some m

(s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m
message: Type
X: VLSM message
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
tr: list transition_item
Htr: finite_valid_trace (preloaded_with_all_messages_vlsm X) is (tr ++ [item])
Hm: output item = Some m

(s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m
message: Type
X: VLSM message
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
tr: list transition_item
Htr: finite_valid_trace_init_to (preloaded_with_all_messages_vlsm X) is (finite_trace_last is (tr ++ [item])) (tr ++ [item])
Hm: output item = Some m

(s f : state X) (tr : list transition_item) (item : transition_item), finite_constrained_trace_init_to X s f (tr ++ [item]) ∧ output item = Some m
by eexists _, _, _, _. Qed.

Definitions of valid traces, messages, and states based on constrained ones

Here we state the original mathematical definitions (as presented in the VLSM paper) for valid traces, states, and messages, deriving them from the "constrained" notions, and we show them equivalent to the ones defined in the VLSM module.
A valid trace is a constrained trace whose inputs are all valid messages; a valid message is either an initial message or an output of a valid trace.
Inductive finite_valid_trace_init_to_from_constrained
  : state X -> state X -> list (transition_item X) -> Prop :=
| fvtit_def :
    forall (s f : state X) (tr : list (transition_item X)),
      finite_constrained_trace_init_to_direct s f tr ->
      (forall item, item ∈ tr -> option_valid_message_prop_from_constrained (input item)) ->
      finite_valid_trace_init_to_from_constrained s f tr

with option_valid_message_prop_from_constrained : option message -> Prop :=
| ovmp_def_initial :
    forall (om : option message),
      option_initial_message_prop X om ->
      option_valid_message_prop_from_constrained om
| ovmp_def_emit :
    forall (s f : state X) (tr : list (transition_item X)),
      finite_valid_trace_init_to_from_constrained s f tr ->
      forall (item : transition_item X), item ∈ tr ->
      option_valid_message_prop_from_constrained (output item).

message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_valid_trace_init_to X s f tr → finite_valid_trace_init_to_from_constrained s f tr
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_valid_trace_init_to X s f tr → finite_valid_trace_init_to_from_constrained s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X s f tr

finite_valid_trace_init_to_from_constrained s f tr
message: Type
X: VLSM message
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_init_to_from_constrained is s tr
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr

finite_valid_trace_init_to_from_constrained is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
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_init_to_from_constrained is s tr
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr

finite_constrained_trace_init_to_direct is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
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_init_to_from_constrained is s tr
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr
item : transition_item, item ∈ tr ++ [{| l := l; input := iom; destination := sf; output := oom |}] → option_valid_message_prop_from_constrained (input item)
message: Type
X: VLSM message
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_init_to_from_constrained is s tr
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr

finite_constrained_trace_init_to_direct is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)

finite_constrained_trace_init_to_direct is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom: option message
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)

finite_constrained_trace_init_to X is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
T: VLSMType message
M: VLSMMachine T
is, s: state {| vlsm_type := T; vlsm_machine := M |}
tr: list transition_item
Htr1: finite_valid_trace_init_to {| vlsm_type := T; vlsm_machine := M |} is s tr
iom: option message
sf: state {| vlsm_type := T; vlsm_machine := M |}
oom: option message
l: label {| vlsm_type := T; vlsm_machine := M |}
Ht: input_valid_transition {| vlsm_type := T; vlsm_machine := M |} l (s, iom) (sf, oom)

finite_constrained_trace_init_to {| vlsm_type := T; vlsm_machine := M |} is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
T: VLSMType message
M: VLSMMachine T
is, s: state {| vlsm_type := T; vlsm_machine := M |}
tr: list transition_item
Htr1: finite_valid_trace_init_to {| vlsm_type := T; vlsm_machine := M |} is s tr
iom: option message
sf: state {| vlsm_type := T; vlsm_machine := M |}
oom: option message
l: label {| vlsm_type := T; vlsm_machine := M |}
Ht: input_valid_transition {| vlsm_type := T; vlsm_machine := M |} l (s, iom) (sf, oom)

finite_valid_trace_init_to {| vlsm_type := {| vlsm_type := T; vlsm_machine := M |}; vlsm_machine := M |} is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
T: VLSMType message
M: VLSMMachine T
is, s: state {| vlsm_type := T; vlsm_machine := M |}
tr: list transition_item
Htr1: finite_valid_trace_from_to {| vlsm_type := T; vlsm_machine := M |} is s tr
Hinit: initial_state_prop is
iom: option message
sf: state {| vlsm_type := T; vlsm_machine := M |}
oom: option message
l: label {| vlsm_type := T; vlsm_machine := M |}
Ht: input_valid_transition {| vlsm_type := T; vlsm_machine := M |} l (s, iom) (sf, oom)

finite_valid_trace_init_to {| vlsm_type := {| vlsm_type := T; vlsm_machine := M |}; vlsm_machine := M |} is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
T: VLSMType message
M: VLSMMachine T
is, s: state {| vlsm_type := T; vlsm_machine := M |}
tr: list transition_item
Htr1: finite_valid_trace_from_to {| vlsm_type := T; vlsm_machine := M |} is s tr
Hinit: initial_state_prop is
iom: option message
sf: state {| vlsm_type := T; vlsm_machine := M |}
oom: option message
l: label {| vlsm_type := T; vlsm_machine := M |}
Ht: input_valid_transition {| vlsm_type := T; vlsm_machine := M |} l (s, iom) (sf, oom)

finite_valid_trace_from_to {| vlsm_type := {| vlsm_type := T; vlsm_machine := M |}; vlsm_machine := M |} is sf (tr ++ [{| l := l; input := iom; destination := sf; output := oom |}])
message: Type
X: VLSM message
T: VLSMType message
M: VLSMMachine T
is, s: state {| vlsm_type := T; vlsm_machine := M |}
tr: list transition_item
Htr1: finite_valid_trace_from_to {| vlsm_type := T; vlsm_machine := M |} is s tr
Hinit: initial_state_prop is
iom: option message
sf: state {| vlsm_type := T; vlsm_machine := M |}
oom: option message
l: label {| vlsm_type := T; vlsm_machine := M |}
Ht: input_valid_transition {| vlsm_type := T; vlsm_machine := M |} l (s, iom) (sf, oom)

finite_valid_trace_from_to {| vlsm_type := T; vlsm_machine := M |} s sf [{| l := l; input := iom; destination := sf; output := oom |}]
by apply finite_valid_trace_from_to_singleton.
message: Type
X: VLSM message
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_init_to_from_constrained is s tr
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr

item : transition_item, item ∈ tr ++ [{| l := l; input := iom; destination := sf; output := oom |}] → option_valid_message_prop_from_constrained (input item)
message: Type
X: VLSM message
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)
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr
IHoutput: item : transition_item, item ∈ tr → option_valid_message_prop_from_constrained (input item)

item : transition_item, item ∈ tr ++ [{| l := l; input := iom; destination := sf; output := oom |}] → option_valid_message_prop_from_constrained (input item)
message: Type
X: VLSM message
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)
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr
IHoutput: item : transition_item, item ∈ tr → option_valid_message_prop_from_constrained (input item)
item: transition_item

item ∈ tr ++ [{| l := l; input := iom; destination := sf; output := oom |}] → option_valid_message_prop_from_constrained (input item)
message: Type
X: VLSM message
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)
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr
IHoutput: item : transition_item, item ∈ tr → option_valid_message_prop_from_constrained (input item)
item: transition_item

item ∈ tr ∨ item = {| l := l; input := iom; destination := sf; output := oom |} → option_valid_message_prop_from_constrained (input item)
message: Type
X: VLSM message
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)
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr
IHoutput: item : transition_item, item ∈ tr → option_valid_message_prop_from_constrained (input item)

option_valid_message_prop_from_constrained (input {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X: VLSM message
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: match has_last_or_null iom_tr with | inleft (existT x (x0 ↾ _)) => output x0 = iom | inright _ => option_initial_message_prop X iom end
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)
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s iom_tr
IHoutput: item : transition_item, item ∈ tr → option_valid_message_prop_from_constrained (input item)

option_valid_message_prop_from_constrained (input {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X: VLSM message
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, iom_tr': list transition_item
item: transition_item
Heq: iom_tr = iom_tr' ++ [item]
Heqiom: output item = iom
Htr2: finite_valid_trace_init_to X iom_si iom_s (iom_tr' ++ [item])
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s (iom_tr' ++ [item])
IHoutput: item : transition_item, item ∈ tr → option_valid_message_prop_from_constrained (input item)

option_valid_message_prop_from_constrained (input {| l := l; input := iom; destination := sf; output := oom |})
message: Type
X: VLSM message
is, s: state X
tr: list transition_item
Htr1: finite_valid_trace_init_to X is s tr
iom_si, iom_s: state X
iom_tr, iom_tr': list transition_item
item: transition_item
Heq: iom_tr = iom_tr' ++ [item]
Htr2: finite_valid_trace_init_to X iom_si iom_s (iom_tr' ++ [item])
sf: state X
oom: option message
l: label X
Ht: input_valid_transition X l ( s, output item) (sf, oom)
IHHtr2: finite_valid_trace_init_to_from_constrained iom_si iom_s (iom_tr' ++ [item])
IHoutput: item : transition_item, item ∈ tr → option_valid_message_prop_from_constrained (input item)

item ∈ iom_tr' ++ [item]
by rewrite elem_of_app, elem_of_list_singleton; right. Qed.
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om

(s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om

(s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om

(s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
s, f: state X
tr: list transition_item
s0, f0: state X
tr0: list transition_item
Htrc: constrained_transitions_from_to s0 f0 tr0
Hinit: initial_state_prop s0
Hmsgs: item : transition_item, item ∈ tr0 → option_valid_message_prop_from_constrained (input item)

finite_valid_trace_init_to X s0 f0 tr0
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
s, f: state X
tr: list transition_item
s0, f0: state X
tr0: list transition_item
Htrc: constrained_transitions_from_to s0 f0 tr0
Hinit: initial_state_prop s0
Hmsgs: item : transition_item, item ∈ tr0 → option_valid_message_prop_from_constrained (input item)

Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr0
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
s, f: state X
tr: list transition_item
s0, f0: state X
tr0: list transition_item
Htrc: constrained_transitions_from_to s0 f0 tr0
Hinit: initial_state_prop s0
Hmsgs: item : transition_item, item ∈ tr0 → option_valid_message_prop_from_constrained (input item)
x: transition_item
H: x ∈ tr0

option_valid_message_prop X (input x)
by apply option_valid_message_prop_from_constrained_left_impl, Hmsgs.
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om

om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
om: option message
s, f: state X
tr: list transition_item
Hemit: finite_valid_trace_init_to_from_constrained s f tr
item: transition_item
Hitem: item ∈ tr

option_valid_message_prop X (output item)
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
om: option message
s, f: state X
tr: list transition_item
Hemit: finite_valid_trace_init_to_from_constrained s f tr
item: transition_item
Hitem: item ∈ tr
m: message
Houtput: output item = Some m

option_valid_message_prop X (Some m)
message: Type
X: VLSM message
finite_valid_trace_init_to_from_constrained_left_impl: (s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
option_valid_message_prop_from_constrained_left_impl: om : option message, option_valid_message_prop_from_constrained om → option_valid_message_prop X om
om: option message
s, f: state X
tr: list transition_item
Hemit: finite_valid_trace_init_to_from_constrained s f tr
item: transition_item
Hitem: item ∈ tr
m: message
Houtput: output item = Some m

finite_valid_trace_from X ?is tr
by eapply valid_trace_forget_last, finite_valid_trace_init_to_from_constrained_left_impl. Qed.
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr ↔ finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message

(s f : state X) (tr : list transition_item), finite_valid_trace_init_to_from_constrained s f tr ↔ finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item

finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item
finite_valid_trace_init_to X s f tr → finite_valid_trace_init_to_from_constrained s f tr
message: Type
X: VLSM message
s, f: state X
tr: list transition_item

finite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f tr
by apply finite_valid_trace_init_to_from_constrained_left_impl.
message: Type
X: VLSM message
s, f: state X
tr: list transition_item

finite_valid_trace_init_to X s f tr → finite_valid_trace_init_to_from_constrained s f tr
by apply finite_valid_trace_init_to_from_constrained_right_impl. Qed.
message: Type
X: VLSM message

om : option message, option_valid_message_prop X om → option_valid_message_prop_from_constrained om
message: Type
X: VLSM message

om : option message, option_valid_message_prop X om → option_valid_message_prop_from_constrained om
message: Type
X: VLSM message
m: message
Hm: option_valid_message_prop X (Some m)

option_valid_message_prop_from_constrained (Some m)
message: Type
X: VLSM message
m: message
Hm: can_emit X m

option_valid_message_prop_from_constrained (Some m)
message: Type
X: VLSM message
m: message
is: state X
tr: list transition_item
item: transition_item
Htr: finite_valid_trace X is (tr ++ [item])

option_valid_message_prop_from_constrained (output item)
message: Type
X: VLSM message
m: message
is: state X
tr: list transition_item
item: transition_item
Htr: finite_valid_trace_init_to_from_constrained is (finite_trace_last is (tr ++ [item])) (tr ++ [item])

option_valid_message_prop_from_constrained (output item)
message: Type
X: VLSM message
m: message
is: state X
tr: list transition_item
item: transition_item
Htr: finite_valid_trace_init_to_from_constrained is (finite_trace_last is (tr ++ [item])) (tr ++ [item])

item ∈ tr ++ [item]
by rewrite elem_of_app, elem_of_list_singleton; right. Qed.
message: Type
X: VLSM message

om : option message, option_valid_message_prop_from_constrained om ↔ option_valid_message_prop X om
message: Type
X: VLSM message

om : option message, option_valid_message_prop_from_constrained om ↔ option_valid_message_prop X om
message: Type
X: VLSM message
om: option message

option_valid_message_prop_from_constrained om → option_valid_message_prop X om
message: Type
X: VLSM message
om: option message
option_valid_message_prop X om → option_valid_message_prop_from_constrained om
message: Type
X: VLSM message
om: option message

option_valid_message_prop_from_constrained om → option_valid_message_prop X om
by apply option_valid_message_prop_from_constrained_left_impl.
message: Type
X: VLSM message
om: option message

option_valid_message_prop X om → option_valid_message_prop_from_constrained om
by apply option_valid_message_prop_from_constrained_right_impl. Qed.
A valid state is a state reachable through a valid trace.
Definition valid_state_prop_from_constrained (s : state X) : Prop :=
  exists (is : state X) (tr : list (transition_item X)),
    finite_valid_trace_init_to_from_constrained is s tr.

message: Type
X: VLSM message

s : state X, valid_state_prop_from_constrained s → valid_state_prop X s
message: Type
X: VLSM message

s : state X, valid_state_prop_from_constrained s → valid_state_prop X s
message: Type
X: VLSM message
s, is: state X
tr: list transition_item
Htr: finite_valid_trace_init_to_from_constrained is s tr

valid_state_prop X s
by apply finite_valid_trace_init_to_from_constrained_equiv, valid_trace_last_pstate in Htr. Qed.
message: Type
X: VLSM message

s : state X, valid_state_prop X s → valid_state_prop_from_constrained s
message: Type
X: VLSM message

s : state X, valid_state_prop X s → valid_state_prop_from_constrained s
message: Type
X: VLSM message
s: state X
Hs: valid_state_prop X s

valid_state_prop_from_constrained s
message: Type
X: VLSM message
s, is: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X is s tr

valid_state_prop_from_constrained s
by exists is, tr; apply finite_valid_trace_init_to_from_constrained_equiv. Qed.
message: Type
X: VLSM message

s : state X, valid_state_prop_from_constrained s ↔ valid_state_prop X s
message: Type
X: VLSM message

s : state X, valid_state_prop_from_constrained s ↔ valid_state_prop X s
message: Type
X: VLSM message
s: state X

valid_state_prop_from_constrained s → valid_state_prop X s
message: Type
X: VLSM message
s: state X
valid_state_prop X s → valid_state_prop_from_constrained s
message: Type
X: VLSM message
s: state X

valid_state_prop_from_constrained s → valid_state_prop X s
by apply valid_state_prop_from_constrained_left_impl.
message: Type
X: VLSM message
s: state X

valid_state_prop X s → valid_state_prop_from_constrained s
by apply valid_state_prop_from_constrained_right_impl. Qed. End sec_constrained_direct_defs.
message: Type
X: VLSM message

VLSM_eq X (preloaded_vlsm X (valid_message_prop X))
message: Type
X: VLSM message

VLSM_eq X (preloaded_vlsm X (valid_message_prop X))
message: Type
X: VLSM message

VLSM_incl {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} {| vlsm_type := X; vlsm_machine := X |}
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
m: message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, Some m)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
HmX: initial_message_prop m

valid_message_prop {| vlsm_type := X; vlsm_machine := X |} m
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
om: option message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, om)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
HomY: option_valid_message_prop {| vlsm_type := X; vlsm_machine := X |} om
valid l (s, om)
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
om: option message
s': state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
om': option message
H: input_valid_transition {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, om) (s', om')
transition l (s, om) = (s', om')
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
m: message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, Some m)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
HmX: initial_message_prop m

valid_message_prop {| vlsm_type := X; vlsm_machine := X |} m
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
m: message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, Some m)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
Hinit: initial_message_prop m

valid_message_prop {| vlsm_type := X; vlsm_machine := X |} m
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
m: message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, Some m)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
HmX: valid_message_prop X m
valid_message_prop {| vlsm_type := X; vlsm_machine := X |} m
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
m: message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, Some m)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
Hinit: initial_message_prop m

valid_message_prop {| vlsm_type := X; vlsm_machine := X |} m
by apply initial_message_is_valid.
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
m: message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, Some m)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
HmX: valid_message_prop X m

valid_message_prop {| vlsm_type := X; vlsm_machine := X |} m
by destruct X.
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
om: option message
Hv: input_valid {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, om)
HsY: valid_state_prop {| vlsm_type := X; vlsm_machine := X |} (id s)
HomY: option_valid_message_prop {| vlsm_type := X; vlsm_machine := X |} om

valid l (s, om)
by apply Hv.
message: Type
X: VLSM message
l: label {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
s: state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
om: option message
s': state {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |}
om': option message
H: input_valid_transition {| vlsm_type := X; vlsm_machine := preloaded_vlsm X (valid_message_prop X) |} l (s, om) (s', om')

transition l (s, om) = (s', om')
by apply H. Qed.