From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From VLSM.Lib Require Import Preamble.
From VLSM.Core Require Import VLSM Equivocation.[Loading ML file coq-itauto.plugin ... done]
From VLSM.Core Require Import Composition VLSMProjections Validator ProjectionTraces.

Core: VLSM Projections and Messages Properties

In this section, we show that messages properties (oracles like has_been_sent, has_been_received, and has_been_directly_observed) are reflected and, in some cases, preserved by VLSM projections.

Section sec_projection_oracle.

VLSM projections reflect message properties

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

Section sec_selectors.

Context
  (selectorX : message -> transition_item X -> Prop)
  (selectorY : message -> transition_item Y -> Prop)
  (Hselector : forall itemX itemY,
    input itemX = input itemY -> output itemX = output itemY ->
    forall m, selectorX m itemX <-> selectorY m itemY)
  .

Given the fact that all traces leading to a state in X project to traces leading to its projection in Y, and since all messages in a trace projection come from the original trace, it follows that any oracle for Y with the same selector is reflected to X.

Lemma VLSM_projection_oracle_reflect
  (oracleX : state X -> message -> Prop)
  (oracleY : state Y -> message -> Prop)
  (HstepwiseX : oracle_stepwise_props (vlsm := X) selectorX oracleX)
  (HstepwiseY : oracle_stepwise_props (vlsm := Y) selectorY oracleY)
  : forall s, constrained_state_prop X s ->
  forall m, oracleY (state_project s) m -> oracleX s m.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      oracleY (state_project s) m → oracleX s m
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      oracleY (state_project s) m → oracleX s m
  intros s Hs m Hm.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: oracleY (state_project s) m
oracleX s m
  apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseX _ Hs m).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: oracleY (state_project s) m
selected_message_exists_in_all_preloaded_traces X
  selectorX s m
  intros isX trX HtrX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: oracleY (state_project s) m
isX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) isX s
  trX
trace_has_message selectorX m trX
  apply (VLSM_projection_finite_valid_trace_init_to Hsimul) in HtrX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: oracleY (state_project s) m
isX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
trace_has_message selectorX m trX
  apply (VLSM_projection_valid_state Hsimul) in Hs as HsY.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: oracleY (state_project s) m
isX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
trace_has_message selectorX m trX
  apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseY _ HsY m) in Hm.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: selected_message_exists_in_all_preloaded_traces Y
  selectorY (state_project s) m
isX: state (preloaded_with_all_messages_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
trace_has_message selectorX m trX
  specialize (Hm _ _ HtrX).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
Hm: trace_has_message selectorY m
  (VLSM_projection_finite_trace_project Hsimul
     trX)
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
trace_has_message selectorX m trX
  apply Exists_exists in Hm as [itemY [HitemY Hm]].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY: transition_item
HitemY: itemY
∈ VLSM_projection_finite_trace_project Hsimul
    trX
Hm: selectorY m itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
trace_has_message selectorX m trX
  apply pre_VLSM_projection_finite_trace_project_elem_of_iff in HitemY
    as [itemX [HitemX Hpr]].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
Hpr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project itemX = 
Some itemY
Hm: selectorY m itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
trace_has_message selectorX m trX
  apply Exists_exists.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
Hpr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project itemX = 
Some itemY
Hm: selectorY m itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
∃ x : transition_item, x ∈ trX ∧ selectorX m x
  exists itemX.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
Hpr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project itemX = 
Some itemY
Hm: selectorY m itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
itemX ∈ trX ∧ selectorX m itemX split; [done |].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
Hpr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project itemX = 
Some itemY
Hm: selectorY m itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
selectorX m itemX
  revert Hm.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
Hpr: pre_VLSM_projection_transition_item_project
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project itemX = 
Some itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
selectorY m itemY → selectorX m itemX
  unfold pre_VLSM_projection_transition_item_project in Hpr.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
Hpr: match label_project (l itemX) with
| Some lY =>
    Some
      {|
        l := lY;
        input := input itemX;
        destination :=
          state_project (destination itemX);
        output := output itemX
      |}
| None => None
end = Some itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
selectorY m itemY → selectorX m itemX
  destruct (label_project (l itemX)); [| by congruence].message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
l: label Y
Hpr: Some
  {|
    l := l;
    input := input itemX;
    destination :=
      state_project (destination itemX);
    output := output itemX
  |} = Some itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
selectorY m itemY → selectorX m itemX
  inversion Hpr.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state X → message → Prop
oracleY: state Y → message → Prop
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
trX: list transition_item
itemY, itemX: transition_item
HitemX: itemX ∈ trX
l: label Y
Hpr: Some
  {|
    l := l;
    input := input itemX;
    destination :=
      state_project (destination itemX);
    output := output itemX
  |} = Some itemY
isX: state (preloaded_with_all_messages_vlsm X)
HtrX: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project isX) (state_project s)
  (VLSM_projection_finite_trace_project Hsimul
     trX)
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
H0: {|
  l := l;
  input := input itemX;
  destination :=
    state_project (destination itemX);
  output := output itemX
|} = itemY
selectorY m
  {|
    l := l;
    input := input itemX;
    destination := state_project (destination itemX);
    output := output itemX
  |} → selectorX m itemX
  by apply Hselector.
