From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.
From Coq Require Import Streams.
From VLSM.Lib Require Import Preamble.
From VLSM.Core Require Import VLSM PreloadedVLSM VLSMInclusion VLSMEmbedding VLSMEquality.

Core: Constrained VLSMs

Given a base VLSM X, we can further constrain its validity condition with the given predicate, producing a new VLSM.

Section sec_constrained_vlsm.

Context
  {message : Type}
  (X : VLSM message)
  (constraint : label X -> state X * option message -> Prop)
  .

Definition constrained_vlsm_type : VLSMType message :=
  vlsm_type X.

Definition constrained_vlsm_machine : VLSMMachine X :=
{|
  initial_state_prop := @initial_state_prop _ _ X;
  initial_message_prop := @initial_message_prop _ _ X;
  s0 := @s0 _ _ X;
  transition := @transition _ _ X;
  valid := fun l som => valid X l som /\ constraint l som;
|}.

Definition constrained_vlsm : VLSM message :=
{|
  vlsm_type := vlsm_type X;
  vlsm_machine := constrained_vlsm_machine;
|}.

End sec_constrained_vlsm.

Lemma VLSM_embedding_constrained_vlsm :
  forall `(X : VLSM message) (constraint : label X -> state X * option message -> Prop),
    VLSM_embedding (constrained_vlsm X constraint) X id id.∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop),
  VLSM_embedding (constrained_vlsm X constraint) X id
    id
Proof.∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop),
  VLSM_embedding (constrained_vlsm X constraint) X id
    id
  intros.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_embedding (constrained_vlsm X constraint) X id id
  apply basic_VLSM_strong_embedding; red; cbn; [| done..].message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (l : label X) (s : state X) (om : option message),
  valid l (s, om) ∧ constraint l (s, om)
  → valid l (s, om)
  by itauto.
Qed.

Lemma VLSM_incl_constrained_vlsm :
  forall `(X : VLSM message) (constraint : label X -> state X * option message -> Prop),
    VLSM_incl (constrained_vlsm X constraint) X.∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop),
  VLSM_incl (constrained_vlsm X constraint) X
Proof.∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop),
  VLSM_incl (constrained_vlsm X constraint) X
  intros message X.message: Type
X: VLSM message
∀ constraint : label X
               → state X * option message → Prop,
  VLSM_incl (constrained_vlsm X constraint) X
  rewrite <- (mk_vlsm_machine X); cbn.message: Type
X: VLSM message
∀ constraint : label X
               → state X * option message → Prop,
  VLSM_incl_part
    (constrained_vlsm_machine
       {| vlsm_type := X; vlsm_machine := X |}
       constraint) X
  intros constraint.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_incl_part
  (constrained_vlsm_machine
     {| vlsm_type := X; vlsm_machine := X |}
     constraint) X
  apply (VLSMInclusion.VLSM_incl_embedding_iff (constrained_vlsm_machine X constraint)).message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_embedding
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint
  |}
  {|
    vlsm_type := X;
    vlsm_machine :=
      let
        (vlsm_type, vlsm_machine) as v
         return (VLSMMachine v) := X in
      vlsm_machine
  |} id id
  by apply (VLSM_embedding_constrained_vlsm {| vlsm_type := X; vlsm_machine := X; |}).
Qed.

Section sec_constrained_vlsm_lemmas.

Context
  {message : Type}
  (X : VLSM message)
  (constraint : label X -> state X * option message -> Prop)
  .

Lemma option_initial_message_prop_constrained_vlsm :
  forall om : option message,
    @option_initial_message_prop _ _ (constrained_vlsm X constraint) om
      <->
    @option_initial_message_prop _ _ X om.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ om : option message,
  option_initial_message_prop
    (constrained_vlsm X constraint) om
  ↔ option_initial_message_prop X om
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ om : option message,
  option_initial_message_prop
    (constrained_vlsm X constraint) om
  ↔ option_initial_message_prop X om
  done.
Qed.

Lemma valid_state_message_prop_constrained_vlsm :
  forall
    (s : state _) (om : option message),
      valid_state_message_prop (constrained_vlsm X constraint) s om ->
        valid_state_message_prop X s om.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (om : 
                                               option
                                                 message),
  valid_state_message_prop
    (constrained_vlsm X constraint) s om
  → valid_state_message_prop X s om
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (om : 
                                               option
                                                 message),
  valid_state_message_prop
    (constrained_vlsm X constraint) s om
  → valid_state_message_prop X s om
  intros s om H.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
om: option message
H: valid_state_message_prop
  (constrained_vlsm X constraint) s om
