From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From VLSM.Core Require Import VLSM VLSMProjections Equivocators.Equivocators.[Loading ML file coq-itauto.plugin ... done]
From VLSM.Core Require Import Equivocation EquivocationProjections Equivocators.MessageProperties.[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
[Loading ML file equations_plugin.cmxs (using legacy method) ... done]

Core: Equivocator State Append Determines a Projection

In this module, we show that we can "append" two equivocator traces by simulating the second at the end of the first.

The transformation on the states of the second trace is obtained by equivocator_state_appending each state to the last state of the first trace.

Section sec_equivocator_state_append_projection.

Context
  {message : Type}
  (X : VLSM message)
  .

Definition equivocator_state_append_label
  (base_s : equivocator_state X)
  (l : equivocator_label X)
  : equivocator_label X
  :=
  match l with
  | Spawn _ => l
  | ContinueWith i lx => ContinueWith (i + equivocator_state_n base_s) lx
  | ForkWith i lx => ForkWith (i + equivocator_state_n base_s) lx
  end.

Lemma equivocator_state_append_valid l s om base_s
  : equivocator_valid X l (s, om) ->
    equivocator_valid X
      (equivocator_state_append_label base_s l)
      (equivocator_state_append base_s s, om).message: Type
X: VLSM message
l: equivocator_label X
s: equivocator_state X
om: option message
base_s: equivocator_state X
equivocator_valid X l (s, om)
→ equivocator_valid X
    (equivocator_state_append_label base_s l)
    (equivocator_state_append base_s s, om)
Proof.message: Type
X: VLSM message
l: equivocator_label X
s: equivocator_state X
om: option message
base_s: equivocator_state X
equivocator_valid X l (s, om)
→ equivocator_valid X
    (equivocator_state_append_label base_s l)
    (equivocator_state_append base_s s, om)
  by destruct l; cbn; [done | ..]
  ; (destruct (equivocator_state_project s n) as [sn |] eqn: Hn; [| done])
  ; rewrite (equivocator_state_append_project_2 _ base_s s _ n eq_refl)
  ; rewrite Hn.
Qed.

Lemma equivocator_state_append_transition l s om s' om' base_s
  : equivocator_valid X l (s, om) ->
    equivocator_transition X l (s, om) = (s', om') ->
    equivocator_transition X (equivocator_state_append_label base_s l)
      (equivocator_state_append base_s s, om) = (equivocator_state_append base_s s', om').message: Type
X: VLSM message
l: equivocator_label X
s: equivocator_state X
om: option message
s': equivocator_state X
om': option message
base_s: equivocator_state X
equivocator_valid X l (s, om)
→ equivocator_transition X l (s, om) = (s', om')
  → equivocator_transition X
      (equivocator_state_append_label base_s l)
      (equivocator_state_append base_s s, om) =
    (equivocator_state_append base_s s', om')
Proof.message: Type
X: VLSM message
l: equivocator_label X
s: equivocator_state X
om: option message
s': equivocator_state X
om': option message
base_s: equivocator_state X
equivocator_valid X l (s, om)
→ equivocator_transition X l (s, om) = (s', om')
  → equivocator_transition X
      (equivocator_state_append_label base_s l)
      (equivocator_state_append base_s s, om) =
    (equivocator_state_append base_s s', om')
  destruct l; cbn; intros Hv Ht
  ; [by inversion_clear Ht; f_equal; apply equivocator_state_append_extend_commute | ..]
  ; (destruct (equivocator_state_project s n) as [sn |] eqn: Hn; [| done])
  ;  rewrite (equivocator_state_append_project_2 _ base_s s _ n eq_refl)
  ;  rewrite Hn
  ;  destruct (transition _ _ _) as (sn', _om') eqn: Hti
  ;  inversion_clear Ht; f_equal.message: Type
X: VLSM message
n: nat
l: label X
s: equivocator_state X
om: option message
s': equivocator_state X
om': option message
base_s: equivocator_state X
sn: state X
Hn: equivocator_state_project s n = Some sn
Hv: valid l (sn, om)
sn': state X
_om': option message
Hti: transition l (sn, om) = (sn', _om')
equivocator_state_update
  (equivocator_state_append base_s s)
  (n + equivocator_state_n base_s) sn' =
equivocator_state_append base_s
  (equivocator_state_update s n sn')
message: Type
X: VLSM message
n: nat
l: label X
s: equivocator_state X
om: option message
s': equivocator_state X
om': option message
base_s: equivocator_state X
sn: state X
Hn: equivocator_state_project s n = Some sn
Hv: valid l (sn, om)
sn': state X
_om': option message
Hti: transition l (sn, om) = (sn', _om')
equivocator_state_extend
  (equivocator_state_append base_s s) sn' =
equivocator_state_append base_s
  (equivocator_state_extend s sn')
  -message: Type
X: VLSM message
n: nat
l: label X
s: equivocator_state X
om: option message
s': equivocator_state X
om': option message
base_s: equivocator_state X
sn: state X
Hn: equivocator_state_project s n = Some sn
Hv: valid l (sn, om)
sn': state X
_om': option message
Hti: transition l (sn, om) = (sn', _om')
equivocator_state_update
  (equivocator_state_append base_s s)
  (n + equivocator_state_n base_s) sn' =
equivocator_state_append base_s
  (equivocator_state_update s n sn') by apply equivocator_state_append_update_commute.
  -message: Type
X: VLSM message
n: nat
l: label X
s: equivocator_state X
om: option message
s': equivocator_state X
om': option message
base_s: equivocator_state X
sn: state X
Hn: equivocator_state_project s n = Some sn
Hv: valid l (sn, om)
sn': state X
_om': option message
Hti: transition l (sn, om) = (sn', _om')
equivocator_state_extend
  (equivocator_state_append base_s s) sn' =
equivocator_state_append base_s
  (equivocator_state_extend s sn') by apply equivocator_state_append_extend_commute.
Qed.

Lemma equivocator_state_append_initial_state_in_futures
    (seed : message -> Prop)
    (base_s : equivocator_state X)
    (Hbase_s : valid_state_prop (preloaded_vlsm (equivocator_vlsm X) seed) base_s)
    s
    : initial_state_prop (equivocator_vlsm X) s ->
      in_futures (preloaded_vlsm (equivocator_vlsm X) seed) base_s
        (equivocator_state_append base_s s).message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
initial_state_prop s
→ in_futures
    (preloaded_vlsm (equivocator_vlsm X) seed) base_s
    (equivocator_state_append base_s s)
Proof.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
initial_state_prop s
→ in_futures
    (preloaded_vlsm (equivocator_vlsm X) seed) base_s
    (equivocator_state_append base_s s)
  exists
    [(Build_transition_item (equivocator_vlsm X)
      (Spawn (equivocator_state_zero s))
      None
      (equivocator_state_append base_s s)
      None)].message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed) base_s
  (equivocator_state_append base_s s)
  [{|
     l := Spawn (equivocator_state_zero s);
     input := None;
     destination := equivocator_state_append base_s s;
     output := None
   |}]
  apply (finite_valid_trace_from_to_singleton (preloaded_vlsm (equivocator_vlsm X) seed)).message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
input_valid_transition
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (Spawn (equivocator_state_zero s)) (base_s, None)
  (equivocator_state_append base_s s, None)
  repeat split.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) base_s
message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
option_valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) None
message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
initial_state_prop (equivocator_state_zero s)
message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
transition (Spawn (equivocator_state_zero s))
  (base_s, None) =
(equivocator_state_append base_s s, None)
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) base_s done.
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
option_valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) None by apply option_valid_message_None.
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
initial_state_prop (equivocator_state_zero s) by apply H.
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
transition (Spawn (equivocator_state_zero s))
  (base_s, None) =