Qed.

End sec_selectors.

Lemma VLSM_projection_has_been_sent_reflect
  `{HasBeenSentCapability message X}
  `{HasBeenSentCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_sent Y (state_project s) m -> has_been_sent X s m.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent Y (state_project s) m
      → has_been_sent X s m
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent Y (state_project s) m
      → has_been_sent X s m
  apply VLSM_projection_oracle_reflect with (field_selector output) (field_selector output).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector output m itemX
        ↔ field_selector output m itemY
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent X)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent Y)
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector output m itemX
        ↔ field_selector output m itemY by intros [] [] **; cbn in *; subst.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent X) by apply (has_been_sent_stepwise_props X).
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent Y) by apply (has_been_sent_stepwise_props Y).
Qed.

Lemma VLSM_projection_has_been_received_reflect
  `{HasBeenReceivedCapability message X}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_received Y (state_project s) m -> has_been_received X s m.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received Y (state_project s) m
      → has_been_received X s m
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received Y (state_project s) m
      → has_been_received X s m
  apply VLSM_projection_oracle_reflect with (field_selector input) (field_selector input).message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector input m itemX
        ↔ field_selector input m itemY
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received X)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received Y)
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector input m itemX
        ↔ field_selector input m itemY by intros [] [] **; cbn in *; subst.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received X) by apply (has_been_received_stepwise_props X).
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received Y) by apply (has_been_received_stepwise_props Y).
Qed.

Lemma VLSM_projection_has_been_directly_observed_reflect
  `{HasBeenSentCapability message X}
  `{HasBeenReceivedCapability message X}
  `{HasBeenSentCapability message Y}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_directly_observed Y (state_project s) m -> has_been_directly_observed X s m.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed Y (state_project s) m
      → has_been_directly_observed X s m
Proof.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed Y (state_project s) m
      → has_been_directly_observed X s m
  apply VLSM_projection_oracle_reflect with item_sends_or_receives item_sends_or_receives.message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        item_sends_or_receives m itemX
        ↔ item_sends_or_receives m itemY
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed X)
message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed Y)
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        item_sends_or_receives m itemX
        ↔ item_sends_or_receives m itemY by intros [] [] **; cbn in *; subst.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed X) by apply has_been_directly_observed_stepwise_props.
  -message: Type
X, Y: VLSM message
label_project: label X → option (label Y)
state_project: state X → state Y
Hsimul: VLSM_projection
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed Y) by apply has_been_directly_observed_stepwise_props.
Qed.

End sec_projection_oracle.

Section sec_weak_embedding_oracle.

VLSM_weak_embeddings preserve message properties

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

Section sec_selectors.

Context
  (selectorX : message -> transition_item X -> Prop)
  (selectorY : message -> transition_item Y -> Prop)
  (Hselector : forall itemX itemY,
    input itemX = input itemY -> output itemX = output itemY ->
    forall m, selectorX m itemX <-> selectorY m itemY)
  .

Lemma VLSM_weak_embedding_selected_message_exists_in_some_preloaded_traces
  s m
  : selected_message_exists_in_some_preloaded_traces X selectorX s m ->
  selected_message_exists_in_some_preloaded_traces Y selectorY (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
selected_message_exists_in_some_preloaded_traces X
  selectorX s m
→ selected_message_exists_in_some_preloaded_traces Y
    selectorY (state_project s) m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
selected_message_exists_in_some_preloaded_traces X
  selectorX s m
→ selected_message_exists_in_some_preloaded_traces Y
    selectorY (state_project s) m
  intros [is [tr [Htr Hm]]].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) is s tr
Hm: trace_has_message selectorX m tr
selected_message_exists_in_some_preloaded_traces Y
  selectorY (state_project s) m
  destruct Htr as [Htr His].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is s tr
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
selected_message_exists_in_some_preloaded_traces Y
  selectorY (state_project s) m
  apply (VLSM_weak_embedding_finite_valid_trace_from_to Hsimul) in Htr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
selected_message_exists_in_some_preloaded_traces Y
  selectorY (state_project s) m
  apply valid_trace_first_pstate in Htr as Hpr_is.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