valid_state_message_prop X s om
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
H: valid_state_message_prop
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s om
valid_state_message_prop
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s om
  eapply VLSM_incl_valid_state_message; [.. | by do 2 red | done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
H: valid_state_message_prop
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s om
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma valid_state_prop_constrained_vlsm :
  forall (s : state _),
    valid_state_prop (constrained_vlsm X constraint) s ->
      valid_state_prop X s.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ s : state (constrained_vlsm X constraint),
  valid_state_prop (constrained_vlsm X constraint) s
  → valid_state_prop X s
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ s : state (constrained_vlsm X constraint),
  valid_state_prop (constrained_vlsm X constraint) s
  → valid_state_prop X s
  intros s [om Hvsmp].message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
om: option message
Hvsmp: valid_state_message_prop
  (constrained_vlsm X constraint) s om
valid_state_prop X s
  exists om.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
om: option message
Hvsmp: valid_state_message_prop
  (constrained_vlsm X constraint) s om
valid_state_message_prop X s om
  by apply valid_state_message_prop_constrained_vlsm.
Qed.

Lemma valid_message_prop_constrained_vlsm :
  forall (m : message),
    valid_message_prop (constrained_vlsm X constraint) m ->
      valid_message_prop X m.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ m : message,
  valid_message_prop (constrained_vlsm X constraint) m
  → valid_message_prop X m
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ m : message,
  valid_message_prop (constrained_vlsm X constraint) m
  → valid_message_prop X m
  intros m [s Hvsmp].message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
m: message
s: state (constrained_vlsm X constraint)
Hvsmp: valid_state_message_prop
  (constrained_vlsm X constraint) s 
  (Some m)
valid_message_prop X m
  exists s.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
m: message
s: state (constrained_vlsm X constraint)
Hvsmp: valid_state_message_prop
  (constrained_vlsm X constraint) s 
  (Some m)
valid_state_message_prop X s (Some m)
  by apply valid_state_message_prop_constrained_vlsm.
Qed.

Lemma option_valid_message_prop_constrained_vlsm :
  forall (om : option message),
    option_valid_message_prop (constrained_vlsm X constraint) om ->
      option_valid_message_prop X om.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ om : option message,
  option_valid_message_prop
    (constrained_vlsm X constraint) om
  → option_valid_message_prop X om
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ om : option message,
  option_valid_message_prop
    (constrained_vlsm X constraint) om
  → option_valid_message_prop X om
  intros om [s Hvsmp].message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
om: option message
s: state (constrained_vlsm X constraint)
Hvsmp: valid_state_message_prop
  (constrained_vlsm X constraint) s om
option_valid_message_prop X om
  exists s.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
om: option message
s: state (constrained_vlsm X constraint)
Hvsmp: valid_state_message_prop
  (constrained_vlsm X constraint) s om
valid_state_message_prop X s om
  by apply valid_state_message_prop_constrained_vlsm.
Qed.

Lemma input_valid_constrained_vlsm :
  forall (l : label _) (som : state _ * option message),
    input_valid (constrained_vlsm X constraint) l som ->
      input_valid X l som.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (l : label (constrained_vlsm X constraint)) (som : 
                                               state
                                                 (constrained_vlsm
                                                 X
                                                 constraint) *
                                               option
                                                 message),
  input_valid (constrained_vlsm X constraint) l som
  → input_valid X l som
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (l : label (constrained_vlsm X constraint)) (som : 
                                               state
                                                 (constrained_vlsm
                                                 X
                                                 constraint) *
                                               option
                                                 message),
  input_valid (constrained_vlsm X constraint) l som
  → input_valid X l som
  intros l [s om] Hiv.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
l: label (constrained_vlsm X constraint)
s: state (constrained_vlsm X constraint)
om: option message
Hiv: input_valid (constrained_vlsm X constraint) l
  (s, om)
input_valid X l (s, om)
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
l: label
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
Hiv: input_valid
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) l (
  s, om)
input_valid
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} l (s, om)
  apply VLSM_incl_input_valid; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
l: label
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
Hiv: input_valid
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) l (
  s, om)
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma input_valid_transition_constrained_vlsm :
  forall (l : label _) (som som' : state _ * option message),
    input_valid_transition (constrained_vlsm X constraint) l som som' ->
      input_valid_transition X l som som'.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (l : label (constrained_vlsm X constraint)) (som
                                               som' : 
                                               state
                                                 (constrained_vlsm
                                                 X
                                                 constraint) *
                                               option
                                                 message),
  input_valid_transition
    (constrained_vlsm X constraint) l som som'
  → input_valid_transition X l som som'
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (l : label (constrained_vlsm X constraint)) (som
                                               som' : 
                                               state
                                                 (constrained_vlsm
                                                 X
                                                 constraint) *
                                               option
                                                 message),
  input_valid_transition
    (constrained_vlsm X constraint) l som som'
  → input_valid_transition X l som som'
  intros l [s om] [s' om'] Hivt.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
l: label (constrained_vlsm X constraint)
s: state (constrained_vlsm X constraint)
om: option message
s': state (constrained_vlsm X constraint)
om': option message
Hivt: input_valid_transition
  (constrained_vlsm X constraint) l (
  s, om) (s', om')
input_valid_transition X l (s, om) (s', om')
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
l: label
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
s': state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om': option message
Hivt: input_valid_transition
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) l (
  s, om) (s', om')
input_valid_transition
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} l (s, om) (s', om')
  apply VLSM_incl_input_valid_transition; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
l: label
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
s': state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om': option message
Hivt: input_valid_transition
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) l (
  s, om) (s', om')
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma option_can_produce_constrained_vlsm :
  forall (s : state _) (om : option message),
    option_can_produce (constrained_vlsm X constraint) s om ->
      option_can_produce X s om.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (om : 
                                               option
                                                 message),
  option_can_produce (constrained_vlsm X constraint) s
    om → option_can_produce X s om
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (om : 
                                               option
                                                 message),
  option_can_produce (constrained_vlsm X constraint) s
    om → option_can_produce X s om
  intros s om Hocp.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
om: option message
Hocp: option_can_produce
  (constrained_vlsm X constraint) s om
option_can_produce X s om
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
Hocp: option_can_produce
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s om
option_can_produce
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s om
  eapply VLSM_incl_can_produce; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
om: option message
Hocp: option_can_produce
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s om
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma can_produce_constrained_vlsm :
  forall (s : state _) (m : message),
    can_produce (constrained_vlsm X constraint) s m ->
      can_produce X s m.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (m : message),
  can_produce (constrained_vlsm X constraint) s m
  → can_produce X s m
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (m : message),
  can_produce (constrained_vlsm X constraint) s m
  → can_produce X s m
  by intros; apply option_can_produce_constrained_vlsm.
Qed.