(equivocator_state_append base_s s, None) cbn.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
(equivocator_state_extend base_s
   (equivocator_state_zero s), None) =
(equivocator_state_append base_s s, None) f_equal.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
equivocator_state_extend base_s
  (equivocator_state_zero s) =
equivocator_state_append base_s s symmetry.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
H: initial_state_prop s
equivocator_state_append base_s s =
equivocator_state_extend base_s
  (equivocator_state_zero s)
    by apply equivocator_state_append_singleton_is_extend, H.
Qed.

Lemma equivocator_state_append_transition_initial_state
    (seed : message -> Prop)
    (base_s : equivocator_state X)
    (Hbase_s : valid_state_prop (preloaded_vlsm (equivocator_vlsm X) seed) base_s)
    s
    : initial_state_prop (equivocator_vlsm X) s ->
      valid_state_prop (preloaded_vlsm (equivocator_vlsm X) seed)
        (equivocator_state_append base_s s).message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
initial_state_prop s
→ valid_state_prop
    (preloaded_vlsm (equivocator_vlsm X) seed)
    (equivocator_state_append base_s s)
Proof.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
initial_state_prop s
→ valid_state_prop
    (preloaded_vlsm (equivocator_vlsm X) seed)
    (equivocator_state_append base_s s)
  intros Hs.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