Hpr_is: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project is)
selected_message_exists_in_some_preloaded_traces Y
  selectorY (state_project s) m
  apply valid_state_has_trace in Hpr_is as [is' [tr_is Hpr_is]].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
selected_message_exists_in_some_preloaded_traces Y
  selectorY (state_project s) m
  exists is', (tr_is ++ (VLSM_weak_embedding_finite_trace_project Hsimul tr)).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
∃ _ : finite_valid_trace_init_to
        (preloaded_with_all_messages_vlsm Y) is'
        (state_project s)
        (tr_is ++
         VLSM_weak_embedding_finite_trace_project
           Hsimul tr),
  trace_has_message selectorY m
    (tr_is ++
     VLSM_weak_embedding_finite_trace_project Hsimul
       tr)
  destruct Hpr_is as [Hpr_is His'].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
∃ _ : finite_valid_trace_init_to
        (preloaded_with_all_messages_vlsm Y) is'
        (state_project s)
        (tr_is ++
         VLSM_weak_embedding_finite_trace_project
           Hsimul tr),
  trace_has_message selectorY m
    (tr_is ++
     VLSM_weak_embedding_finite_trace_project Hsimul
       tr)
  repeat split; [| done |].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project s)
  (tr_is ++
   VLSM_weak_embedding_finite_trace_project Hsimul tr)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
trace_has_message selectorY m
  (tr_is ++
   VLSM_weak_embedding_finite_trace_project Hsimul tr)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project s)
  (tr_is ++
   VLSM_weak_embedding_finite_trace_project Hsimul tr) by eapply (finite_valid_trace_from_to_app (preloaded_with_all_messages_vlsm Y)).
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
trace_has_message selectorY m
  (tr_is ++
   VLSM_weak_embedding_finite_trace_project Hsimul tr) apply Exists_app.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m) tr_is
∨ Exists (selectorY m)
    (VLSM_weak_embedding_finite_trace_project Hsimul
       tr) right.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
Hm: trace_has_message selectorX m tr
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (VLSM_weak_embedding_finite_trace_project Hsimul tr)
    apply Exists_exists in Hm as [item [Hitem Hm]].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
item: transition_item
Hitem: item ∈ tr
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (VLSM_weak_embedding_finite_trace_project Hsimul tr)
    apply elem_of_list_split in Hitem as [pre [suf Heqtr]].message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul tr)
His: initial_state_prop is
item: transition_item
pre, suf: list transition_item
Heqtr: tr = pre ++ item :: suf
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (VLSM_weak_embedding_finite_trace_project Hsimul tr)
    subst tr.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
pre, suf: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul (pre ++ item :: suf))
His: initial_state_prop is
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (VLSM_weak_embedding_finite_trace_project Hsimul
     (pre ++ item :: suf))
    setoid_rewrite map_app.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
pre, suf: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul (pre ++ item :: suf))
His: initial_state_prop is
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (map
     (pre_VLSM_embedding_transition_item_project
        (preloaded_with_all_messages_vlsm X)
        (preloaded_with_all_messages_vlsm Y)
        label_project state_project) pre ++
   map
     (pre_VLSM_embedding_transition_item_project
        (preloaded_with_all_messages_vlsm X)
        (preloaded_with_all_messages_vlsm Y)
        label_project state_project) (item :: suf))
    apply List.Exists_app.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
pre, suf: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul (pre ++ item :: suf))
His: initial_state_prop is
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (map
     (pre_VLSM_embedding_transition_item_project
        (preloaded_with_all_messages_vlsm X)
        (preloaded_with_all_messages_vlsm Y)
        label_project state_project) pre)
∨ Exists (selectorY m)
    (map
       (pre_VLSM_embedding_transition_item_project
          (preloaded_with_all_messages_vlsm X)
          (preloaded_with_all_messages_vlsm Y)
          label_project state_project) (item :: suf)) right.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
pre, suf: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul (pre ++ item :: suf))
His: initial_state_prop is
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (map
     (pre_VLSM_embedding_transition_item_project
        (preloaded_with_all_messages_vlsm X)
        (preloaded_with_all_messages_vlsm Y)
        label_project state_project) (item :: suf)) simpl.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
pre, suf: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul (pre ++ item :: suf))
His: initial_state_prop is
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
Exists (selectorY m)
  (pre_VLSM_embedding_transition_item_project X Y
     label_project state_project item
   :: map
        (pre_VLSM_embedding_transition_item_project X
           Y label_project state_project) suf) left.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