Lemma can_emit_constrained_vlsm :
  forall (m : message),
    can_emit (constrained_vlsm X constraint) m ->
      can_emit X m.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ m : message,
  can_emit (constrained_vlsm X constraint) m
  → can_emit X m
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ m : message,
  can_emit (constrained_vlsm X constraint) m
  → can_emit X m
  intros m Hce.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
m: message
Hce: can_emit (constrained_vlsm X constraint) m
can_emit X m
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
m: message
Hce: can_emit
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) m
can_emit
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} m
  eapply VLSM_incl_can_emit; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
m: message
Hce: can_emit
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) m
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma finite_valid_trace_from_constrained_vlsm :
  forall (s : state _) (tr : list transition_item),
    finite_valid_trace_from (constrained_vlsm X constraint) s tr ->
      finite_valid_trace_from X s tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               list
                                                 transition_item),
  finite_valid_trace_from
    (constrained_vlsm X constraint) s tr
  → finite_valid_trace_from X s tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               list
                                                 transition_item),
  finite_valid_trace_from
    (constrained_vlsm X constraint) s tr
  → finite_valid_trace_from X s tr
  intros s tr Hfvtf.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
tr: list transition_item
Hfvtf: finite_valid_trace_from
  (constrained_vlsm X constraint) s tr
finite_valid_trace_from X s tr
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvtf: finite_valid_trace_from
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
finite_valid_trace_from
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s tr
  apply VLSM_incl_finite_valid_trace_from; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvtf: finite_valid_trace_from
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma finite_valid_trace_constrained_vlsm :
  forall (s : state _) (tr : list transition_item),
    finite_valid_trace (constrained_vlsm X constraint) s tr ->
      finite_valid_trace X s tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               list
                                                 transition_item),
  finite_valid_trace (constrained_vlsm X constraint) s
    tr → finite_valid_trace X s tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               list
                                                 transition_item),
  finite_valid_trace (constrained_vlsm X constraint) s
    tr → finite_valid_trace X s tr
  intros s tr Hfvt.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
tr: list transition_item
Hfvt: finite_valid_trace
  (constrained_vlsm X constraint) s tr
finite_valid_trace X s tr
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvt: finite_valid_trace
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
finite_valid_trace
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s tr
  apply VLSM_incl_finite_valid_trace; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvt: finite_valid_trace
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma finite_valid_trace_from_to_constrained_vlsm :
  forall (s1 s2 : state _) (tr : list transition_item),
    finite_valid_trace_from_to (constrained_vlsm X constraint) s1 s2 tr ->
      finite_valid_trace_from_to X s1 s2 tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s1 s2 : state (constrained_vlsm X constraint)) 
  (tr : list transition_item),
  finite_valid_trace_from_to
    (constrained_vlsm X constraint) s1 s2 tr
  → finite_valid_trace_from_to X s1 s2 tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s1 s2 : state (constrained_vlsm X constraint)) 
  (tr : list transition_item),
  finite_valid_trace_from_to
    (constrained_vlsm X constraint) s1 s2 tr
  → finite_valid_trace_from_to X s1 s2 tr
  intros s1 s2 tr Hfvtft.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s1, s2: state (constrained_vlsm X constraint)
tr: list transition_item
Hfvtft: finite_valid_trace_from_to
  (constrained_vlsm X constraint) s1 s2 tr
finite_valid_trace_from_to X s1 s2 tr
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s1, s2: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvtft: finite_valid_trace_from_to
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s1 s2 tr
finite_valid_trace_from_to
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s1 s2 tr
  apply VLSM_incl_finite_valid_trace_from_to; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s1, s2: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvtft: finite_valid_trace_from_to
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s1 s2 tr
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma finite_valid_trace_init_to_constrained_vlsm :
  forall (s1 s2 : state _) (tr : list transition_item),
    finite_valid_trace_init_to (constrained_vlsm X constraint) s1 s2 tr ->
      finite_valid_trace_init_to X s1 s2 tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s1 s2 : state (constrained_vlsm X constraint)) 
  (tr : list transition_item),
  finite_valid_trace_init_to
    (constrained_vlsm X constraint) s1 s2 tr
  → finite_valid_trace_init_to X s1 s2 tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s1 s2 : state (constrained_vlsm X constraint)) 
  (tr : list transition_item),
  finite_valid_trace_init_to
    (constrained_vlsm X constraint) s1 s2 tr
  → finite_valid_trace_init_to X s1 s2 tr
  intros s1 s2 tr Hfvtit.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s1, s2: state (constrained_vlsm X constraint)
tr: list transition_item
Hfvtit: finite_valid_trace_init_to
  (constrained_vlsm X constraint) s1 s2 tr
finite_valid_trace_init_to X s1 s2 tr
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s1, s2: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvtit: finite_valid_trace_init_to
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s1 s2 tr
finite_valid_trace_init_to
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s1 s2 tr
  apply VLSM_incl_finite_valid_trace_init_to; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s1, s2: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: list transition_item
Hfvtit: finite_valid_trace_init_to
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s1 s2 tr
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma finite_valid_trace_init_to_emit_constrained_vlsm :
  forall (s1 s2 : state _) (om : option message) (tr : list transition_item),
    finite_valid_trace_init_to_emit (constrained_vlsm X constraint) s1 s2 om tr ->
      finite_valid_trace_init_to_emit X s1 s2 om tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s1 s2 : state (constrained_vlsm X constraint)) 
  (om : option message) (tr : list transition_item),
  finite_valid_trace_init_to_emit
    (constrained_vlsm X constraint) s1 s2 om tr
  → finite_valid_trace_init_to_emit X s1 s2 om tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s1 s2 : state (constrained_vlsm X constraint)) 
  (om : option message) (tr : list transition_item),
  finite_valid_trace_init_to_emit
    (constrained_vlsm X constraint) s1 s2 om tr
  → finite_valid_trace_init_to_emit X s1 s2 om tr
  induction 1; cbn; [by constructor |].message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