Hs: initial_state_prop s
valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s s) apply in_futures_valid_snd with base_s.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (equivocator_vlsm X)
Hs: initial_state_prop s
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s s)
  by apply equivocator_state_append_initial_state_in_futures.
Qed.

Lemma equivocator_state_append_preloaded_with_weak_projection
  (seed : message -> Prop)
  (base_s : equivocator_state X)
  (Hbase_s : valid_state_prop (preloaded_vlsm (equivocator_vlsm X) seed) base_s)
  : VLSM_weak_embedding (preloaded_vlsm (equivocator_vlsm X) seed)
      (preloaded_vlsm (equivocator_vlsm X) seed)
      (equivocator_state_append_label base_s) (equivocator_state_append base_s).message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Proof.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
  apply basic_VLSM_weak_embedding; intro; intros.message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hv: input_valid
  (preloaded_vlsm (equivocator_vlsm X) seed) l
  (s, om)
HsY: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s s)
HomY: option_valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
valid (equivocator_state_append_label base_s l)
  (equivocator_state_append base_s s, om)
message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
s': state (preloaded_vlsm (equivocator_vlsm X) seed)
om': option message
H: input_valid_transition
  (preloaded_vlsm (equivocator_vlsm X) seed) l
  (s, om) (s', om')
transition (equivocator_state_append_label base_s l)
  (equivocator_state_append base_s s, om) =
(equivocator_state_append base_s s', om')
message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
H: initial_state_prop s
valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s s)
message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
m: message
Hv: input_valid
  (preloaded_vlsm (equivocator_vlsm X) seed) l
  (s, Some m)
HsY: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s s)
HmX: initial_message_prop m
valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) m
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hv: input_valid
  (preloaded_vlsm (equivocator_vlsm X) seed) l
  (s, om)
HsY: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s s)
HomY: option_valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
valid (equivocator_state_append_label base_s l)
  (equivocator_state_append base_s s, om) by apply equivocator_state_append_valid, Hv.
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
s': state (preloaded_vlsm (equivocator_vlsm X) seed)
om': option message
H: input_valid_transition
  (preloaded_vlsm (equivocator_vlsm X) seed) l
  (s, om) (s', om')
transition (equivocator_state_append_label base_s l)
  (equivocator_state_append base_s s, om) =
(equivocator_state_append base_s s', om') by apply equivocator_state_append_transition; apply H.
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
H: initial_state_prop s
valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s s) by apply equivocator_state_append_transition_initial_state.
  -message: Type
X: VLSM message
seed: message → Prop
base_s: equivocator_state X
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
m: message
Hv: input_valid
  (preloaded_vlsm (equivocator_vlsm X) seed) l
  (s, Some m)
