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 Coq Require Import FunctionalExtensionality.
From stdpp Require Import prelude.
From VLSM.Lib Require Import Preamble ListExtras.
From VLSM.Core Require Import VLSM PreloadedVLSM Composition.

Class HistoryVLSM `(X : VLSM message) : Prop :=
{
  not_valid_transition_next_initial :
    forall s2, initial_state_prop X s2 ->
    forall s1, ~ valid_transition_next X s1 s2;
  unique_transition_to_state :
    forall [s : state X],
    forall [l1 s1 iom1 oom1], valid_transition X l1 s1 iom1 s oom1 ->
    forall [l2 s2 iom2 oom2], valid_transition X l2 s2 iom2 s oom2 ->
    l1 = l2 /\ s1 = s2 /\ iom1 = iom2 /\ oom1 = oom2;
}.

#[global] Hint Mode HistoryVLSM - ! : typeclass_instances.

Section sec_history_vlsm_preloaded.

Context
  `{HistoryVLSM message X}
  .

#[export] Instance preloaded_history_vlsm :
  HistoryVLSM (preloaded_with_all_messages_vlsm X).
message: Type
X: VLSM message
H: HistoryVLSM X
HistoryVLSM (preloaded_with_all_messages_vlsm X)
Proof.
message: Type
X: VLSM message
H: HistoryVLSM X
HistoryVLSM (preloaded_with_all_messages_vlsm X)
  split; intros.
message: Type
X: VLSM message
H: HistoryVLSM X
s2: state (preloaded_with_all_messages_vlsm X)
H0: initial_state_prop s2
s1: state (preloaded_with_all_messages_vlsm X)
¬ valid_transition_next
    (preloaded_with_all_messages_vlsm X) s1 s2
message: Type
X: VLSM message
H: HistoryVLSM X
s: state (preloaded_with_all_messages_vlsm X)
l1: label (preloaded_with_all_messages_vlsm X)
s1: state (preloaded_with_all_messages_vlsm X)
iom1, oom1: option message
H0: valid_transition
  (preloaded_with_all_messages_vlsm X) l1 s1 iom1
  s oom1
l2: label (preloaded_with_all_messages_vlsm X)
s2: state (preloaded_with_all_messages_vlsm X)
iom2, oom2: option message
H1: valid_transition
  (preloaded_with_all_messages_vlsm X) l2 s2 iom2
  s oom2
l1 = l2 ∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2
  -
message: Type
X: VLSM message
H: HistoryVLSM X
s2: state (preloaded_with_all_messages_vlsm X)
H0: initial_state_prop s2
s1: state (preloaded_with_all_messages_vlsm X)
¬ valid_transition_next
    (preloaded_with_all_messages_vlsm X) s1 s2 rewrite <- valid_transition_next_preloaded_iff.
message: Type
X: VLSM message
H: HistoryVLSM X
s2: state (preloaded_with_all_messages_vlsm X)
H0: initial_state_prop s2
s1: state (preloaded_with_all_messages_vlsm X)
¬ valid_transition_next X s1 s2
    by apply not_valid_transition_next_initial.
  -
message: Type
X: VLSM message
H: HistoryVLSM X
s: state (preloaded_with_all_messages_vlsm X)
l1: label (preloaded_with_all_messages_vlsm X)
s1: state (preloaded_with_all_messages_vlsm X)
iom1, oom1: option message
H0: valid_transition
  (preloaded_with_all_messages_vlsm X) l1 s1 iom1
  s oom1
l2: label (preloaded_with_all_messages_vlsm X)
s2: state (preloaded_with_all_messages_vlsm X)
iom2, oom2: option message
H1: valid_transition
  (preloaded_with_all_messages_vlsm X) l2 s2 iom2
  s oom2
l1 = l2 ∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2 by eapply (@unique_transition_to_state _ X);
      [| apply valid_transition_preloaded_iff..].
Qed.

Lemma history_unique_trace_to_reachable :
  forall is s tr,
    finite_constrained_trace_init_to X is s tr ->
  forall is' tr',
    finite_constrained_trace_init_to X is' s tr' ->
      is' = is /\ tr' = tr.