is, s: state (constrained_vlsm X constraint)
_om: option message
tl: list transition_item
H: finite_valid_trace_init_to_emit
  (constrained_vlsm X constraint) is s _om tl
iom_is, iom_s: state (constrained_vlsm X constraint)
iom: option message
iom_tl: list transition_item
H0: finite_valid_trace_init_to_emit
  (constrained_vlsm X constraint) iom_is iom_s
  iom iom_tl
l: label (constrained_vlsm X constraint)
Hv: valid l (s, iom)
s': state (constrained_vlsm X constraint)
oom: option message
Ht: transition l (s, iom) = (s', oom)
IHfinite_valid_trace_init_to_emit1: finite_valid_trace_init_to_emit
  X is s _om tl
IHfinite_valid_trace_init_to_emit2: finite_valid_trace_init_to_emit
  X iom_is iom_s
  iom iom_tl
finite_valid_trace_init_to_emit X is s' oom
  (tl ++
   [{|
      l := l;
      input := iom;
      destination := s';
      output := oom
    |}])
  by destruct Hv; econstructor.
Qed.

Lemma empty_initial_message_or_final_output_constrained_vlsm :
  forall (tr : list transition_item) (om : option message),
    empty_initial_message_or_final_output (constrained_vlsm X constraint) tr om ->
      empty_initial_message_or_final_output X tr om.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (tr : list transition_item) (om : option message),
  empty_initial_message_or_final_output
    (constrained_vlsm X constraint) tr om
  → empty_initial_message_or_final_output X tr om
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (tr : list transition_item) (om : option message),
  empty_initial_message_or_final_output
    (constrained_vlsm X constraint) tr om
  → empty_initial_message_or_final_output X tr om
  intros tr om.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
tr: list transition_item
om: option message
empty_initial_message_or_final_output
  (constrained_vlsm X constraint) tr om
→ empty_initial_message_or_final_output X tr om
  unfold empty_initial_message_or_final_output; cbn.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
tr: list transition_item
om: option message
match ListExtras.has_last_or_null tr with
| inleft (existT x (x0 ↾ _)) => output x0 = om
| inright _ =>
    option_initial_message_prop
      (constrained_vlsm_machine X constraint) om
end
→ match ListExtras.has_last_or_null tr with
  | inleft (existT x (x0 ↾ _)) => output x0 = om
  | inright _ => option_initial_message_prop X om
  end
  by case_match.
Qed.

Lemma infinite_valid_trace_from_constrained_vlsm :
  forall (s : state _) (tr : Stream transition_item),
    infinite_valid_trace_from (constrained_vlsm X constraint) s tr ->
      infinite_valid_trace_from X s tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               Stream
                                                 transition_item),
  infinite_valid_trace_from
    (constrained_vlsm X constraint) s tr
  → infinite_valid_trace_from X s tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               Stream
                                                 transition_item),
  infinite_valid_trace_from
    (constrained_vlsm X constraint) s tr
  → infinite_valid_trace_from X s tr
  intros s tr Hivtf.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
tr: Stream transition_item
Hivtf: infinite_valid_trace_from
  (constrained_vlsm X constraint) s tr
infinite_valid_trace_from X s tr
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: Stream transition_item
Hivtf: infinite_valid_trace_from
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
infinite_valid_trace_from
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s tr
  apply VLSM_incl_infinite_valid_trace_from; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: Stream transition_item
Hivtf: infinite_valid_trace_from
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma infinite_valid_trace_constrained_vlsm :
  forall (s : state _) (tr : Stream transition_item),
    infinite_valid_trace (constrained_vlsm X constraint) s tr ->
      infinite_valid_trace X s tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               Stream
                                                 transition_item),
  infinite_valid_trace (constrained_vlsm X constraint)
    s tr → infinite_valid_trace X s tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ (s : state (constrained_vlsm X constraint)) (tr : 
                                               Stream
                                                 transition_item),
  infinite_valid_trace (constrained_vlsm X constraint)
    s tr → infinite_valid_trace X s tr
  intros s tr Hivt.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
tr: Stream transition_item
Hivt: infinite_valid_trace
  (constrained_vlsm X constraint) s tr
infinite_valid_trace X s tr
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: Stream transition_item
Hivt: infinite_valid_trace
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
infinite_valid_trace
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s tr
  apply VLSM_incl_infinite_valid_trace; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
tr: Stream transition_item
Hivt: infinite_valid_trace
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s tr
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma valid_trace_from_prop_constrained_vlsm :
  forall (tr : Trace),
    valid_trace_from_prop (constrained_vlsm X constraint) tr ->
      valid_trace_from_prop X tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ tr : Trace,
  valid_trace_from_prop
    (constrained_vlsm X constraint) tr
  → valid_trace_from_prop X tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ tr : Trace,
  valid_trace_from_prop
    (constrained_vlsm X constraint) tr
  → valid_trace_from_prop X tr
  intros [] Hvtfp; cbn.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
l: list transition_item
Hvtfp: valid_trace_from_prop
  (constrained_vlsm X constraint) 
  (Finite s l)
finite_valid_trace_from X s l
message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
s0: Stream transition_item
Hvtfp: valid_trace_from_prop
  (constrained_vlsm X constraint)
  (Infinite s s0)
infinite_valid_trace_from X s s0
  -message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
l: list transition_item
Hvtfp: valid_trace_from_prop
  (constrained_vlsm X constraint) 
  (Finite s l)