HsY: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s s)
HmX: initial_message_prop m
valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) m by apply initial_message_is_valid.
Qed.

Lemma equivocator_state_append_preloaded_weak_projection
  (base_s : equivocator_state X)
  (Hbase_s : constrained_state_prop (equivocator_vlsm X) base_s)
  : VLSM_weak_embedding (preloaded_with_all_messages_vlsm (equivocator_vlsm X))
      (preloaded_with_all_messages_vlsm (equivocator_vlsm X))
      (equivocator_state_append_label base_s) (equivocator_state_append base_s).message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Proof.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
  by constructor; apply equivocator_state_append_preloaded_with_weak_projection.
Qed.

Lemma equivocator_state_append_weak_projection
  (base_s : equivocator_state X)
  (Hbase_s : valid_state_prop (equivocator_vlsm X) base_s)
  : VLSM_weak_embedding (equivocator_vlsm X) (equivocator_vlsm X)
        (equivocator_state_append_label base_s) (equivocator_state_append base_s).message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
VLSM_weak_embedding (equivocator_vlsm X)
  (equivocator_vlsm X)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Proof.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
VLSM_weak_embedding (equivocator_vlsm X)
  (equivocator_vlsm X)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
  specialize (vlsm_is_preloaded_with_False (equivocator_vlsm X)) as Heq.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
Heq: VLSM_eq (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
VLSM_weak_embedding (equivocator_vlsm X)
  (equivocator_vlsm X)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
  constructor.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
Heq: VLSM_eq (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
∀ (sX : state (equivocator_vlsm X)) (trX : list
                                             transition_item),
  finite_valid_trace_from (equivocator_vlsm X) sX trX
  → finite_valid_trace_from (equivocator_vlsm X)
      (equivocator_state_append base_s sX)
      (pre_VLSM_embedding_finite_trace_project
         (equivocator_vlsm X) (equivocator_vlsm X)
         (equivocator_state_append_label base_s)
         (equivocator_state_append base_s) trX)
  intros sX trX HtrX.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
Heq: VLSM_eq (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
sX: state (equivocator_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace_from 
  (equivocator_vlsm X) sX trX
finite_valid_trace_from (equivocator_vlsm X)
  (equivocator_state_append base_s sX)
  (pre_VLSM_embedding_finite_trace_project
     (equivocator_vlsm X) (equivocator_vlsm X)
     (equivocator_state_append_label base_s)
     (equivocator_state_append base_s) trX)
  apply (VLSM_eq_finite_valid_trace_from Heq) in HtrX.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
Heq: VLSM_eq (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
sX: state (equivocator_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace_from
  {|
    vlsm_type := equivocator_vlsm X;
    vlsm_machine :=
      preloaded_vlsm (equivocator_vlsm X)
        (λ _ : message, False)
  |} sX trX
finite_valid_trace_from (equivocator_vlsm X)
  (equivocator_state_append base_s sX)
  (pre_VLSM_embedding_finite_trace_project
     (equivocator_vlsm X) (equivocator_vlsm X)
     (equivocator_state_append_label base_s)
     (equivocator_state_append base_s) trX)
  apply (VLSM_eq_finite_valid_trace_from Heq).message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
Heq: VLSM_eq (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
sX: state (equivocator_vlsm X)
trX: list transition_item
HtrX: finite_valid_trace_from
  {|
    vlsm_type := equivocator_vlsm X;
    vlsm_machine :=
      preloaded_vlsm (equivocator_vlsm X)
        (λ _ : message, False)
  |} sX trX
finite_valid_trace_from
  {|
    vlsm_type := equivocator_vlsm X;
    vlsm_machine :=
      preloaded_vlsm (equivocator_vlsm X)
        (λ _ : message, False)
  |} (equivocator_state_append base_s sX)
  (pre_VLSM_embedding_finite_trace_project
     (equivocator_vlsm X) (equivocator_vlsm X)
     (equivocator_state_append_label base_s)
     (equivocator_state_append base_s) trX)
  revert sX trX HtrX.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
Heq: VLSM_eq (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
∀ (sX : state (equivocator_vlsm X)) (trX : list
                                             transition_item),
  finite_valid_trace_from
    {|
      vlsm_type := equivocator_vlsm X;
      vlsm_machine :=
        preloaded_vlsm (equivocator_vlsm X)
          (λ _ : message, False)
    |} sX trX
  → finite_valid_trace_from
      {|
        vlsm_type := equivocator_vlsm X;
        vlsm_machine :=
          preloaded_vlsm (equivocator_vlsm X)
            (λ _ : message, False)
      |} (equivocator_state_append base_s sX)
      (pre_VLSM_embedding_finite_trace_project
         (equivocator_vlsm X) (equivocator_vlsm X)
         (equivocator_state_append_label base_s)
         (equivocator_state_append base_s) trX)
  apply equivocator_state_append_preloaded_with_weak_projection.message: Type
X: VLSM message
base_s: equivocator_state X
Hbase_s: valid_state_prop (equivocator_vlsm X) base_s
Heq: VLSM_eq (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False)) base_s
  by apply (VLSM_eq_valid_state Heq).
Qed.

Lemma equivocator_state_append_in_futures
  (seed : message -> Prop)
  base_s (Hbase_s : valid_state_prop (preloaded_vlsm (equivocator_vlsm X) seed) base_s)
  s (Hs : valid_state_prop (preloaded_vlsm (equivocator_vlsm X) seed) s)
  : in_futures (preloaded_vlsm (equivocator_vlsm X) seed) base_s (equivocator_state_append base_s s).message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hs: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s s)
Proof.message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hs: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s s)
  apply valid_state_has_trace in Hs as [is [tr [Htr His]]].message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s, is: state (preloaded_vlsm (equivocator_vlsm X) seed)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed) is
  s tr
His: initial_state_prop is
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s s)
  specialize (equivocator_state_append_preloaded_with_weak_projection seed _ Hbase_s) as Hproj.message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s, is: state (preloaded_vlsm (equivocator_vlsm X) seed)
tr: list transition_item
Htr: finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed) is
  s tr
His: initial_state_prop is
Hproj: VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s s)
  apply (VLSM_weak_embedding_finite_valid_trace_from_to Hproj) in Htr.message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s, is: state (preloaded_vlsm (equivocator_vlsm X) seed)
tr: list transition_item
Hproj: VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Htr: finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s is)
  (equivocator_state_append base_s s)
  (VLSM_weak_embedding_finite_trace_project
     Hproj tr)