pre, suf: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul (pre ++ item :: suf))
His: initial_state_prop is
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
selectorY m
  (pre_VLSM_embedding_transition_item_project X Y
     label_project state_project item)
    remember  (pre_VLSM_embedding_transition_item_project _ _ _ _ _) as itemY.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
s: state (preloaded_with_all_messages_vlsm X)
m: message
is: state (preloaded_with_all_messages_vlsm X)
item: transition_item
pre, suf: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y)
  (state_project is) (state_project s)
  (VLSM_weak_embedding_finite_trace_project
     Hsimul (pre ++ item :: suf))
His: initial_state_prop is
Hm: selectorX m item
is': state (preloaded_with_all_messages_vlsm Y)
tr_is: list transition_item
Hpr_is: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Y) is'
  (state_project is) tr_is
His': initial_state_prop is'
itemY: transition_item
HeqitemY: itemY =
pre_VLSM_embedding_transition_item_project
  X Y label_project state_project item
selectorY m itemY
    by apply (Hselector item itemY); subst.
Qed.

Lemma VLSM_weak_embedding_oracle
  oracleX oracleY
  (HstepwiseX : oracle_stepwise_props (vlsm := X) selectorX oracleX)
  (HstepwiseY : oracle_stepwise_props (vlsm := Y) selectorY oracleY)
  (HoracleX_dec : RelDecision oracleX)
  (HoracleY_dec : RelDecision oracleY)
  : forall s, constrained_state_prop X s ->
    forall m, oracleX s m -> oracleY (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      oracleX s m → oracleY (state_project s) m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      oracleX s m → oracleY (state_project s) m
  intros s Hs m Hm.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: oracleX s m
oracleY (state_project s) m
  apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseX _ Hs m) in Hm.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: selected_message_exists_in_all_preloaded_traces X
  selectorX s m
oracleY (state_project s) m
  apply (selected_messages_consistency_prop_from_stepwise _ _ _ _ HstepwiseX HoracleX_dec _ Hs) in Hm.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: selected_message_exists_in_some_preloaded_traces
  X selectorX s m
oracleY (state_project s) m
  apply (VLSM_weak_embedding_valid_state Hsimul) in Hs as HsY.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: selected_message_exists_in_some_preloaded_traces
  X selectorX s m
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
oracleY (state_project s) m
  apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseY _ HsY m).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: selected_message_exists_in_some_preloaded_traces
  X selectorX s m
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
selected_message_exists_in_all_preloaded_traces Y
  selectorY (state_project s) m
  apply (selected_messages_consistency_prop_from_stepwise _ _ _ _ HstepwiseY HoracleY_dec _ HsY).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
selectorX, selectorY: message → transition_item → Prop
Hselector: ∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        selectorX m itemX
        ↔ selectorY m itemY
oracleX: state_message_oracle X
oracleY: state_message_oracle Y
HstepwiseX: oracle_stepwise_props selectorX oracleX
HstepwiseY: oracle_stepwise_props selectorY oracleY
HoracleX_dec: RelDecision oracleX
HoracleY_dec: RelDecision oracleY
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: selected_message_exists_in_some_preloaded_traces
  X selectorX s m
HsY: valid_state_prop
  (preloaded_with_all_messages_vlsm Y)
  (state_project s)
selected_message_exists_in_some_preloaded_traces Y
  selectorY (state_project s) m
  by apply VLSM_weak_embedding_selected_message_exists_in_some_preloaded_traces.
Qed.

End sec_selectors.

Lemma VLSM_weak_embedding_has_been_sent
  `{HasBeenSentCapability message X}
  `{HasBeenSentCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_sent X s m -> has_been_sent Y (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent X s m
      → has_been_sent Y (state_project s) m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent X s m
      → has_been_sent Y (state_project s) m
  apply VLSM_weak_embedding_oracle with (field_selector output) (field_selector output).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector output m itemX
        ↔ field_selector output m itemY
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent X)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent Y)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
RelDecision (has_been_sent X)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
RelDecision (has_been_sent Y)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector output m itemX
        ↔ field_selector output m itemY by intros [] [] Hin Hout; cbn in *; subst.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent X) by apply (has_been_sent_stepwise_props X).
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
oracle_stepwise_props (field_selector output)
  (has_been_sent Y) by apply (has_been_sent_stepwise_props Y).
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
RelDecision (has_been_sent X) by apply has_been_sent_dec.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
RelDecision (has_been_sent Y) by apply has_been_sent_dec.
Qed.