message: Type
X: VLSM message
H: HistoryVLSM X
∀ (is s : state (preloaded_with_all_messages_vlsm X)) 
  (tr : list transition_item),
  finite_constrained_trace_init_to X is s tr
  → ∀ (is' : state
               (preloaded_with_all_messages_vlsm X)) 
      (tr' : list transition_item),
      finite_constrained_trace_init_to X is' s tr'
      → is' = is ∧ tr' = tr
Proof.
message: Type
X: VLSM message
H: HistoryVLSM X
∀ (is s : state (preloaded_with_all_messages_vlsm X)) 
  (tr : list transition_item),
  finite_constrained_trace_init_to X is s tr
  → ∀ (is' : state
               (preloaded_with_all_messages_vlsm X)) 
      (tr' : list transition_item),
      finite_constrained_trace_init_to X is' s tr'
      → is' = is ∧ tr' = tr
  intros is s tr Htr; induction Htr using finite_valid_trace_init_to_rev_ind;
    intros is' tr' [Htr' His'].
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
Hsi: initial_state_prop si
is': state (preloaded_with_all_messages_vlsm X)
tr': list transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' si
  tr'
His': initial_state_prop is'
is' = si ∧ tr' = []
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr': list transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' sf
  tr'
His': initial_state_prop is'
is' = si
∧ tr' =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
  -
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
Hsi: initial_state_prop si
is': state (preloaded_with_all_messages_vlsm X)
tr': list transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' si
  tr'
His': initial_state_prop is'
is' = si ∧ tr' = [] destruct_list_last tr' tr'' item Heqtr'; [by inversion Htr' | subst].
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
Hsi: initial_state_prop si
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
item: transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' si
  (tr'' ++ [item])
His': initial_state_prop is'
is' = si ∧ tr'' ++ [item] = []
    apply finite_valid_trace_from_to_app_split in Htr' as [_ Hitem].
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
Hsi: initial_state_prop si
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
item: transition_item
Hitem: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X)
  (finite_trace_last is' tr'') si [item]
His': initial_state_prop is'
is' = si ∧ tr'' ++ [item] = []
    inversion Hitem; inversion Htl; subst.
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
Hsi: initial_state_prop si
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hitem: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X)
  (finite_trace_last is' tr'') si
  [{|
     l := l;
     input := iom;
     destination := si;
     output := oom
   |}]
His': initial_state_prop is'
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l
  (finite_trace_last is' tr'', iom) (
  si, oom)
Htl: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) si si []
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) si
is' = si
∧ tr'' ++
  [{|
     l := l;
     input := iom;
     destination := si;
     output := oom
   |}] = []
    destruct Ht as [(_ & _ & Hv) Ht].
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
Hsi: initial_state_prop si
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hitem: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X)
  (finite_trace_last is' tr'') si
  [{|
     l := l;
     input := iom;
     destination := si;
     output := oom
   |}]
His': initial_state_prop is'
Hv: valid l (finite_trace_last is' tr'', iom)
Ht: transition l (finite_trace_last is' tr'', iom) =
(si, oom)
Htl: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) si si []
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) si
is' = si
∧ tr'' ++
  [{|
     l := l;
     input := iom;
     destination := si;
     output := oom
   |}] = []
    exfalso; clear His'; eapply @not_valid_transition_next_initial;
      [| done | by esplit].
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
Hsi: initial_state_prop si
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hitem: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X)
  (finite_trace_last is' tr'') si
  [{|
     l := l;
     input := iom;
     destination := si;
     output := oom
   |}]
Hv: valid l (finite_trace_last is' tr'', iom)
Ht: transition l (finite_trace_last is' tr'', iom) =
(si, oom)
Htl: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) si si []
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) si
HistoryVLSM (preloaded_with_all_messages_vlsm X)
    by typeclasses eauto.
  -
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr': list transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' sf
  tr'
His': initial_state_prop is'
is' = si
∧ tr' =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}] destruct_list_last tr' tr'' item Heqtr'; subst tr'.
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' sf
  []
His': initial_state_prop is'
is' = si
∧ [] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
item: transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' sf
  (tr'' ++ [item])
His': initial_state_prop is'
is' = si
∧ tr'' ++ [item] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
    +
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' sf
  []
His': initial_state_prop is'
is' = si
∧ [] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}] inversion Htr'; subst; clear Htr'.
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
His': initial_state_prop sf
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
sf = si
∧ [] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
      destruct Ht as [(_ & _ & Hv) Ht].
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (s, iom)
Ht: transition l (s, iom) = (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
His': initial_state_prop sf
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
sf = si
∧ [] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
      exfalso; eapply @not_valid_transition_next_initial; [| done | by esplit].
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Hv: valid l (s, iom)
Ht: transition l (s, iom) = (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
His': initial_state_prop sf
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
HistoryVLSM (preloaded_with_all_messages_vlsm X)
      by typeclasses eauto.
    +
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
item: transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is' sf
  (tr'' ++ [item])
His': initial_state_prop is'
is' = si
∧ tr'' ++ [item] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}] apply finite_valid_trace_from_to_app_split in Htr' as [Htr' Hitem].
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
item: transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is'
  (finite_trace_last is' tr'') tr''
Hitem: finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X)
  (finite_trace_last is' tr'') sf [item]
His': initial_state_prop is'
is' = si
∧ tr'' ++ [item] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
      inversion Hitem; inversion Htl; subst; clear Hitem Htl.
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l (
  s, iom) (sf, oom)
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is'
  (finite_trace_last is' tr'') tr''
iom0, oom0: option message
l0: label (preloaded_with_all_messages_vlsm X)
His': initial_state_prop is'
Ht0: input_valid_transition
  (preloaded_with_all_messages_vlsm X) l0
  (finite_trace_last is' tr'', iom0) (
  sf, oom0)
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
is' = si
∧ tr'' ++
  [{|
     l := l0;
     input := iom0;
     destination := sf;
     output := oom0
   |}] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
      apply input_valid_transition_forget_input in Ht, Ht0.
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: valid_transition
  (preloaded_with_all_messages_vlsm X) l s iom sf
  oom
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is'
  (finite_trace_last is' tr'') tr''
iom0, oom0: option message
l0: label (preloaded_with_all_messages_vlsm X)
His': initial_state_prop is'
Ht0: valid_transition
  (preloaded_with_all_messages_vlsm X) l0
  (finite_trace_last is' tr'') iom0 sf oom0
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
is' = si
∧ tr'' ++
  [{|
     l := l0;
     input := iom0;
     destination := sf;
     output := oom0
   |}] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
      specialize (unique_transition_to_state Ht Ht0) as Heqs.
message: Type
X: VLSM message
H: HistoryVLSM X
si, s: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si s tr
sf: state (preloaded_with_all_messages_vlsm X)
iom, oom: option message
l: label (preloaded_with_all_messages_vlsm X)
Ht: valid_transition
  (preloaded_with_all_messages_vlsm X) l s iom sf
  oom
IHHtr: ∀ (is' : state
           (preloaded_with_all_messages_vlsm X)) 
  (tr' : list transition_item),
  finite_constrained_trace_init_to X is' s tr'
  → is' = si ∧ tr' = tr
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is'
  (finite_trace_last is' tr'') tr''
iom0, oom0: option message
l0: label (preloaded_with_all_messages_vlsm X)
His': initial_state_prop is'
Ht0: valid_transition
  (preloaded_with_all_messages_vlsm X) l0
  (finite_trace_last is' tr'') iom0 sf oom0
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
Heqs: l = l0
∧ s = finite_trace_last is' tr''
  ∧ iom = iom0 ∧ oom = oom0
is' = si
∧ tr'' ++
  [{|
     l := l0;
     input := iom0;
     destination := sf;
     output := oom0
   |}] =
  tr ++
  [{|
     l := l;
     input := iom;
     destination := sf;
     output := oom
   |}]
      destruct_and! Heqs; subst.
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si
  (finite_trace_last is' tr'') tr
sf: state (preloaded_with_all_messages_vlsm X)
l0: label (preloaded_with_all_messages_vlsm X)
IHHtr: ∀ (is'0 : state
            (preloaded_with_all_messages_vlsm
               X)) (tr' : 
                    list transition_item),
  finite_constrained_trace_init_to X is'0
    (finite_trace_last is' tr'') tr'
  → is'0 = si ∧ tr' = tr
iom0, oom0: option message
Ht: valid_transition
  (preloaded_with_all_messages_vlsm X) l0
  (finite_trace_last is' tr'') iom0 sf oom0
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is'
  (finite_trace_last is' tr'') tr''
His': initial_state_prop is'
Ht0: valid_transition
  (preloaded_with_all_messages_vlsm X) l0
  (finite_trace_last is' tr'') iom0 sf oom0
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
is' = si
∧ tr'' ++
  [{|
     l := l0;
     input := iom0;
     destination := sf;
     output := oom0
   |}] =
  tr ++
  [{|
     l := l0;
     input := iom0;
     destination := sf;
     output := oom0
   |}]
      specialize (IHHtr _ _  (conj Htr' His')).
message: Type
X: VLSM message
H: HistoryVLSM X
si: state (preloaded_with_all_messages_vlsm X)
tr: list transition_item
is': state (preloaded_with_all_messages_vlsm X)
tr'': list transition_item
Htr: finite_valid_trace_init_to
  (preloaded_with_all_messages_vlsm X) si
  (finite_trace_last is' tr'') tr
sf: state (preloaded_with_all_messages_vlsm X)
l0: label (preloaded_with_all_messages_vlsm X)
IHHtr: is' = si ∧ tr'' = tr
iom0, oom0: option message
Ht: valid_transition
  (preloaded_with_all_messages_vlsm X) l0
  (finite_trace_last is' tr'') iom0 sf oom0
Htr': finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm X) is'
  (finite_trace_last is' tr'') tr''
His': initial_state_prop is'
Ht0: valid_transition
  (preloaded_with_all_messages_vlsm X) l0
  (finite_trace_last is' tr'') iom0 sf oom0
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm X) sf
is' = si
∧ tr'' ++
  [{|
     l := l0;
     input := iom0;
     destination := sf;
     output := oom0
   |}] =
  tr ++
  [{|
     l := l0;
     input := iom0;
     destination := sf;
     output := oom0
   |}]
      by destruct_and! IHHtr; subst.
Qed.

End sec_history_vlsm_preloaded.

Section sec_history_vlsm_composite.

Context
  {message : Type}
  `{EqDecision index}
  (IM : index -> VLSM message)
  `{forall i : index, HistoryVLSM (IM i)}
  (Free := free_composite_vlsm IM)
  .

Lemma not_composite_valid_transition_next_initial :
  forall s2, composite_initial_state_prop IM s2 ->
  forall s1, ~ composite_valid_transition_next IM s1 s2.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ s2 : composite_state IM,
  composite_initial_state_prop IM s2
  → ∀ s1 : state (free_composite_vlsm IM),
      ¬ composite_valid_transition_next IM s1 s2
Proof.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ s2 : composite_state IM,
  composite_initial_state_prop IM s2
  → ∀ s1 : state (free_composite_vlsm IM),
      ¬ composite_valid_transition_next IM s1 s2
  intros s2 Hs2 s1 [* Hs1].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s2: composite_state IM
Hs2: composite_initial_state_prop IM s2
s1: state (free_composite_vlsm IM)
l: label (free_composite_vlsm IM)
iom, oom: option message
Hs1: valid_transition (free_composite_vlsm IM) l s1
  iom s2 oom
False
  apply composite_valid_transition_projection, proj1, transition_next in Hs1; cbn in Hs1.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s2: composite_state IM
Hs2: composite_initial_state_prop IM s2
s1: state (free_composite_vlsm IM)
l: label (free_composite_vlsm IM)
iom, oom: option message
Hs1: valid_transition_next (IM (projT1 l))
  (s1 (projT1 l)) (s2 (projT1 l))
False
  by contradict Hs1; apply not_valid_transition_next_initial, Hs2.
Qed.

Lemma composite_quasi_unique_transition_to_state :
  forall [s],
  forall [l1 s1 iom1 oom1], composite_valid_transition IM l1 s1 iom1 s oom1 ->
  forall [l2 s2 iom2 oom2], composite_valid_transition IM l2 s2 iom2 s oom2 ->
  projT1 l1 = projT1 l2 ->
  l1 = l2 /\ s1 = s2 /\ iom1 = iom2 /\ oom1 = oom2.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ (s : state (free_composite_vlsm IM)) (l1 : label
                                               (free_composite_vlsm
                                                 IM)) 
  (s1 : state (free_composite_vlsm IM)) (iom1
                                         oom1 : option
                                                 message),
  composite_valid_transition IM l1 s1 iom1 s oom1
  → ∀ (l2 : label (free_composite_vlsm IM)) (s2 : 
                                             state
                                               (free_composite_vlsm
                                                 IM)) 
      (iom2 oom2 : option message),
      composite_valid_transition IM l2 s2 iom2 s oom2
      → projT1 l1 = projT1 l2
        → l1 = l2
          ∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2
Proof.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ (s : state (free_composite_vlsm IM)) (l1 : label
                                               (free_composite_vlsm
                                                 IM)) 
  (s1 : state (free_composite_vlsm IM)) (iom1
                                         oom1 : option
                                                 message),
  composite_valid_transition IM l1 s1 iom1 s oom1
  → ∀ (l2 : label (free_composite_vlsm IM)) (s2 : 
                                             state
                                               (free_composite_vlsm
                                                 IM)) 
      (iom2 oom2 : option message),
      composite_valid_transition IM l2 s2 iom2 s oom2
      → projT1 l1 = projT1 l2
        → l1 = l2
          ∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2
  intros ? [i li1] * Ht1 [_i li2] * Ht2 [=]; subst _i.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
li1: label (IM i)
s1: state (free_composite_vlsm IM)
iom1, oom1: option message
Ht1: composite_valid_transition IM 
  (existT i li1) s1 iom1 s oom1
li2: label (IM i)
s2: state (free_composite_vlsm IM)
iom2, oom2: option message
Ht2: composite_valid_transition IM 
  (existT i li2) s2 iom2 s oom2
existT i li1 = existT i li2
∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2
  apply composite_valid_transition_projection in Ht1, Ht2; cbn in Ht1, Ht2.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
li1: label (IM i)
s1: state (free_composite_vlsm IM)
iom1, oom1: option message
Ht1: valid_transition (IM i) li1 
  (s1 i) iom1 (s i) oom1
∧ s = state_update IM s1 i (s i)
li2: label (IM i)
s2: state (free_composite_vlsm IM)
iom2, oom2: option message
Ht2: valid_transition (IM i) li2 
  (s2 i) iom2 (s i) oom2
∧ s = state_update IM s2 i (s i)
existT i li1 = existT i li2
∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2
  destruct Ht1 as [Ht1 Heq_s], Ht2 as [Ht2 Heqs].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
li1: label (IM i)
s1: state (free_composite_vlsm IM)
iom1, oom1: option message
Ht1: valid_transition (IM i) li1 
  (s1 i) iom1 (s i) oom1
Heq_s: s = state_update IM s1 i (s i)
li2: label (IM i)
s2: state (free_composite_vlsm IM)
iom2, oom2: option message
Ht2: valid_transition (IM i) li2 
  (s2 i) iom2 (s i) oom2
Heqs: s = state_update IM s2 i (s i)
existT i li1 = existT i li2
∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2
  rewrite Heq_s in Heqs at 1; clear Heq_s.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
li1: label (IM i)
s1: state (free_composite_vlsm IM)
iom1, oom1: option message
Ht1: valid_transition (IM i) li1 
  (s1 i) iom1 (s i) oom1
li2: label (IM i)
s2: state (free_composite_vlsm IM)
iom2, oom2: option message
Ht2: valid_transition (IM i) li2 
  (s2 i) iom2 (s i) oom2
Heqs: state_update IM s1 i (s i) =
state_update IM s2 i (s i)
existT i li1 = existT i li2
∧ s1 = s2 ∧ iom1 = iom2 ∧ oom1 = oom2
  specialize (unique_transition_to_state Ht1 Ht2) as Heq;
    destruct_and! Heq; subst; repeat split.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
s1: state (free_composite_vlsm IM)
li2: label (IM i)
iom2, oom2: option message
Ht1: valid_transition (IM i) li2 
  (s1 i) iom2 (s i) oom2
s2: state (free_composite_vlsm IM)
Ht2: valid_transition (IM i) li2 
  (s2 i) iom2 (s i) oom2
Heqs: state_update IM s1 i (s i) =
state_update IM s2 i (s i)
H2: s1 i = s2 i
s1 = s2
  extensionality j.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
s1: state (free_composite_vlsm IM)
li2: label (IM i)
iom2, oom2: option message
Ht1: valid_transition (IM i) li2 
  (s1 i) iom2 (s i) oom2
s2: state (free_composite_vlsm IM)
Ht2: valid_transition (IM i) li2 
  (s2 i) iom2 (s i) oom2
Heqs: state_update IM s1 i (s i) =
state_update IM s2 i (s i)
H2: s1 i = s2 i
j: index
s1 j = s2 j
  destruct (decide (i = j)); subst; [done |].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
s1: state (free_composite_vlsm IM)
li2: label (IM i)
iom2, oom2: option message
Ht1: valid_transition (IM i) li2 
  (s1 i) iom2 (s i) oom2
s2: state (free_composite_vlsm IM)
Ht2: valid_transition (IM i) li2 
  (s2 i) iom2 (s i) oom2
Heqs: state_update IM s1 i (s i) =
state_update IM s2 i (s i)
H2: s1 i = s2 i
j: index
n: i ≠ j
s1 j = s2 j
  apply f_equal with (f := fun s => s j) in Heqs.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (free_composite_vlsm IM)
i: index
s1: state (free_composite_vlsm IM)
li2: label (IM i)
iom2, oom2: option message
Ht1: valid_transition (IM i) li2 
  (s1 i) iom2 (s i) oom2
s2: state (free_composite_vlsm IM)
Ht2: valid_transition (IM i) li2 
  (s2 i) iom2 (s i) oom2
j: index
Heqs: state_update IM s1 i (s i) j =
state_update IM s2 i (s i) j
H2: s1 i = s2 i
n: i ≠ j
s1 j = s2 j
  by state_update_simpl.
Qed.

Lemma composite_valid_transition_reflects_rechability :
  forall l s1 iom s2 oom,
  composite_valid_transition IM l s1 iom s2 oom ->
  constrained_state_prop Free s2 ->
  input_constrained_transition Free l (s1, iom) (s2, oom).
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ (l : label (free_composite_vlsm IM)) (s1 : state
                                               (free_composite_vlsm
                                                 IM)) 
  (iom : option message) (s2 : state
                                 (free_composite_vlsm
                                    IM)) (oom : option
                                                 message),
  composite_valid_transition IM l s1 iom s2 oom
  → constrained_state_prop Free s2
    → input_constrained_transition Free l (s1, iom)
        (s2, oom)
Proof.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ (l : label (free_composite_vlsm IM)) (s1 : state
                                               (free_composite_vlsm
                                                 IM)) 
  (iom : option message) (s2 : state
                                 (free_composite_vlsm
                                    IM)) (oom : option
                                                 message),
  composite_valid_transition IM l s1 iom s2 oom
  → constrained_state_prop Free s2
    → input_constrained_transition Free l (s1, iom)
        (s2, oom)
  intros * Hnext Hs2; revert l s1 iom oom Hnext.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s2: state (free_composite_vlsm IM)
Hs2: constrained_state_prop Free s2
∀ (l : label (free_composite_vlsm IM)) (s1 : state
                                               (free_composite_vlsm
                                                 IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s2 oom
  → input_constrained_transition Free l (s1, iom)
      (s2, oom)
  induction Hs2 using valid_state_prop_ind; intros * Hnext.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (preloaded_with_all_messages_vlsm Free)
Hs: initial_state_prop s
l: label (free_composite_vlsm IM)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM l s1 iom s oom
input_constrained_transition Free l (s1, iom) (s, oom)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
l: label (preloaded_with_all_messages_vlsm Free)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free) l
  (s, om) (s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
l0: label (free_composite_vlsm IM)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM l0 s1 iom s' oom
input_constrained_transition Free l0 (
  s1, iom) (s', oom)
  -
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (preloaded_with_all_messages_vlsm Free)
Hs: initial_state_prop s
l: label (free_composite_vlsm IM)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM l s1 iom s oom
input_constrained_transition Free l (s1, iom) (s, oom) apply transition_next in Hnext.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s: state (preloaded_with_all_messages_vlsm Free)
Hs: initial_state_prop s
l: label (free_composite_vlsm IM)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: valid_transition_next (free_composite_vlsm IM)
  s1 s
input_constrained_transition Free l (s1, iom) (s, oom)
    by contradict Hnext; apply not_composite_valid_transition_next_initial.
  -
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
l: label (preloaded_with_all_messages_vlsm Free)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free) l
  (s, om) (s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
l0: label (free_composite_vlsm IM)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM l0 s1 iom s' oom
input_constrained_transition Free l0 (s1, iom)
  (s', oom) destruct l as [i li], l0 as [j lj].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
    destruct (decide (i = j)).
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
e: i = j
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
n: i ≠ j
input_constrained_transition Free 
  (existT j lj) (s1, iom) (
  s', oom)
    +
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
e: i = j
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom) subst; apply input_valid_transition_forget_input in Ht as Hvt.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
j: index
li: label (IM j)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT j li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
Hvt: valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT j li) s om s' om'
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      apply composite_valid_transition_reachable_iff in Hvt.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
j: index
li: label (IM j)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT j li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
Hvt: composite_valid_transition IM 
  (existT j li) s om s' om'
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      specialize (composite_quasi_unique_transition_to_state Hnext Hvt eq_refl) as Heq.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
j: index
li: label (IM j)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT j li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
Hvt: composite_valid_transition IM 
  (existT j li) s om s' om'
Heq: existT j lj = existT j li
∧ s1 = s ∧ iom = om ∧ oom = om'
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      by destruct_and! Heq; simplify_eq.
    +
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
n: i ≠ j
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom) apply input_valid_transition_forget_input in Ht as Hti.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
n: i ≠ j
Hti: valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) s om s' om'
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      apply composite_valid_transition_reachable_iff,
        composite_valid_transition_projection in Hti;
        cbn in Hti; destruct Hti as [[Hvi Hti] Heqs'].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hnext: composite_valid_transition IM 
  (existT j lj) s1 iom s' oom
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': s' = state_update IM s i (s' i)
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      apply composite_valid_transition_projection in Hnext;
        cbn in Hnext; destruct Hnext as [[Hvj Htj] Heq_s'].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': s' = state_update IM s i (s' i)
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      rewrite Heq_s' in Heqs'; state_update_simpl.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
IHHs2: ∀ (l : label (free_composite_vlsm IM)) 
  (s1 : state (free_composite_vlsm IM)) 
  (iom oom : option message),
  composite_valid_transition IM l s1 iom s oom
  → input_constrained_transition Free l
      (s1, iom) (s, oom)
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      specialize (IHHs2 (existT j lj) (state_update IM s j (s1 j)) iom oom).
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      spec IHHs2.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
composite_valid_transition IM (existT j lj)
  (state_update IM s j (s1 j)) iom s oom
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
input_constrained_transition Free 
  (existT j lj) (s1, iom) (
  s', oom)
      {
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
composite_valid_transition IM (existT j lj)
  (state_update IM s j (s1 j)) iom s oom
        apply composite_valid_transition_projection_inv with (s1 j) (s' j); [done | |].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
state_update IM s j (s1 j) j = s1 j
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
s =
state_update IM (state_update IM s j (s1 j)) j (s' j)
        -
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
state_update IM s j (s1 j) j = s1 j by state_update_simpl.
        -
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
s =
state_update IM (state_update IM s j (s1 j)) j (s' j) rewrite state_update_twice.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
s = state_update IM s j (s' j)
          symmetry; apply state_update_id.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
s j = s' j
          apply f_equal with (f := fun s => s j) in Heqs'.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
IHHs2: composite_valid_transition IM 
  (existT j lj) (state_update IM s j (s1 j))
  iom s oom
→ input_constrained_transition Free
    (existT j lj)
    (state_update IM s j (s1 j), iom) (
    s, oom)
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) j =
state_update IM s i (s1 i) j
s j = s' j
          by state_update_simpl.
      }
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      assert (Hss1 : input_constrained_transition Free (existT i li)
                  (state_update IM s j (s1 j), om) (s1, om')).
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
input_constrained_transition Free (existT i li)
  (state_update IM s j (s1 j), om) (s1, om')
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
input_constrained_transition Free 
  (existT j lj) (s1, iom) (
  s', oom)
      {
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
input_constrained_transition Free (existT i li)
  (state_update IM s j (s1 j), om) (s1, om')
        repeat split; [by apply IHHs2 | by apply any_message_is_valid_in_preloaded | ..]
        ; cbn; state_update_simpl; [done |].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
(let (si', om') := transition li (s i, om) in
 (state_update IM (state_update IM s j (s1 j)) i si',
  om')) = (s1, om')
        replace (transition _ _ _) with (s' i, om').
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
(state_update IM (state_update IM s j (s1 j)) i (s' i),
 om') = (s1, om')
        f_equal; extensionality k; apply f_equal with (f := fun s => s k) in Heqs'.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
k: index
Heqs': state_update IM s1 j (s' j) k =
state_update IM s i (s1 i) k
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
state_update IM (state_update IM s j (s1 j)) i (s' i)
  k = s1 k
        rewrite Heq_s'.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
k: index
Heqs': state_update IM s1 j (s' j) k =
state_update IM s i (s1 i) k
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
state_update IM (state_update IM s j (s1 j)) i
  (state_update IM s1 j (s' j) i) k = s1 k
        by destruct (decide (i = k)), (decide (j = k)); subst; state_update_simpl.
      }
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
input_constrained_transition Free (existT j lj)
  (s1, iom) (s', oom)
      repeat split; cbn.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
valid_state_prop
  (preloaded_with_all_messages_vlsm Free) s1
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
option_valid_message_prop
  (preloaded_with_all_messages_vlsm Free) iom
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
valid lj (s1 j, iom)
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
(let (si', om') := transition lj (s1 j, iom) in
 (state_update IM s1 j si', om')) = (
s', oom)
      *
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
valid_state_prop
  (preloaded_with_all_messages_vlsm Free) s1 by eapply input_valid_transition_destination.
      *
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
option_valid_message_prop
  (preloaded_with_all_messages_vlsm Free) iom by apply any_message_is_valid_in_preloaded.
      *
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
valid lj (s1 j, iom) done.
      *
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s': state (preloaded_with_all_messages_vlsm Free)
i: index
li: label (IM i)
om, om': option message
s: state (preloaded_with_all_messages_vlsm Free)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm Free)
  (existT i li) (s, om) (
  s', om')
j: index
lj: label (IM j)
s1: state (free_composite_vlsm IM)
iom, oom: option message
Hvj: valid lj (s1 j, iom)
Htj: transition lj (s1 j, iom) = (s' j, oom)
Heq_s': s' = state_update IM s1 j (s' j)
n: i ≠ j
Hvi: valid li (s i, om)
Hti: transition li (s i, om) = (s' i, om')
Heqs': state_update IM s1 j (s' j) =
state_update IM s i (s1 i)
IHHs2: input_constrained_transition Free
  (existT j lj)
  (state_update IM s j (s1 j), iom) (
  s, oom)
Hss1: input_constrained_transition Free 
  (existT i li)
  (state_update IM s j (s1 j), om) (
  s1, om')
(let (si', om') := transition lj (s1 j, iom) in
 (state_update IM s1 j si', om')) = (s', oom) by replace (transition _ _ _) with (s' j, oom); f_equal.
Qed.

Lemma composite_valid_transition_next_reflects_rechability :
  forall s1 s2, composite_valid_transition_next IM s1 s2 ->
    constrained_state_prop Free s2 -> constrained_state_prop Free s1.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ s1 s2 : state (free_composite_vlsm IM),
  composite_valid_transition_next IM s1 s2
  → constrained_state_prop Free s2
    → constrained_state_prop Free s1
Proof.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ s1 s2 : state (free_composite_vlsm IM),
  composite_valid_transition_next IM s1 s2
  → constrained_state_prop Free s2
    → constrained_state_prop Free s1
  by intros s1 s2 []; eapply composite_valid_transition_reflects_rechability.
Qed.

Lemma composite_valid_transition_future_reflects_rechability :
  forall s1 s2, composite_valid_transition_future IM s1 s2 ->
    constrained_state_prop Free s2 -> constrained_state_prop Free s1.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ s1 s2 : composite_state IM,
  composite_valid_transition_future IM s1 s2
  → constrained_state_prop Free s2
    → constrained_state_prop Free s1
Proof.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ s1 s2 : composite_state IM,
  composite_valid_transition_future IM s1 s2
  → constrained_state_prop Free s2
    → constrained_state_prop Free s1 by apply tc_reflect, composite_valid_transition_next_reflects_rechability. Qed.

Lemma composite_valid_transitions_from_to_reflects_reachability :
  forall s s' tr,
  composite_valid_transitions_from_to IM s s' tr ->
  constrained_state_prop Free s' -> finite_constrained_trace_from_to Free s s' tr.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ (s s' : composite_state IM) (tr : list
                                      (composite_transition_item
                                         IM)),
  composite_valid_transitions_from_to IM s s' tr
  → constrained_state_prop Free s'
    → finite_constrained_trace_from_to Free s s' tr
Proof.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
∀ (s s' : composite_state IM) (tr : list
                                      (composite_transition_item
                                         IM)),
  composite_valid_transitions_from_to IM s s' tr
  → constrained_state_prop Free s'
    → finite_constrained_trace_from_to Free s s' tr
  induction 1; intros; [by constructor |].
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': composite_state IM
tr: list (composite_transition_item IM)
item: composite_transition_item IM
H0: composite_valid_transitions_from_to IM s s' tr
H1: composite_valid_transition_item IM s' item
IHcomposite_valid_transitions_from_to: constrained_state_prop
  Free s'
→ finite_constrained_trace_from_to
    Free s s' tr
H2: constrained_state_prop Free (destination item)
finite_constrained_trace_from_to Free s
  (destination item) (tr ++ [item])
  assert (Hitem : input_constrained_transition Free (l item) (s', input item)
                          (destination item, output item))
    by (apply composite_valid_transition_reflects_rechability; done).
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': composite_state IM
tr: list (composite_transition_item IM)
item: composite_transition_item IM
H0: composite_valid_transitions_from_to IM s s' tr
H1: composite_valid_transition_item IM s' item
IHcomposite_valid_transitions_from_to: constrained_state_prop
  Free s'
→ finite_constrained_trace_from_to
    Free s s' tr
H2: constrained_state_prop Free (destination item)
Hitem: input_constrained_transition Free 
  (l item) (
  s', input item)
  (destination item, output item)
finite_constrained_trace_from_to Free s
  (destination item) (tr ++ [item])
  eapply finite_valid_trace_from_to_app.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': composite_state IM
tr: list (composite_transition_item IM)
item: composite_transition_item IM
H0: composite_valid_transitions_from_to IM s s' tr
H1: composite_valid_transition_item IM s' item
IHcomposite_valid_transitions_from_to: constrained_state_prop
  Free s'
→ finite_constrained_trace_from_to
    Free s s' tr
H2: constrained_state_prop Free (destination item)
Hitem: input_constrained_transition Free 
  (l item) (
  s', input item)
  (destination item, output item)
finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Free) s ?m tr
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': composite_state IM
tr: list (composite_transition_item IM)
item: composite_transition_item IM
H0: composite_valid_transitions_from_to IM s s' tr
H1: composite_valid_transition_item IM s' item
IHcomposite_valid_transitions_from_to: constrained_state_prop
  Free s'
→ finite_constrained_trace_from_to
    Free s s' tr
H2: constrained_state_prop Free (destination item)
Hitem: input_constrained_transition Free 
  (l item) (
  s', input item)
  (destination item, output item)
finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Free) 
  ?m (destination item) [item]
  -
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': composite_state IM
tr: list (composite_transition_item IM)
item: composite_transition_item IM
H0: composite_valid_transitions_from_to IM s s' tr
H1: composite_valid_transition_item IM s' item
IHcomposite_valid_transitions_from_to: constrained_state_prop
  Free s'
→ finite_constrained_trace_from_to
    Free s s' tr
H2: constrained_state_prop Free (destination item)
Hitem: input_constrained_transition Free 
  (l item) (
  s', input item)
  (destination item, output item)
finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Free) s ?m tr apply IHcomposite_valid_transitions_from_to.
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': composite_state IM
tr: list (composite_transition_item IM)
item: composite_transition_item IM
H0: composite_valid_transitions_from_to IM s s' tr
H1: composite_valid_transition_item IM s' item
IHcomposite_valid_transitions_from_to: constrained_state_prop
  Free s'
→ finite_constrained_trace_from_to
    Free s s' tr
H2: constrained_state_prop Free (destination item)
Hitem: input_constrained_transition Free 
  (l item) (
  s', input item)
  (destination item, output item)
constrained_state_prop Free s'
    by eapply input_valid_transition_origin.
  -
message, index: Type
EqDecision0: EqDecision index
IM: index → VLSM message
H: ∀ i : index, HistoryVLSM (IM i)
Free:= free_composite_vlsm IM: VLSM message
s, s': composite_state IM
tr: list (composite_transition_item IM)
item: composite_transition_item IM
H0: composite_valid_transitions_from_to IM s s' tr
H1: composite_valid_transition_item IM s' item
IHcomposite_valid_transitions_from_to: constrained_state_prop
  Free s'
→ finite_constrained_trace_from_to
    Free s s' tr
H2: constrained_state_prop Free (destination item)
Hitem: input_constrained_transition Free 
  (l item) (
  s', input item)
  (destination item, output item)
finite_valid_trace_from_to
  (preloaded_with_all_messages_vlsm Free) s'
  (destination item) [item] by destruct item; apply finite_valid_trace_from_to_singleton.
Qed.

End sec_history_vlsm_composite.