finite_valid_trace_from X s l by apply finite_valid_trace_from_constrained_vlsm.
  -message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s: state (constrained_vlsm X constraint)
s0: Stream transition_item
Hvtfp: valid_trace_from_prop
  (constrained_vlsm X constraint)
  (Infinite s s0)
infinite_valid_trace_from X s s0 by apply infinite_valid_trace_from_constrained_vlsm.
Qed.

Lemma valid_trace_prop_constrained_vlsm :
  forall (tr : Trace),
    valid_trace_prop (constrained_vlsm X constraint) tr ->
      valid_trace_prop X tr.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ tr : Trace,
  valid_trace_prop (constrained_vlsm X constraint) tr
  → valid_trace_prop X tr
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ tr : Trace,
  valid_trace_prop (constrained_vlsm X constraint) tr
  → valid_trace_prop X tr
  intros tr Hvtp.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
tr: Trace
Hvtp: valid_trace_prop
  (constrained_vlsm X constraint) tr
valid_trace_prop X tr
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
tr: Trace
Hvtp: valid_trace_prop
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) tr
valid_trace_prop
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} tr
  apply VLSM_incl_valid_trace; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
tr: Trace
Hvtp: valid_trace_prop
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) tr
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

Lemma in_futures_constrained_vlsm :
  forall (s1 s2 : state _),
    in_futures (constrained_vlsm X constraint) s1 s2 ->
      in_futures X s1 s2.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ s1 s2 : state (constrained_vlsm X constraint),
  in_futures (constrained_vlsm X constraint) s1 s2
  → in_futures X s1 s2
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ s1 s2 : state (constrained_vlsm X constraint),
  in_futures (constrained_vlsm X constraint) s1 s2
  → in_futures X s1 s2
  intros s1 s2 Hif.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
s1, s2: state (constrained_vlsm X constraint)
Hif: in_futures (constrained_vlsm X constraint) s1 s2
in_futures X s1 s2
  destruct X.message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s1, s2: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
Hif: in_futures
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s1 s2
in_futures
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |} s1 s2
  apply VLSM_incl_in_futures; [| done].message: Type
X: VLSM message
vlsm_type: VLSMType message
vlsm_machine: VLSMMachine vlsm_type
constraint: label
  {|
    vlsm_type := vlsm_type;
    vlsm_machine := vlsm_machine
  |}
→ state
    {|
      vlsm_type := vlsm_type;
      vlsm_machine := vlsm_machine
    |} * option message → Prop
s1, s2: state
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint)
Hif: in_futures
  (constrained_vlsm
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) s1 s2
VLSM_incl_part
  (constrained_vlsm_machine
     {|
       vlsm_type := vlsm_type;
       vlsm_machine := vlsm_machine
     |} constraint) vlsm_machine
  by apply (VLSM_incl_constrained_vlsm {| vlsm_type := vlsm_type; vlsm_machine := vlsm_machine; |}).
Qed.

End sec_constrained_vlsm_lemmas.

Section sec_constrained_vlsm_commutation_lemmas.

Lemma constrained_preloaded_comm :
  forall `(X : VLSM message) (constraint : label X -> state X * option message -> Prop)
    (initial : message -> Prop),
      VLSM_eq
        (constrained_vlsm (preloaded_vlsm X initial) constraint)
        (preloaded_vlsm (constrained_vlsm X constraint) initial).∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop) (initial : 
                                                 message
                                                 → Prop),
  VLSM_eq
    (constrained_vlsm (preloaded_vlsm X initial)
       constraint)
    (preloaded_vlsm (constrained_vlsm X constraint)
       initial)
Proof.∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop) (initial : 
                                                 message
                                                 → Prop),
  VLSM_eq
    (constrained_vlsm (preloaded_vlsm X initial)
       constraint)
    (preloaded_vlsm (constrained_vlsm X constraint)
       initial)
  intros message X.message: Type
X: VLSM message
∀ (constraint : label X
                → state X * option message → Prop) 
  (initial : message → Prop),
  VLSM_eq
    (constrained_vlsm (preloaded_vlsm X initial)
       constraint)
    (preloaded_vlsm (constrained_vlsm X constraint)
       initial)
  rewrite <- (mk_vlsm_machine X); cbn.message: Type
X: VLSM message
∀ (constraint : label X
                → state X * option message → Prop) 
  (initial : message → Prop),
  VLSM_eq_part
    (constrained_vlsm_machine
       (preloaded_vlsm
          {| vlsm_type := X; vlsm_machine := X |}
          initial) constraint)
    (preloaded_vlsm_machine
       (constrained_vlsm
          {| vlsm_type := X; vlsm_machine := X |}
          constraint) initial)
  intros constraint initial.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
initial: message → Prop
VLSM_eq_part
  (constrained_vlsm_machine
     (preloaded_vlsm
        {| vlsm_type := X; vlsm_machine := X |}
        initial) constraint)
  (preloaded_vlsm_machine
     (constrained_vlsm
        {| vlsm_type := X; vlsm_machine := X |}
        constraint) initial)
  by split; apply (VLSM_incl_embedding_iff (constrained_vlsm_machine
    (preloaded_vlsm X initial) constraint)), basic_VLSM_strong_embedding; red; cbn.
Qed.

Lemma VLSM_incl_constrained_preloaded :
  forall `(X : VLSM message) (constraint : label X -> state X * option message -> Prop)
    (initial : message -> Prop),
      VLSM_incl
        (constrained_vlsm (preloaded_vlsm X initial) constraint)
        (preloaded_vlsm (constrained_vlsm X constraint) initial).∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop) (initial : 
                                                 message
                                                 → Prop),
  VLSM_incl
    (constrained_vlsm (preloaded_vlsm X initial)
       constraint)
    (preloaded_vlsm (constrained_vlsm X constraint)
       initial)