Lemma VLSM_weak_embedding_has_been_received
  `{HasBeenReceivedCapability message X}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_received X s m -> has_been_received Y (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received X s m
      → has_been_received Y (state_project s) m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received X s m
      → has_been_received Y (state_project s) m
  apply VLSM_weak_embedding_oracle with (field_selector input) (field_selector input).message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector input m itemX
        ↔ field_selector input m itemY
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received X)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received Y)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
RelDecision (has_been_received X)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
RelDecision (has_been_received Y)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        field_selector input m itemX
        ↔ field_selector input m itemY by intros [] [] Hin Hout; cbn in *; subst.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received X) by apply (has_been_received_stepwise_props X).
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
oracle_stepwise_props (field_selector input)
  (has_been_received Y) by apply (has_been_received_stepwise_props Y).
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
RelDecision (has_been_received X) by apply has_been_received_dec.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
RelDecision (has_been_received Y) by apply has_been_received_dec.
Qed.

Lemma VLSM_weak_embedding_has_been_directly_observed
  `{HasBeenSentCapability message X}
  `{HasBeenReceivedCapability message X}
  `{HasBeenSentCapability message Y}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_directly_observed X s m -> has_been_directly_observed Y (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed X s m
      → has_been_directly_observed Y (state_project s)
          m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed X s m
      → has_been_directly_observed Y (state_project s)
          m
  apply VLSM_weak_embedding_oracle with item_sends_or_receives item_sends_or_receives.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        item_sends_or_receives m itemX
        ↔ item_sends_or_receives m itemY
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed X)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed Y)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
RelDecision (has_been_directly_observed X)
message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
RelDecision (has_been_directly_observed Y)
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ itemX itemY : transition_item,
  input itemX = input itemY
  → output itemX = output itemY
    → ∀ m : message,
        item_sends_or_receives m itemX
        ↔ item_sends_or_receives m itemY by intros [] [] **; cbn in *; subst.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed X) by apply has_been_directly_observed_stepwise_props.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
oracle_stepwise_props item_sends_or_receives
  (has_been_directly_observed Y) by apply has_been_directly_observed_stepwise_props.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
RelDecision (has_been_directly_observed X) by apply has_been_directly_observed_dec.
  -message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
RelDecision (has_been_directly_observed Y) by apply has_been_directly_observed_dec.
Qed.

End sec_weak_embedding_oracle.

Section sec_embedding_oracle.

VLSM_embeddings both preserve and reflect message properties

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

