From stdpp Require Import prelude. From VLSM.Lib Require Import Preamble ListExtras. From VLSM.Core Require Import VLSM VLSMProjections.
Core: Preloaded VLSMs
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
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.
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)) omby intros; apply valid_initial_state_message; [apply proj2_sig | destruct om]; cbn; [right |]. Qed.message: Type
X: VLSM message∀ om : option message, constrained_state_message_prop X (`(vs0 X)) ommessage: Type
X: VLSM message∀ (s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s ommessage: Type
X: VLSM message∀ (s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s ommessage: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X omconstrained_state_message_prop X s ommessage: 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 omconstrained_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 omconstrained_state_message_prop X s omby destruct om; cbn; [right |].message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X omoption_initial_message_prop (preloaded_vlsm_machine X (λ _ : message, True)) omby eapply valid_generated_state_message; cycle 2. Qed.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 omconstrained_state_message_prop X s' om'message: Type
X: VLSM message∀ s : state X, valid_state_prop X s → constrained_state_prop X smessage: Type
X: VLSM message∀ s : state X, valid_state_prop X s → constrained_state_prop X smessage: Type
X: VLSM message
s: state X
om: option message
Hvsp: valid_state_message_prop X s omconstrained_state_prop X sby apply preloaded_with_all_messages_valid_state_message_preservation. Qed.message: Type
X: VLSM message
s: state X
om: option message
Hvsp: valid_state_message_prop X s omvalid_state_message_prop (preloaded_with_all_messages_vlsm X) s ommessage: Type
X: VLSM message∀ om : option message, option_valid_message_prop (preloaded_with_all_messages_vlsm X) omby eexists; apply preloaded_with_all_messages_message_valid_initial_state_message. Qed.message: Type
X: VLSM message∀ om : option message, option_valid_message_prop (preloaded_with_all_messages_vlsm X) ommessage: Type
X: VLSM message∀ (s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s ommessage: Type
X: VLSM message∀ (s : state X) (om : option message), valid_state_message_prop X s om → constrained_state_message_prop X s ommessage: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X omconstrained_state_message_prop X s ommessage: 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 omconstrained_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 omconstrained_state_message_prop X s omby destruct om; cbn; [right |].message: Type
X: VLSM message
s: state X
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop X omoption_initial_message_prop (preloaded_with_all_messages_vlsm X) omby eapply valid_generated_state_message; cycle 2. Qed.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 omconstrained_state_message_prop X 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), 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) smessage: 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) omby 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')valid_state_prop (preloaded_with_all_messages_vlsm X) sby apply any_message_is_valid_in_preloaded. Qed.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) ommessage: Type
X: VLSM message∀ (s : state X) (tr : list transition_item), finite_valid_trace_from X s tr → finite_constrained_trace_from X s trmessage: Type
X: VLSM message∀ (s : state X) (tr : list transition_item), finite_valid_trace_from X s tr → finite_constrained_trace_from X s trmessage: Type
X: VLSM message
s: state X
H: valid_state_prop X sfinite_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 trfinite_constrained_trace_from X s (tr ++ [x])message: Type
X: VLSM message
s: state X
H: valid_state_prop X sfinite_constrained_trace_from X s []message: Type
X: VLSM message
s: state X
H: valid_state_prop X svalid_state_prop (preloaded_with_all_messages_vlsm X) smessage: Type
X: VLSM message
s: state X
om: option message
H: valid_state_message_prop X s omvalid_state_prop (preloaded_with_all_messages_vlsm X) sby apply preloaded_weaken_valid_state_message_prop.message: Type
X: VLSM message
s: state X
om: option message
H: valid_state_message_prop X s omvalid_state_message_prop (preloaded_with_all_messages_vlsm X) s ommessage: 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 trfinite_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 trfinite_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 trfinite_valid_trace_from (preloaded_with_all_messages_vlsm X) (finite_trace_last s tr) [x]by apply preloaded_weaken_input_valid_transition. Qed.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 trinput_valid_transition (preloaded_with_all_messages_vlsm X) l (finite_trace_last s tr, iom) (sf, oom)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 trmessage: 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 trmessage: 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 trvalid_state_prop X s → Forall (λ item : transition_item, option_valid_message_prop X (input item)) tr → finite_valid_trace_from_to X s f trmessage: 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 tlvalid_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)) tlfinite_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)) tlinput_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)) tlinput_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)) tlinput_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)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
H1: input_valid_transition X l (s', iom) (s, oom)finite_valid_trace_from_to X s f tlmessage: 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)) tlinput_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)) tlinput_valid_transition X l (s', iom) (s, oom)by destruct iom; [| apply option_valid_message_None]. Qed.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)) tloption_valid_message_prop X iommessage: 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 trmessage: 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 trmessage: 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)) trfinite_valid_trace_init_to X s f trmessage: 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)) trfinite_valid_trace_from_to X s f trby 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
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)) trvalid_state_prop X smessage: 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 oomby firstorder. Qed.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 oommessage: Type
X: VLSM message∀ s1 s2 : state X, valid_transition_next X s1 s2 ↔ valid_transition_next (preloaded_with_all_messages_vlsm X) s1 s2by 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: VLSM message∀ s1 s2 : state X, valid_transition_next X s1 s2 ↔ valid_transition_next (preloaded_with_all_messages_vlsm X) s1 s2message: 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_projectVLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_projectmessage: 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_projectVLSM_projection_type (preloaded_with_all_messages_vlsm X) Y label_project state_projectmessage: 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 trstate_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))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
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) = Nonestate_project sf = 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_projectVLSM_projection (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_projectmessage: 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_projectVLSM_projection (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_projectmessage: 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_projectVLSM_projection (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_projectmessage: 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 trXfinite_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 trXfinite_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 => [] endmessage: 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 lYfinite_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 lYinput_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 lYinput_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 lYoption_valid_message_prop (preloaded_with_all_messages_vlsm Y) iommessage: 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 lYvalid 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 lYtransition 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 lYoption_valid_message_prop (preloaded_with_all_messages_vlsm Y) iomby 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)
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 lYoption_valid_message_prop (preloaded_with_all_messages_vlsm Y) (Some m)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 lYvalid lY (state_project (finite_trace_last si tr), iom)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
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 lYtransition 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_projectVLSM_projection_type (preloaded_vlsm X P) Y label_project state_projectmessage: 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_projectVLSM_projection_type (preloaded_vlsm X P) Y label_project state_projectmessage: 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 trstate_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))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
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) = Nonestate_project sf = List.last (map destination []) (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_projectVLSM_projection (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_projectmessage: 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_projectVLSM_projection (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_projectmessage: 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_projectVLSM_projection (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_projectmessage: 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 trXfinite_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 trXfinite_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 => [] endmessage: 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 lYfinite_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 lYinput_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 lYoption_valid_message_prop (preloaded_vlsm Y Q) iommessage: 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 lYvalid 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 lYtransition 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 lYoption_valid_message_prop (preloaded_vlsm Y Q) iomby 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)
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 lYoption_valid_message_prop (preloaded_vlsm Y Q) (Some m)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 lYvalid lY (state_project (finite_trace_last si tr), iom)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
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 lYtransition lY (state_project (finite_trace_last si 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 YVLSM_embedding (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_projectmessage: 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 YVLSM_embedding (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y) label_project state_projectmessage: 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 trXfinite_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 trXfinite_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)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)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 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
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 YVLSM_embedding (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_projectmessage: 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 YVLSM_embedding (preloaded_vlsm X P) (preloaded_vlsm Y Q) label_project state_projectmessage: 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 trXfinite_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) trXfinite_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) trXfinite_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) iommessage: 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)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: 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, 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]))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
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])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 MYVLSM_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
Hinitial_state: strong_incl_initial_state_preservation MX MY
Hvalid: strong_incl_valid_preservation MX MY
Htransition: strong_incl_transition_preservation MX MYVLSM_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
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 MYVLSM_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
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 MYVLSM_incl (preloaded_vlsm X P) (preloaded_vlsm Y Q)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∀ P : message → Prop, VLSM_incl X (preloaded_vlsm X P)message: Type
X: VLSM messageVLSM_incl X (preloaded_with_all_messages_vlsm X)by apply vlsm_incl_preloaded. Qed.message: Type
X: VLSM messageVLSM_incl X (preloaded_with_all_messages_vlsm X)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) mVLSM_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) mweak_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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} mmessage: 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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} mby 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
Him: initial_message_prop mvalid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} mmessage: 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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} mby apply initial_message_is_valid; right. Qed.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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := preloaded_vlsm_machine X Q |} mmessage: 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 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 : 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 (preloaded_vlsm X P) P) (preloaded_vlsm X 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_vlsm (preloaded_vlsm X P) P)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∀ P : message → Prop, VLSM_incl (preloaded_vlsm X P) (preloaded_with_all_messages_vlsm X)message: Type
X: VLSM message∀ m : message, can_emit X m → can_emit (preloaded_with_all_messages_vlsm X) mmessage: Type
X: VLSM message∀ m : message, can_emit X m → can_emit (preloaded_with_all_messages_vlsm X) mmessage: Type
X: VLSM message
m: message
Hm: can_emit X mcan_emit (preloaded_with_all_messages_vlsm X) mby rewrite mk_vlsm_machine. Qed.message: Type
X: VLSM message
m: message
Hm: can_emit X mcan_emit {| vlsm_type := X; vlsm_machine := X |} mmessage: Type
X: VLSM message∀ (from : state X) (tr : list transition_item), finite_valid_trace_from X from tr → finite_constrained_trace_from X from trby 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 : state X) (tr : list transition_item), finite_valid_trace_from X from tr → finite_constrained_trace_from X from trmessage: 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 trby 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∀ (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 trmessage: 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) mVLSM_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) mVLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine X (λ m : message, P m ∨ Q m))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) mVLSM_incl_part (preloaded_vlsm_machine X (λ m : message, P m ∨ Q m)) (preloaded_vlsm_machine X P)by apply preloaded_vlsm_incl; itauto. Qed.message: Type
X: VLSM message
P, Q: message → Prop
H: ∀ m : message, Q m → valid_message_prop (preloaded_vlsm X P) mVLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine X (λ m : message, P m ∨ Q m))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 → PropVLSM_incl_part (preloaded_vlsm_machine (preloaded_vlsm X P) P) (preloaded_vlsm_machine X P)message: Type
X: VLSM message
P: message → PropVLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine (preloaded_vlsm X P) P)by apply preloaded_vlsm_idem_l.message: Type
X: VLSM message
P: message → PropVLSM_incl_part (preloaded_vlsm_machine (preloaded_vlsm X P) P) (preloaded_vlsm_machine X P)by apply preloaded_vlsm_idem_r. Qed.message: Type
X: VLSM message
P: message → PropVLSM_incl_part (preloaded_vlsm_machine X P) (preloaded_vlsm_machine (preloaded_vlsm X P) 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, (∀ (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) mVLSM_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) mVLSM_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) mstrong_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) mweak_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) mweak_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) mweak_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 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) mstrong_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 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) mweak_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 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) mweak_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 s' om' [_ Ht]. Qed.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) mweak_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 messageVLSM_eq X (preloaded_vlsm X (λ _ : message, False))by cbn; split; apply basic_VLSM_strong_incl; cbv; itauto. Qed.message: Type
X: VLSM messageVLSM_eq X (preloaded_vlsm X (λ _ : message, False))message: Type
X: VLSM messagestrong_embedding_initial_message_preservation X (preloaded_vlsm X (λ _ : message, False))by intros m Hm; left. Qed.message: Type
X: VLSM messagestrong_embedding_initial_message_preservation X (preloaded_vlsm X (λ _ : message, False))message: Type
X: VLSM messagestrong_embedding_initial_message_preservation (preloaded_vlsm X (λ _ : message, False)) Xby intros m []. Qed.message: Type
X: VLSM messagestrong_embedding_initial_message_preservation (preloaded_vlsm X (λ _ : message, False)) Xmessage: 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 ommessage: 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 ommessage: 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 omby split; (apply VLSM_incl_valid_state_message; [| cbv]); itauto. Qed. End sec_VLSM_eq_preloaded_properties.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
Direct definitions of constrained traces, states and messages
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 trmessage: 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 trmessage: 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 sfinite_constrained_trace_init_to_direct s f trmessage: 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 trconstrained_transitions_from_to s f trmessage: Type
X: VLSM message
s: state (preloaded_with_all_messages_vlsm X)
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) sconstrained_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 tlconstrained_transitions_from_to s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)by constructor.message: Type
X: VLSM message
s: state (preloaded_with_all_messages_vlsm X)
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) sconstrained_transitions_from_to s s []by constructor; [apply Ht..|]. Qed.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 tlconstrained_transitions_from_to s' f ({| l := l; input := iom; destination := s; output := oom |} :: tl)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 trmessage: 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 trmessage: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: constrained_transitions_from_to s f tr
Hs: initial_state_prop sfinite_constrained_trace_init_to X s f trmessage: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: constrained_transitions_from_to s f tr
Hs: initial_state_prop sfinite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f trmessage: 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) sfinite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f trmessage: Type
X: VLSM message
f: state X
Htr: constrained_transitions_from_to f f []
Hs: valid_state_prop (preloaded_with_all_messages_vlsm X) ffinite_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 trfinite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s f ({| l := l; input := om; destination := s'; output := om' |} :: tr)by apply (finite_valid_trace_from_to_empty (preloaded_with_all_messages_vlsm X)).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) ffinite_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 trfinite_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 trinput_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 trfinite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s' f trby 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 trinput_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 trfinite_valid_trace_from_to (preloaded_with_all_messages_vlsm X) s' f trmessage: 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 trvalid_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')by repeat split; [| apply any_message_is_valid_in_preloaded | ..]. Qed.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 trinput_valid_transition (preloaded_with_all_messages_vlsm X) l (s, om) (s', om')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 trmessage: 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 trmessage: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_constrained_trace_init_to_direct s f tr → finite_constrained_trace_init_to X s f trmessage: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_constrained_trace_init_to X s f tr → finite_constrained_trace_init_to_direct s f trby apply finite_constrained_trace_init_to_direct_left_impl.message: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_constrained_trace_init_to_direct s f tr → finite_constrained_trace_init_to X s f trby apply finite_constrained_trace_init_to_direct_right_impl. Qed.message: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_constrained_trace_init_to X s f tr → finite_constrained_trace_init_to_direct s f tr
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 smessage: Type
X: VLSM message∀ s : state X, constrained_state_prop_direct s ↔ constrained_state_prop X smessage: 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 smessage: 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 smessage: 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 smessage: Type
X: VLSM message
s: state Xconstrained_state_prop X s → ∃ (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to X s0 s trby intros (? & ? & []); eapply finite_valid_trace_from_to_last_pstate.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 sby intro Hs; apply valid_state_has_trace in Hs as (? & ? & ?); eexists _, _. Qed.message: Type
X: VLSM message
s: state Xconstrained_state_prop X s → ∃ (s0 : state X) (tr : list transition_item), finite_constrained_trace_init_to X s0 s tr
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 mmessage: Type
X: VLSM message∀ m : message, constrained_message_prop_direct m ↔ constrained_message_prop X mmessage: Type
X: VLSM message
m: messageconstrained_message_prop_direct m ↔ constrained_message_prop X mmessage: 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) mmessage: 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 mmessage: 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 mmessage: 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 mmessage: 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 mmessage: 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 mfinite_valid_trace (preloaded_with_all_messages_vlsm X) is (tr ++ [item]) ∧ last_error (tr ++ [item]) = Some item ∧ destination item = s ∧ output item = Some mmessage: 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 mfinite_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 mlast_error (tr ++ [item]) = Some itemmessage: 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 mdestination item = sby 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 mfinite_valid_trace (preloaded_with_all_messages_vlsm X) is (tr ++ [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 mlast_error (tr ++ [item]) = Some itemmessage: 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 mdestination item = sby erewrite <- finite_trace_last_is_last.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 mdestination item = smessage: 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 mmessage: 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 mmessage: 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 mmessage: 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 mby eexists _, _, _, _. Qed.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
Definitions of valid traces, messages, and states based on constrained ones
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 trmessage: 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 trmessage: Type
X: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X s f trfinite_valid_trace_init_to_from_constrained s f trmessage: 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_trfinite_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_trfinite_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_trfinite_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 |}])by apply finite_valid_trace_from_to_singleton.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 |}]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_itemitem ∈ 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_itemitem ∈ 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 |})by rewrite elem_of_app, elem_of_list_singleton; right. Qed.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]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 trmessage: 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 ommessage: 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 trmessage: 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 ommessage: 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 trmessage: 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 tr0message: 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)) tr0by 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
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 ∈ tr0option_valid_message_prop X (input x)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 ommessage: 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 ∈ troption_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 moption_valid_message_prop X (Some m)by eapply valid_trace_forget_last, finite_valid_trace_init_to_from_constrained_left_impl. 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
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 mfinite_valid_trace_from X ?is trmessage: 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 trmessage: 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 trmessage: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f trmessage: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_valid_trace_init_to X s f tr → finite_valid_trace_init_to_from_constrained s f trby apply finite_valid_trace_init_to_from_constrained_left_impl.message: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_valid_trace_init_to_from_constrained s f tr → finite_valid_trace_init_to X s f trby apply finite_valid_trace_init_to_from_constrained_right_impl. Qed.message: Type
X: VLSM message
s, f: state X
tr: list transition_itemfinite_valid_trace_init_to X s f tr → finite_valid_trace_init_to_from_constrained s f trmessage: Type
X: VLSM message∀ om : option message, option_valid_message_prop X om → option_valid_message_prop_from_constrained ommessage: Type
X: VLSM message∀ om : option message, option_valid_message_prop X om → option_valid_message_prop_from_constrained ommessage: 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 moption_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)by rewrite elem_of_app, elem_of_list_singleton; right. Qed.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]message: Type
X: VLSM message∀ om : option message, option_valid_message_prop_from_constrained om ↔ option_valid_message_prop X ommessage: Type
X: VLSM message∀ om : option message, option_valid_message_prop_from_constrained om ↔ option_valid_message_prop X ommessage: Type
X: VLSM message
om: option messageoption_valid_message_prop_from_constrained om → option_valid_message_prop X ommessage: Type
X: VLSM message
om: option messageoption_valid_message_prop X om → option_valid_message_prop_from_constrained omby apply option_valid_message_prop_from_constrained_left_impl.message: Type
X: VLSM message
om: option messageoption_valid_message_prop_from_constrained om → option_valid_message_prop X omby apply option_valid_message_prop_from_constrained_right_impl. Qed.message: Type
X: VLSM message
om: option messageoption_valid_message_prop X om → option_valid_message_prop_from_constrained om
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 smessage: Type
X: VLSM message∀ s : state X, valid_state_prop_from_constrained s → valid_state_prop X sby apply finite_valid_trace_init_to_from_constrained_equiv, valid_trace_last_pstate in Htr. Qed.message: Type
X: VLSM message
s, is: state X
tr: list transition_item
Htr: finite_valid_trace_init_to_from_constrained is s trvalid_state_prop X smessage: Type
X: VLSM message∀ s : state X, valid_state_prop X s → valid_state_prop_from_constrained smessage: Type
X: VLSM message∀ s : state X, valid_state_prop X s → valid_state_prop_from_constrained smessage: Type
X: VLSM message
s: state X
Hs: valid_state_prop X svalid_state_prop_from_constrained sby exists is, tr; apply finite_valid_trace_init_to_from_constrained_equiv. Qed.message: Type
X: VLSM message
s, is: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X is s trvalid_state_prop_from_constrained smessage: Type
X: VLSM message∀ s : state X, valid_state_prop_from_constrained s ↔ valid_state_prop X smessage: Type
X: VLSM message∀ s : state X, valid_state_prop_from_constrained s ↔ valid_state_prop X smessage: Type
X: VLSM message
s: state Xvalid_state_prop_from_constrained s → valid_state_prop X smessage: Type
X: VLSM message
s: state Xvalid_state_prop X s → valid_state_prop_from_constrained sby apply valid_state_prop_from_constrained_left_impl.message: Type
X: VLSM message
s: state Xvalid_state_prop_from_constrained s → valid_state_prop X sby apply valid_state_prop_from_constrained_right_impl. Qed. End sec_constrained_direct_defs.message: Type
X: VLSM message
s: state Xvalid_state_prop X s → valid_state_prop_from_constrained smessage: Type
X: VLSM messageVLSM_eq X (preloaded_vlsm X (valid_message_prop X))message: Type
X: VLSM messageVLSM_eq X (preloaded_vlsm X (valid_message_prop X))message: Type
X: VLSM messageVLSM_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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := X |} mmessage: 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 |} omvalid 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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := X |} mmessage: 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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := X |} mmessage: 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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := X |} mby 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)
Hinit: initial_message_prop mvalid_message_prop {| vlsm_type := X; vlsm_machine := X |} mby 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) |}
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 mvalid_message_prop {| vlsm_type := X; vlsm_machine := X |} mby 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
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 |} omvalid l (s, om)by apply H. Qed.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')