Proof.∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop) (initial : 
                                                 message
                                                 → Prop),
  VLSM_incl
    (constrained_vlsm (preloaded_vlsm X initial)
       constraint)
    (preloaded_vlsm (constrained_vlsm X constraint)
       initial)
  by intros; apply constrained_preloaded_comm.
Qed.

Lemma VLSM_incl_preloaded_constrained :
  forall `(X : VLSM message) (constraint : label X -> state X * option message -> Prop)
    (initial : message -> Prop),
      VLSM_incl
        (preloaded_vlsm (constrained_vlsm X constraint) initial)
        (constrained_vlsm (preloaded_vlsm X initial) constraint).∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop) (initial : 
                                                 message
                                                 → Prop),
  VLSM_incl
    (preloaded_vlsm (constrained_vlsm X constraint)
       initial)
    (constrained_vlsm (preloaded_vlsm X initial)
       constraint)
Proof.∀ (message : Type) (X : VLSM message) (constraint : 
                                       label X
                                       → state X *
                                         option
                                           message
                                         → Prop) (initial : 
                                                 message
                                                 → Prop),
  VLSM_incl
    (preloaded_vlsm (constrained_vlsm X constraint)
       initial)
    (constrained_vlsm (preloaded_vlsm X initial)
       constraint)
  by intros; apply constrained_preloaded_comm.
Qed.

End sec_constrained_vlsm_commutation_lemmas.

Section sec_constraint_subsumption.

Context
  `(X : VLSM message)
  (constraint : label X -> state X * option message -> Prop)
  .

Lemma constrained_preloaded_vlsm_incl_preloaded_with_all_messages :
  forall (P : message -> Prop),
    VLSM_incl
      (preloaded_vlsm (constrained_vlsm X constraint) P)
      (preloaded_with_all_messages_vlsm X).message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ P : message → Prop,
  VLSM_incl
    (preloaded_vlsm (constrained_vlsm X constraint) P)
    (preloaded_with_all_messages_vlsm X)
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
∀ P : message → Prop,
  VLSM_incl
    (preloaded_vlsm (constrained_vlsm X constraint) P)
    (preloaded_with_all_messages_vlsm X)
  by intros; apply basic_VLSM_strong_incl; cbv; [| itauto.. |].
Qed.

Lemma constrained_preloaded_incl :
  VLSM_incl (constrained_vlsm X constraint) (preloaded_with_all_messages_vlsm X).message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_incl (constrained_vlsm X constraint)
  (preloaded_with_all_messages_vlsm X)
Proof.message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_incl (constrained_vlsm X constraint)
  (preloaded_with_all_messages_vlsm X)
  apply (@VLSM_incl_trans _ _ _ X).message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_incl
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint
  |} {| vlsm_type := X; vlsm_machine := X |}
message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_incl {| vlsm_type := X; vlsm_machine := X |}
  {|
    vlsm_type := X;
    vlsm_machine :=
      preloaded_vlsm_machine X (λ _ : message, True)
  |}
  -message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_incl
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint
  |} {| vlsm_type := X; vlsm_machine := X |} by cbn; apply VLSM_incl_constrained_vlsm.
  -message: Type
X: VLSM message
constraint: label X → state X * option message → Prop
VLSM_incl {| vlsm_type := X; vlsm_machine := X |}
  {|
    vlsm_type := X;
    vlsm_machine :=
      preloaded_vlsm_machine X (λ _ : message, True)
  |} by apply (vlsm_incl_preloaded_with_all_messages_vlsm X).
Qed.

Context
  (constraint1 constraint2 : label X -> state X * option message -> Prop)
  (X1 := constrained_vlsm X constraint1)
  (X2 := constrained_vlsm X constraint2)
  .

A constraint1 is subsumed by constraint2 if constraint1 is stronger than constraint2 for any input.

Definition strong_constraint_subsumption : Prop :=
  forall (l : label X) (som : state X * option message),
    constraint1 l som -> constraint2 l som.

A weaker version of strong_constraint_subsumption requiring input_validity w.r.t. preloaded_with_all_messages_vlsm as a precondition for the subsumption property.

This definition is useful in proving VLSM_inclusions between VLSMs preloaded with all messages (Lemma preloaded_constraint_subsumption_incl).

Although there are currently no explicit cases for its usage, it might be more useful than the strong_constraint_subsumption property in cases where proving constraint subsumption relies on the state being valid and/or the message being valid.

Definition preloaded_constraint_subsumption : Prop :=
  forall (l : label X) (som : state _ * option message),
    input_constrained (constrained_vlsm X constraint1) l som ->
      constraint2 l som.

A weaker version of preloaded_constraint_subsumption requiring input_validity as a precondition for the subsumption property.

This definition is usually useful in proving VLSM_inclusions between regular VLSMs (Lemma constraint_subsumption_incl).

It is more useful than the strong_constraint_subsumption property in cases where proving constraint subsumption relies on the state/message being valid and/or the message being valid (e.g., Lemma Fixed_incl_StrongFixed).

Definition input_valid_constraint_subsumption : Prop :=
  forall (l : label X) (som : state X * option message),
    input_valid (constrained_vlsm X constraint1) l som -> constraint2 l som.

The weakest form of constraint subsumption also requires that the input state and message are valid for the composition under the second constraint.

Definition weak_input_valid_constraint_subsumption : Prop :=
  forall (l : label X) (som : state X * option message),
    input_valid (constrained_vlsm X constraint1) l som ->
    valid_state_prop (constrained_vlsm X constraint2) som.1 ->
    option_valid_message_prop (constrained_vlsm X constraint2) som.2 ->
      constraint2 l som.