His: initial_state_prop is
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s s)
  apply in_futures_trans with (equivocator_state_append base_s is).message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s, is: state (preloaded_vlsm (equivocator_vlsm X) seed)
tr: list transition_item
Hproj: VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Htr: finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s is)
  (equivocator_state_append base_s s)
  (VLSM_weak_embedding_finite_trace_project
     Hproj tr)
His: initial_state_prop is
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s is)
message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s, is: state (preloaded_vlsm (equivocator_vlsm X) seed)
tr: list transition_item
Hproj: VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Htr: finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s is)
  (equivocator_state_append base_s s)
  (VLSM_weak_embedding_finite_trace_project
     Hproj tr)
His: initial_state_prop is
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s is)
  (equivocator_state_append base_s s)
  -message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s, is: state (preloaded_vlsm (equivocator_vlsm X) seed)
tr: list transition_item
Hproj: VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Htr: finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s is)
  (equivocator_state_append base_s s)
  (VLSM_weak_embedding_finite_trace_project
     Hproj tr)
His: initial_state_prop is
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s (equivocator_state_append base_s is) by apply equivocator_state_append_initial_state_in_futures.
  -message: Type
X: VLSM message
seed: message → Prop
base_s: state
  (preloaded_vlsm (equivocator_vlsm X) seed)
Hbase_s: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed)
  base_s