Lemma VLSM_embedding_has_been_sent
  `{HasBeenSentCapability message X}
  `{HasBeenSentCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_sent X s m -> has_been_sent Y (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent X s m
      → has_been_sent Y (state_project s) m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent X s m
      → has_been_sent Y (state_project s) m
  exact (VLSM_weak_embedding_has_been_sent (VLSM_embedding_weaken Hsimul)).
Qed.

Lemma VLSM_embedding_has_been_received
  `{HasBeenReceivedCapability message X}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_received X s m -> has_been_received Y (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received X s m
      → has_been_received Y (state_project s) m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received X s m
      → has_been_received Y (state_project s) m
  exact (VLSM_weak_embedding_has_been_received (VLSM_embedding_weaken Hsimul)).
Qed.

Lemma VLSM_embedding_has_been_directly_observed
  `{HasBeenSentCapability message X}
  `{HasBeenReceivedCapability message X}
  `{HasBeenSentCapability message Y}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_directly_observed X s m -> has_been_directly_observed Y (state_project s) m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed X s m
      → has_been_directly_observed Y (state_project s)
          m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed X s m
      → has_been_directly_observed Y (state_project s)
          m
  exact (VLSM_weak_embedding_has_been_directly_observed (VLSM_embedding_weaken Hsimul)).
Qed.

Lemma VLSM_embedding_has_been_sent_reflect
  `{HasBeenSentCapability message X}
  `{HasBeenSentCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_sent Y (state_project s) m -> has_been_sent X s m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent Y (state_project s) m
      → has_been_sent X s m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent Y (state_project s) m
      → has_been_sent X s m
  exact (VLSM_projection_has_been_sent_reflect  (VLSM_embedding_is_projection Hsimul)).
Qed.

Lemma VLSM_embedding_has_been_received_reflect
  `{HasBeenReceivedCapability message X}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_received Y (state_project s) m -> has_been_received X s m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received Y (state_project s) m
      → has_been_received X s m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received Y (state_project s) m
      → has_been_received X s m
  exact (VLSM_projection_has_been_received_reflect  (VLSM_embedding_is_projection Hsimul)).
Qed.

Lemma VLSM_embedding_has_been_directly_observed_reflect
  `{HasBeenSentCapability message X}
  `{HasBeenReceivedCapability message X}
  `{HasBeenSentCapability message Y}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_directly_observed Y (state_project s) m -> has_been_directly_observed X s m.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed Y (state_project s) m
      → has_been_directly_observed X s m
Proof.message: Type
X, Y: VLSM message
label_project: label X → label Y
state_project: state X → state Y
Hsimul: VLSM_embedding
  (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
  label_project state_project
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed Y (state_project s) m
      → has_been_directly_observed X s m
  exact (VLSM_projection_has_been_directly_observed_reflect (VLSM_embedding_is_projection Hsimul)).
Qed.

End sec_embedding_oracle.

Section sec_incl_oracle.

VLSM_inclusions both preserve and reflect message properties

Context
  {message : Type}
  {T : VLSMType message}
  {MX MY : VLSMMachine T}
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  (Hincl : VLSM_incl (preloaded_with_all_messages_vlsm X) (preloaded_with_all_messages_vlsm Y))
  .

Lemma VLSM_incl_has_been_sent
  `{HasBeenSentCapability message X}
  `{HasBeenSentCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_sent X s m -> has_been_sent Y s m.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent X s m → has_been_sent Y s m
Proof.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent X s m → has_been_sent Y s m
  intros s Hs m Hm.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: has_been_sent X s m
has_been_sent Y s m
  by eapply
    (@VLSM_embedding_has_been_sent _ X Y _ _
      (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_has_been_received
  `{HasBeenReceivedCapability message X}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_received X s m -> has_been_received Y s m.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received X s m
      → has_been_received Y s m
Proof.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received X s m
      → has_been_received Y s m
  intros s Hs m Hm.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: has_been_received X s m
has_been_received Y s m
  by eapply
    (@VLSM_embedding_has_been_received _ X Y _ _
      (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_has_been_directly_observed
  `{HasBeenSentCapability message X}
  `{HasBeenReceivedCapability message X}
  `{HasBeenSentCapability message Y}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_directly_observed X s m -> has_been_directly_observed Y s m.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed X s m
      → has_been_directly_observed Y s m
Proof.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed X s m
      → has_been_directly_observed Y s m
  intros s Hs m Hm.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: has_been_directly_observed X s m
has_been_directly_observed Y s m
  by eapply
    (@VLSM_embedding_has_been_directly_observed _ X Y _ _
      (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_has_been_sent_reflect
  `{HasBeenSentCapability message X}
  `{HasBeenSentCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_sent Y s m -> has_been_sent X s m.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent Y s m → has_been_sent X s m
Proof.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_sent Y s m → has_been_sent X s m
  intros s Hs m Hm.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenSentCapability Y
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: has_been_sent Y s m
has_been_sent X s m
  by eapply
    (@VLSM_embedding_has_been_sent_reflect _ X Y _ _
      (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_has_been_received_reflect
  `{HasBeenReceivedCapability message X}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_received Y s m -> has_been_received X s m.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received Y s m
      → has_been_received X s m
Proof.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_received Y s m
      → has_been_received X s m
  intros s Hs m Hm.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenReceivedCapability X
H0: HasBeenReceivedCapability Y
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: has_been_received Y s m
has_been_received X s m
  by eapply
    (@VLSM_embedding_has_been_received_reflect _ X Y _ _
      (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_has_been_directly_observed_reflect
  `{HasBeenSentCapability message X}
  `{HasBeenReceivedCapability message X}
  `{HasBeenSentCapability message Y}
  `{HasBeenReceivedCapability message Y}
  : forall s, constrained_state_prop X s ->
    forall m, has_been_directly_observed Y s m -> has_been_directly_observed X s m.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed Y s m
      → has_been_directly_observed X s m
Proof.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
∀ s : state (preloaded_with_all_messages_vlsm X),
  constrained_state_prop X s
  → ∀ m : message,
      has_been_directly_observed Y s m
      → has_been_directly_observed X s m
  intros s Hs m Hm.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
Hincl: VLSM_incl (preloaded_with_all_messages_vlsm X)
  (preloaded_with_all_messages_vlsm Y)
H: HasBeenSentCapability X
H0: HasBeenReceivedCapability X
H1: HasBeenSentCapability Y
H2: HasBeenReceivedCapability Y
s: state (preloaded_with_all_messages_vlsm X)
Hs: constrained_state_prop X s
m: message
Hm: has_been_directly_observed Y s m
has_been_directly_observed X s m
  by eapply
    (@VLSM_embedding_has_been_directly_observed_reflect _ X Y _ _
      (VLSM_incl_is_embedding Hincl)).
Qed.

End sec_incl_oracle.

Section sec_same_IM_oracle_properties.

Context
  {message : Type}
  `{finite.Finite index}
  (IM1 IM2 : index -> VLSM message)
  `{forall i, HasBeenSentCapability (IM1 i)}
  `{forall i, HasBeenSentCapability (IM2 i)}
  (Heq : forall i, IM1 i = IM2 i)
  .

If two indexed sets of VLSMs are extensionally-equal, then the has_been_sent predicate is preserved through the same_IM_state_rew map.

Lemma same_IM_composite_has_been_sent_preservation s1 m
  (Hs1 : constrained_state_prop (free_composite_vlsm IM1) s1)
  : composite_has_been_sent IM1 s1 m ->
    composite_has_been_sent IM2 (same_IM_state_rew Heq s1) m.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM1, IM2: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM1 i)
H1: ∀ i : index, HasBeenSentCapability (IM2 i)
Heq: ∀ i : index, IM1 i = IM2 i
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM1))
m: message
Hs1: constrained_state_prop 
  (free_composite_vlsm IM1) s1
composite_has_been_sent IM1 s1 m
→ composite_has_been_sent IM2
    (same_IM_state_rew Heq s1) m
Proof.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM1, IM2: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM1 i)
H1: ∀ i : index, HasBeenSentCapability (IM2 i)
Heq: ∀ i : index, IM1 i = IM2 i
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM1))
m: message
Hs1: constrained_state_prop 
  (free_composite_vlsm IM1) s1
composite_has_been_sent IM1 s1 m
→ composite_has_been_sent IM2
    (same_IM_state_rew Heq s1) m
  specialize (same_IM_preloaded_free_embedding IM1 IM2 Heq) as Hproj.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM1, IM2: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM1 i)
H1: ∀ i : index, HasBeenSentCapability (IM2 i)
Heq: ∀ i : index, IM1 i = IM2 i
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM1))
m: message
Hs1: constrained_state_prop 
  (free_composite_vlsm IM1) s1
Hproj: VLSM_embedding
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM1))
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM2))
  (same_IM_label_rew Heq)
  (same_IM_state_rew Heq)