Let X1, X2 be two constrained VLSMs constraints constraint1 and constraint2, respectively. Further assume that constraint1 is subsumed by constraint2.

We will show that X1 is trace-included into X2 by applying the lemma basic_VLSM_incl.

Lemma weak_constraint_subsumption_incl
  (Hsubsumption : weak_input_valid_constraint_subsumption)
  : VLSM_incl X1 X2.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
VLSM_incl X1 X2
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
VLSM_incl X1 X2
  apply basic_VLSM_incl.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
strong_incl_initial_state_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2)
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
weak_incl_initial_message_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2)
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
weak_incl_valid_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2)
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
weak_incl_transition_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2)
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
strong_incl_initial_state_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2) by intros s Hs.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
weak_incl_initial_message_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2) by intros _ _ m _ _ Hm; apply initial_message_is_valid.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
weak_incl_valid_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2) by split; [apply Hv | auto].
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: weak_input_valid_constraint_subsumption
weak_incl_transition_preservation
  (constrained_vlsm_machine X constraint1)
  (constrained_vlsm_machine X constraint2) by intros l s om s' om' Ht; apply Ht.
Qed.

Lemma constraint_subsumption_input_valid
  (Hsubsumption : input_valid_constraint_subsumption)
  (l : label X1)
  (s : state X1)
  (om : option message)
  (Hv : input_valid X1 l (s, om))
  : valid X2 l (s, om).message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label X1
s: state X1
om: option message
Hv: input_valid X1 l (s, om)
valid l (s, om)
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label X1
s: state X1
om: option message
Hv: input_valid X1 l (s, om)
valid l (s, om)
  by split; [apply Hv | apply Hsubsumption].
Qed.

Lemma constraint_subsumption_valid_state_message_preservation
  (Hsubsumption : input_valid_constraint_subsumption)
  (s : state X1)
  (om : option message)
  (Hps : valid_state_message_prop X1 s om)
  : valid_state_message_prop X2 s om.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
s: state X1
om: option message
Hps: valid_state_message_prop X1 s om
valid_state_message_prop X2 s om
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
s: state X1
om: option message
Hps: valid_state_message_prop X1 s om
valid_state_message_prop X2 s om
  induction Hps; [by apply valid_initial_state_message |].message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
s: state X1
_om: option message
Hps1: valid_state_message_prop X1 s _om
_s: state X1
om: option message
Hps2: valid_state_message_prop X1 _s om
l: label X1
Hv: valid l (s, om)
s': state X1
om': option message
Ht: transition l (s, om) = (s', om')
IHHps1: valid_state_message_prop X2 s _om
IHHps2: valid_state_message_prop X2 _s om
valid_state_message_prop X2 s' om'
  apply (valid_generated_state_message X2) with s _om _s om l; only 1-2, 4: done.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
s: state X1
_om: option message
Hps1: valid_state_message_prop X1 s _om
_s: state X1
om: option message
Hps2: valid_state_message_prop X1 _s om
l: label X1
Hv: valid l (s, om)
s': state X1
om': option message
Ht: transition l (s, om) = (s', om')
IHHps1: valid_state_message_prop X2 s _om
IHHps2: valid_state_message_prop X2 _s om
valid l (s, om)
  apply constraint_subsumption_input_valid; [done |].message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
s: state X1
_om: option message
Hps1: valid_state_message_prop X1 s _om
_s: state X1
om: option message
Hps2: valid_state_message_prop X1 _s om
l: label X1
Hv: valid l (s, om)
s': state X1
om': option message
Ht: transition l (s, om) = (s', om')
IHHps1: valid_state_message_prop X2 s _om
IHHps2: valid_state_message_prop X2 _s om
input_valid X1 l (s, om)
  by split_and!; [exists _om | exists _s |].
Qed.

Lemma constraint_subsumption_incl
  (Hsubsumption : input_valid_constraint_subsumption)
  : VLSM_incl X1 X2.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
VLSM_incl X1 X2
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
VLSM_incl X1 X2
  apply basic_VLSM_incl; intro; intros.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
H: initial_state_prop s
initial_state_prop (id s)
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
m: message
Hv: input_valid
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |} l (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} m
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |} l (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} om
valid (id l) (id s, om)
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
om: option message
s': state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
om': option message
H: input_valid_transition
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |} l (s, om) (s', om')
transition (id l) (id s, om) = (id s', om')
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
H: initial_state_prop s
initial_state_prop (id s) done.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
m: message
Hv: input_valid
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |} l (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} m by apply initial_message_is_valid.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |} l (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint2
  |} om
valid (id l) (id s, om) by apply constraint_subsumption_input_valid.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
l: label
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
s: state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
om: option message
s': state
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |}
om': option message
H: input_valid_transition
  {|
    vlsm_type := X;
    vlsm_machine :=
      constrained_vlsm_machine X constraint1
  |} l (s, om) (s', om')
transition (id l) (id s, om) = (id s', om') by apply H.
Qed.

Lemma preloaded_constraint_subsumption_input_valid
  (Hpre_subsumption : preloaded_constraint_subsumption)
  (l : label X1)
  (s : state X1)
  (om : option message)
  (Hv : input_constrained X1 l (s, om))
  : valid X2 l (s, om).message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label X1
s: state X1
om: option message
Hv: input_constrained X1 l (s, om)
valid l (s, om)
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label X1
s: state X1
om: option message
Hv: input_constrained X1 l (s, om)
valid l (s, om)
  by split; [apply Hv | apply Hpre_subsumption].
Qed.