s, is: state (preloaded_vlsm (equivocator_vlsm X) seed)
tr: list transition_item
Hproj: VLSM_weak_embedding
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
Htr: finite_valid_trace_from_to
  (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s is)
  (equivocator_state_append base_s s)
  (VLSM_weak_embedding_finite_trace_project
     Hproj tr)
His: initial_state_prop is
in_futures (preloaded_vlsm (equivocator_vlsm X) seed)
  (equivocator_state_append base_s is)
  (equivocator_state_append base_s s) by eexists.
Qed.

Lemma equivocator_state_append_sent_left
  `{HasBeenSentCapability message X}
  base_s (Hbase_s : constrained_state_prop (equivocator_vlsm X) base_s)
  s (Hs : constrained_state_prop (equivocator_vlsm X) s)
  : forall m, equivocator_has_been_sent X base_s m ->
    equivocator_has_been_sent X (equivocator_state_append base_s s) m.message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: constrained_state_prop (equivocator_vlsm X) s
∀ m : message,
  equivocator_has_been_sent X base_s m
  → equivocator_has_been_sent X
      (equivocator_state_append base_s s) m
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: constrained_state_prop (equivocator_vlsm X) s
∀ m : message,
  equivocator_has_been_sent X base_s m
  → equivocator_has_been_sent X
      (equivocator_state_append base_s s) m
  apply (equivocator_state_append_in_futures _ _ Hbase_s) in Hs.message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: in_futures
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, True)) base_s
  (equivocator_state_append base_s s)
∀ m : message,
  equivocator_has_been_sent X base_s m
  → equivocator_has_been_sent X
      (equivocator_state_append base_s s) m
  apply (in_futures_preserving_oracle_from_stepwise _ (equivocator_vlsm X) (field_selector output)
    (equivocator_has_been_sent X)); [| done].message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: in_futures
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, True)) base_s
  (equivocator_state_append base_s s)
oracle_stepwise_props (field_selector output)
  (equivocator_has_been_sent X)
  by apply equivocator_has_been_sent_stepwise_props.
Qed.

Lemma equivocator_state_append_sent_right
  `{HasBeenSentCapability message X}
  base_s (Hbase_s : constrained_state_prop (equivocator_vlsm X) base_s)
  s (Hs : constrained_state_prop (equivocator_vlsm X) s)
  : forall m, equivocator_has_been_sent X s m ->
    equivocator_has_been_sent X (equivocator_state_append base_s s) m.message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: constrained_state_prop (equivocator_vlsm X) s
∀ m : message,
  equivocator_has_been_sent X s m
  → equivocator_has_been_sent X
      (equivocator_state_append base_s s) m
Proof.message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: constrained_state_prop (equivocator_vlsm X) s
∀ m : message,
  equivocator_has_been_sent X s m
  → equivocator_has_been_sent X
      (equivocator_state_append base_s s) m
  specialize (equivocator_state_append_preloaded_weak_projection _ Hbase_s) as Hproj.message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: constrained_state_prop (equivocator_vlsm X) s
Hproj: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
∀ m : message,
  equivocator_has_been_sent X s m
  → equivocator_has_been_sent X
      (equivocator_state_append base_s s) m
  intros m Hm.message: Type
X: VLSM message
H: HasBeenSentCapability X
base_s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hbase_s: constrained_state_prop 
  (equivocator_vlsm X) base_s
s: state
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
Hs: constrained_state_prop (equivocator_vlsm X) s
Hproj: VLSM_weak_embedding
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (preloaded_with_all_messages_vlsm
     (equivocator_vlsm X))
  (equivocator_state_append_label base_s)
  (equivocator_state_append base_s)
m: message
Hm: equivocator_has_been_sent X s m
equivocator_has_been_sent X
  (equivocator_state_append base_s s) m
  by specialize (VLSM_weak_embedding_has_been_sent Hproj _ Hs _ Hm) as HmY.
Qed.

End sec_equivocator_state_append_projection.