composite_has_been_sent IM1 s1 m
→ composite_has_been_sent IM2
    (same_IM_state_rew Heq s1) m
  intros Hbs1_m.message, index: Type
EqDecision0: EqDecision index
H: finite.Finite index
IM1, IM2: index → VLSM message
H0: ∀ i : index, HasBeenSentCapability (IM1 i)
H1: ∀ i : index, HasBeenSentCapability (IM2 i)
Heq: ∀ i : index, IM1 i = IM2 i
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM1))
m: message
Hs1: constrained_state_prop 
  (free_composite_vlsm IM1) s1
Hproj: VLSM_embedding
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM1))
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM2))
  (same_IM_label_rew Heq)
  (same_IM_state_rew Heq)
Hbs1_m: composite_has_been_sent IM1 s1 m
composite_has_been_sent IM2 (same_IM_state_rew Heq s1)
  m
  by specialize (VLSM_embedding_has_been_sent Hproj _ Hs1 m Hbs1_m).
Qed.

End sec_same_IM_oracle_properties.

Section sec_sender_safety_can_emit_projection.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  {validator : Type}
  (A : validator -> index)
  (sender : message -> option validator)
  (Hsender_safety : sender_safety_alt_prop IM A sender)
  (j : index)
  (m : message)
  (Hj : option_map A (sender m) = Some j)
  .

Under sender_safety_alt_property assumptions, if a message can be emitted by the free composition (preloaded with all messages), then it can also be emitted by the component corresponding to its sender (preloaded with all messages).

Lemma can_emit_projection :
  can_emit (preloaded_with_all_messages_vlsm (free_composite_vlsm IM)) m ->
  can_emit (preloaded_with_all_messages_vlsm (IM j)) m.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
j: index
m: message
Hj: option_map A (sender m) = Some j
can_emit
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) m
→ can_emit (preloaded_with_all_messages_vlsm (IM j)) m
Proof.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
j: index
m: message
Hj: option_map A (sender m) = Some j
can_emit
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) m
→ can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  destruct (sender m) as [v |] eqn: Hsender; simpl in Hj; [| by congruence].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
j: index
m: message
v: validator
Hsender: sender m = Some v
Hj: Some (A v) = Some j
can_emit
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) m
→ can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  apply Some_inj in Hj.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
Hsender_safety: sender_safety_alt_prop IM A sender
j: index
m: message
v: validator
Hsender: sender m = Some v
Hj: A v = j
can_emit
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) m
→ can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  specialize (Hsender_safety _ _ Hsender).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
can_emit
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM)) m
→ can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  intros [(s0, om0) [(i, li) [s1 Hemitted]]].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
s0: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (existT i li) (s0, om0) (
  s1, Some m)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  specialize (preloaded_component_projection IM i) as Hproj.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