Lemma preloaded_constraint_subsumption_incl
  (Hpre_subsumption : preloaded_constraint_subsumption)
  : VLSM_incl (preloaded_with_all_messages_vlsm X1) (preloaded_with_all_messages_vlsm X2).message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
VLSM_incl (preloaded_with_all_messages_vlsm X1)
  (preloaded_with_all_messages_vlsm X2)
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
VLSM_incl (preloaded_with_all_messages_vlsm X1)
  (preloaded_with_all_messages_vlsm X2)
  apply basic_VLSM_incl; intro; intros; [done | | | apply H].message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
m: message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2
        (λ _ : message, True)
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2 (λ _ : message, True)
  |} m
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2
        (λ _ : message, True)
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2
        (λ _ : message, True)
  |} om
valid (id l) (id s, om)
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
m: message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2
        (λ _ : message, True)
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2 (λ _ : message, True)
  |} m by apply initial_message_is_valid.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2
        (λ _ : message, True)
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X2
        (λ _ : message, True)
  |} om
valid (id l) (id s, om) by apply preloaded_constraint_subsumption_input_valid.
Qed.

Lemma preloaded_constraint_subsumption_incl_free :
  VLSM_incl
    (preloaded_with_all_messages_vlsm X1)
    (preloaded_with_all_messages_vlsm X).message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
VLSM_incl (preloaded_with_all_messages_vlsm X1)
  (preloaded_with_all_messages_vlsm X)
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
VLSM_incl (preloaded_with_all_messages_vlsm X1)
  (preloaded_with_all_messages_vlsm X)
  apply basic_VLSM_incl; intro; intros; [done | ..].message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
m: message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X (λ _ : message, True)
  |} m
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} om
valid (id l) (id s, om)
message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om: option message
s': state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om': option message
H: input_valid_transition
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, om) (s', om')
transition (id l) (id s, om) = (id s', om')
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
m: message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, Some m)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (id s)
HmX: initial_message_prop m
valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X (λ _ : message, True)
  |} m by apply initial_message_is_valid.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om: option message
Hv: input_valid
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, om)
HsY: valid_state_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} (id s)
HomY: option_valid_message_prop
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X
        (λ _ : message, True)
  |} om
valid (id l) (id s, om) by apply Hv.
  -message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
l: label
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
s: state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om: option message
s': state
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |}
om': option message
H: input_valid_transition
  {|
    vlsm_type := X1;
    vlsm_machine :=
      preloaded_vlsm_machine X1
        (λ _ : message, True)
  |} l (s, om) (s', om')
transition (id l) (id s, om) = (id s', om') by apply H.
Qed.

Lemma weak_constraint_subsumption_weakest
  (Hsubsumption : input_valid_constraint_subsumption)
  : weak_input_valid_constraint_subsumption.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
weak_input_valid_constraint_subsumption
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hsubsumption: input_valid_constraint_subsumption
weak_input_valid_constraint_subsumption
  by intros l som Hv _ _; auto.
Qed.

Lemma preloaded_constraint_subsumption_stronger
  (Hpre_subsumption : preloaded_constraint_subsumption)
  : input_valid_constraint_subsumption.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
input_valid_constraint_subsumption
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
input_valid_constraint_subsumption
  intros l som Hv.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label X
som: (state X * option message)%type
Hv: input_valid (constrained_vlsm X constraint1) l
  som
constraint2 l som
  apply Hpre_subsumption.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label X
som: (state X * option message)%type
Hv: input_valid (constrained_vlsm X constraint1) l
  som
input_constrained (constrained_vlsm X constraint1) l
  som
  destruct som.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label X
s: state X
o: option message
Hv: input_valid (constrained_vlsm X constraint1) l
  (s, o)
input_constrained (constrained_vlsm X constraint1) l
  (s, o)
  eapply VLSM_incl_input_valid; [| done].message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
l: label X
s: state X
o: option message
Hv: input_valid (constrained_vlsm X constraint1) l
  (s, o)
VLSM_incl_part
  (constrained_vlsm_machine X constraint1)
  (preloaded_vlsm_machine
     (constrained_vlsm X constraint1)
     (λ _ : message, True))
  by apply (vlsm_incl_preloaded_with_all_messages_vlsm X1).
Qed.

Lemma strong_constraint_subsumption_strongest
  (Hstrong_subsumption : strong_constraint_subsumption)
  : preloaded_constraint_subsumption.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hstrong_subsumption: strong_constraint_subsumption
preloaded_constraint_subsumption
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hstrong_subsumption: strong_constraint_subsumption
preloaded_constraint_subsumption
  intros l [s om] (_ & _ & _ & Hc).message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hstrong_subsumption: strong_constraint_subsumption
l: label X
s: state
  (preloaded_with_all_messages_vlsm
     (constrained_vlsm X constraint1))
om: option message
Hc: constraint1 l (s, om)
constraint2 l (s, om)
  by apply Hstrong_subsumption.
Qed.

Lemma constraint_subsumption_byzantine_message_prop
  (Hpre_subsumption : preloaded_constraint_subsumption)
  (m : message)
  (Hm : byzantine_message_prop X1 m)
  : byzantine_message_prop X2 m.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
m: message
Hm: byzantine_message_prop X1 m
byzantine_message_prop X2 m
Proof.message: Type
X: VLSM message
constraint, constraint1, constraint2: label X
→ state X * option message → Prop
X1:= constrained_vlsm X constraint1: VLSM message
X2:= constrained_vlsm X constraint2: VLSM message
Hpre_subsumption: preloaded_constraint_subsumption
m: message
Hm: byzantine_message_prop X1 m
byzantine_message_prop X2 m
  by apply (VLSM_incl_can_emit (preloaded_constraint_subsumption_incl Hpre_subsumption)).
Qed.

End sec_constraint_subsumption.