s0: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (existT i li) (s0, om0) (
  s1, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  specialize (VLSM_projection_input_valid_transition Hproj (existT i li) li)
    as Htransition.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
s0: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (existT i li) (s0, om0) (
  s1, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
Htransition: composite_project_label IM i
  (existT i li) = Some li
→ ∀ (s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM))) 
    (im : option message) 
    (s' : state
            (preloaded_with_all_messages_vlsm
               (free_composite_vlsm IM))) 
    (om : option message),
    input_valid_transition
      (preloaded_with_all_messages_vlsm
         (free_composite_vlsm IM))
      (existT i li) (s, im) (
      s', om)
    → input_valid_transition
        (preloaded_with_all_messages_vlsm
           (IM i)) li
        ((λ s0 : state
                   (preloaded_with_all_messages_vlsm
                      (free_composite_vlsm
                      IM)), 
            s0 i) s, im)
        ((λ s0 : state
                   (preloaded_with_all_messages_vlsm
                      (free_composite_vlsm
                      IM)), 
            s0 i) s', om)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  spec Htransition; [by apply (composite_project_label_eq IM) |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
s0: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (existT i li) (s0, om0) (
  s1, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
Htransition: ∀ (s : state
         (preloaded_with_all_messages_vlsm
            (free_composite_vlsm IM))) 
  (im : option message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (free_composite_vlsm IM))) 
  (om : option message),
  input_valid_transition
    (preloaded_with_all_messages_vlsm
       (free_composite_vlsm IM))
    (existT i li) (s, im) (
    s', om)
  → input_valid_transition
      (preloaded_with_all_messages_vlsm
         (IM i)) li (s i, im) (
      s' i, om)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  apply Htransition in Hemitted.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
s0: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0 i, om0) (s1 i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
Htransition: ∀ (s : state
         (preloaded_with_all_messages_vlsm
            (free_composite_vlsm IM))) 
  (im : option message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (free_composite_vlsm IM))) 
  (om : option message),
  input_valid_transition
    (preloaded_with_all_messages_vlsm
       (free_composite_vlsm IM))
    (existT i li) (s, im) (
    s', om)
  → input_valid_transition
      (preloaded_with_all_messages_vlsm
         (IM i)) li (s i, im) (
      s' i, om)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m clear Htransition.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
s0: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0 i, om0) (s1 i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  remember (s0 i) as s0i.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
s0: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s0i: state (IM i)
Heqs0i: s0i = s0 i
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0i, om0) (s1 i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m clear s0 Heqs0i.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s0i: state (IM i)
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0i, om0) (s1 i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  remember (s1 i) as s1i.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
om0: option message
i: index
li: label (IM i)
s1: state
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
s0i, s1i: state (IM i)
Heqs1i: s1i = s1 i
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0i, om0) (s1i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m clear s1 Heqs1i.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender_safety: ∀ i : index,
  can_emit
    (preloaded_with_all_messages_vlsm
       (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
om0: option message
i: index
li: label (IM i)
s0i, s1i: state (IM i)
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0i, om0) (s1i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  specialize (Hsender_safety i).message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
i: index
Hsender_safety: can_emit
  (preloaded_with_all_messages_vlsm
     (IM i)) m → A v = i
j: index
Hsender: sender m = Some v
Hj: A v = j
om0: option message
li: label (IM i)
s0i, s1i: state (IM i)
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0i, om0) (s1i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  spec Hsender_safety; [by eexists _, _, _ |].message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
i, j: index
Hsender: sender m = Some v
Hj: A v = j
om0: option message
li: label (IM i)
s0i, s1i: state (IM i)
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm (IM i))
  li (s0i, om0) (s1i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM i))
  (composite_project_label IM i)
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)), 
     s i)
Hsender_safety: A v = i
can_emit (preloaded_with_all_messages_vlsm (IM j)) m
  rewrite Hsender_safety in Hj; subst.message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
validator: Type
A: validator → index
sender: message → option validator
m: message
v: validator
Hsender: sender m = Some v
om0: option message
li: label (IM (A v))
s0i, s1i: state (IM (A v))
Hemitted: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (IM (A v))) li (s0i, om0)
  (s1i, Some m)
Hproj: VLSM_projection
  (preloaded_with_all_messages_vlsm
     (free_composite_vlsm IM))
  (preloaded_with_all_messages_vlsm (IM (A v)))
  (composite_project_label IM (A v))
  (λ s : state
           (preloaded_with_all_messages_vlsm
              (free_composite_vlsm IM)),
     s (A v))
can_emit (preloaded_with_all_messages_vlsm (IM (A v)))
  m
  by eexists _, _, _.
Qed.

End sec_sender_safety_can_emit_projection.