From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude finite.
From VLSM.Lib Require Import EquationsExtras.[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
[Loading ML file equations_plugin.cmxs (using legacy method) ... done]
From VLSM.Lib Require Import Preamble StdppExtras Measurable.
From VLSM.Core Require Import VLSM PreloadedVLSM MessageDependencies.

ELMO: Basic Definitions and Results for UMO, MO and ELMO

This module contains basic definitions and lemmas needed for the UMO, MO and ELMO protocols. In contrast to the paper, which uses natural numbers, we abstract over the implementation of an Address by making it an arbitrary type with decidable equality.

Section sec_base_ELMO.

Context
  {Address : Type}
  `{EqDecision Address}.

Labels, States, Observations and Messages

Messages can be labeled as either sent or received.

Inductive Label : Type :=
| Receive
| Send.

Inductive State : Type := MkState
{
  obs : list Observation;
  adr  : Address;
}
with Observation : Type := MkObservation
{
  label   : Label;
  message : Message;
}
(** A [Message] is a wrapper for [State]. *)
with Message : Type := MkMessage
{
  state : State;
}.

States, Observations and Messages are printed like ordinary inductive types, using their constructor names, instead of as records with the {| ... |} notation.

Add Printing Constructor State Observation Message.

Two states are equal when they have equal observations and equal addresses.

Lemma eq_State :
  forall s1 s2 : State,
    obs s1 = obs s2 -> adr s1 = adr s2 -> s1 = s2.Address: Type
EqDecision0: EqDecision Address
∀ s1 s2 : State,
  obs s1 = obs s2 → adr s1 = adr s2 → s1 = s2
Proof.Address: Type
EqDecision0: EqDecision Address
∀ s1 s2 : State,
  obs s1 = obs s2 → adr s1 = adr s2 → s1 = s2
  by intros [] []; cbn; congruence.
Qed.

Lemma eq_Message :
  forall m1 m2 : Message,
    obs (state m1) = obs (state m2) -> adr (state m1) = adr (state m2) -> m1 = m2.Address: Type
EqDecision0: EqDecision Address
∀ m1 m2 : Message,
  obs (state m1) = obs (state m2)
  → adr (state m1) = adr (state m2) → m1 = m2
Proof.Address: Type
EqDecision0: EqDecision Address
∀ m1 m2 : Message,
  obs (state m1) = obs (state m2)
  → adr (state m1) = adr (state m2) → m1 = m2
  by intros [[]] [[]]; cbn; congruence.
Qed.

Lemma eq_Observation :
  forall ob1 ob2 : Observation,
    label ob1 = label ob2 -> message ob1 = message ob2 -> ob1 = ob2.Address: Type
EqDecision0: EqDecision Address
∀ ob1 ob2 : Observation,
  label ob1 = label ob2
  → message ob1 = message ob2 → ob1 = ob2
Proof.Address: Type
EqDecision0: EqDecision Address
∀ ob1 ob2 : Observation,
  label ob1 = label ob2
  → message ob1 = message ob2 → ob1 = ob2
  by intros [] []; cbn; congruence.
Qed.

Labels, States, Observations and Messages have decidable equality.

#[export] Instance EqDecision_Label : EqDecision Label.Address: Type
EqDecision0: EqDecision Address
EqDecision Label
Proof.Address: Type
EqDecision0: EqDecision Address
EqDecision Label by intros x y; unfold Decision; decide equality. Defined.

#[local] Lemma State_eq_dec : forall x y : State, {x = y} + {x <> y}
with Observation_eq_dec : forall x y : Observation, {x = y} + {x <> y}
with Message_eq_dec : forall x y : Message, {x = y} + {x <> y}.Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : State, {x = y} + {x ≠ y}
Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : Observation, {x = y} + {x ≠ y}
Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : Message, {x = y} + {x ≠ y}
Proof.Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : State, {x = y} + {x ≠ y}
Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : Observation, {x = y} + {x ≠ y}
Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : Message, {x = y} + {x ≠ y}
  -Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : State, {x = y} + {x ≠ y} intros x y; decide equality.Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
x, y: State
obs0: list Observation
adr0: Address
obs1: list Observation
adr1: Address
a: obs0 = obs1
{adr0 = adr1} + {adr0 ≠ adr1}
Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
x, y: State
obs0: list Observation
adr0: Address
obs1: list Observation
adr1: Address
{obs0 = obs1} + {obs0 ≠ obs1}
    +Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
x, y: State
obs0: list Observation
adr0: Address
obs1: list Observation
adr1: Address
a: obs0 = obs1
{adr0 = adr1} + {adr0 ≠ adr1} by apply EqDecision0.
    +Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
x, y: State
obs0: list Observation
adr0: Address
obs1: list Observation
adr1: Address
{obs0 = obs1} + {obs0 ≠ obs1} by decide equality.
  -Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : Observation, {x = y} + {x ≠ y} by do 2 decide equality.
  -Address: Type
EqDecision0: EqDecision Address
State_eq_dec: ∀ x y : State, {x = y} + {x ≠ y}
Observation_eq_dec: ∀ x y : Observation,
  {x = y} + {x ≠ y}
Message_eq_dec: ∀ x y : Message, {x = y} + {x ≠ y}
∀ x y : Message, {x = y} + {x ≠ y} by intros x y; decide equality.
Defined.

#[export] Instance EqDecision_State : EqDecision State := State_eq_dec.
#[export] Instance EqDecision_Observation : EqDecision Observation := Observation_eq_dec.
#[export] Instance EqDecision_Message : EqDecision Message := Message_eq_dec.

A notion of size for States, Observations and Messages.

Fixpoint sizeState (s : State) : nat :=
  1 + fold_right (fun ob sizeObs => sizeObservation ob + sizeObs) 0 (obs s)

with sizeObservation (ob : Observation) : nat :=
  1 + sizeMessage (message ob)

with sizeMessage (msg : Message) : nat :=
  1 + sizeState (state msg).

Lemma sizeObservation_unfold (ob : Observation) :
  sizeObservation ob = 2 + sizeState (state (message ob)).Address: Type
EqDecision0: EqDecision Address
ob: Observation
sizeObservation ob =
2 + sizeState (state (message ob))
Proof.Address: Type
EqDecision0: EqDecision Address
ob: Observation
sizeObservation ob =
2 + sizeState (state (message ob)) by destruct ob as [? []]. Qed.

Extending States with new Observations

We want to abstract over from the "direction" of the list of Observations, so that we can cons new observations at the beginning, whereas in the paper they are appended to the end. We will use the function addObservation to extend a state with a new observations and addObservations to extend a state with a list of new observations.

Definition addObservation' (ob : Observation) (obs : list Observation) : list Observation :=
  ob :: obs.

Lemma addObservation'_ind (P : list Observation -> Prop)
  (Hempty : P [])
  (Hadd : forall ob obs, P obs -> P (addObservation' ob obs)) :
  forall obs, P obs.Address: Type
EqDecision0: EqDecision Address
P: list Observation → Prop
Hempty: P []
Hadd: ∀ (ob : Observation) (obs : list Observation),
  P obs → P (addObservation' ob obs)
∀ obs : list Observation, P obs
Proof.Address: Type
EqDecision0: EqDecision Address
P: list Observation → Prop
Hempty: P []
Hadd: ∀ (ob : Observation) (obs : list Observation),
  P obs → P (addObservation' ob obs)
∀ obs : list Observation, P obs
  exact (list_ind P Hempty Hadd).
Qed.

Lemma addObservation'_rec (P : list Observation -> Set)
  (Hempty : P [])
  (Hadd : forall ob obs, P obs -> P (addObservation' ob obs)) :
  forall obs, P obs.Address: Type
EqDecision0: EqDecision Address
P: list Observation → Set
Hempty: P []
Hadd: ∀ (ob : Observation) (obs : list Observation),
  P obs → P (addObservation' ob obs)
∀ obs : list Observation, P obs
Proof.Address: Type
EqDecision0: EqDecision Address
P: list Observation → Set
Hempty: P []
Hadd: ∀ (ob : Observation) (obs : list Observation),
  P obs → P (addObservation' ob obs)
∀ obs : list Observation, P obs
  exact (list_rec P Hempty Hadd).
Defined.

Lemma addObservation'_rect (P : list Observation -> Type)
  (Hempty : P [])
  (Hadd : forall ob obs, P obs -> P (addObservation' ob obs)) :
  forall obs, P obs.Address: Type
EqDecision0: EqDecision Address
P: list Observation → Type
Hempty: P []
Hadd: ∀ (ob : Observation) (obs : list Observation),
  P obs → P (addObservation' ob obs)
∀ obs : list Observation, P obs
Proof.Address: Type
EqDecision0: EqDecision Address
P: list Observation → Type
Hempty: P []
Hadd: ∀ (ob : Observation) (obs : list Observation),
  P obs → P (addObservation' ob obs)
∀ obs : list Observation, P obs
  exact (list_rect P Hempty Hadd).
Defined.

Definition addObservation (ob : Observation) (s : State) : State :=
  MkState (addObservation' ob (obs s)) (adr s).

Notation "s <+> ob" := (addObservation ob s) (left associativity, at level 50).

The induction principle addObservation_ind considers a State as built up using addObservation from an initial state.

Lemma addObservation_ind (P : State -> Prop)
  (Hempty : forall a, P (MkState [] a))
  (Hadd : forall ob s, P s -> P (addObservation ob s)) :
  forall obs, P obs.Address: Type
EqDecision0: EqDecision Address
P: State → Prop
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
∀ obs : State, P obs
Proof.Address: Type
EqDecision0: EqDecision Address
P: State → Prop
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
∀ obs : State, P obs
  intros [obs a].Address: Type
EqDecision0: EqDecision Address
P: State → Prop
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
obs: list Observation
a: Address
P (MkState obs a)
  induction obs using addObservation'_ind; [done |].Address: Type
EqDecision0: EqDecision Address
P: State → Prop
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
a: Address
ob: Observation
obs0: list Observation
IHobs: P (MkState obs0 a)
P (MkState (addObservation' ob obs0) a)
  by apply (Hadd ob) in IHobs.
Qed.

Lemma addObservation_rec (P : State -> Set)
  (Hempty : forall a, P (MkState [] a))
  (Hadd : forall ob s, P s -> P (s <+> ob)) :
  forall obs, P obs.Address: Type
EqDecision0: EqDecision Address
P: State → Set
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
∀ obs : State, P obs
Proof.Address: Type
EqDecision0: EqDecision Address
P: State → Set
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
∀ obs : State, P obs
  intros [obs a].Address: Type
EqDecision0: EqDecision Address
P: State → Set
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
obs: list Observation
a: Address
P (MkState obs a)
  induction obs using addObservation'_rec; [done |].Address: Type
EqDecision0: EqDecision Address
P: State → Set
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
a: Address
ob: Observation
obs0: list Observation
IHobs: P (MkState obs0 a)
P (MkState (addObservation' ob obs0) a)
  by apply (Hadd ob) in IHobs.
Defined.

Lemma addObservation_rect (P : State -> Type)
  (Hempty : forall a, P (MkState [] a))
  (Hadd : forall ob s, P s -> P (addObservation ob s)) :
  forall obs, P obs.Address: Type
EqDecision0: EqDecision Address
P: State → Type
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
∀ obs : State, P obs
Proof.Address: Type
EqDecision0: EqDecision Address
P: State → Type
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
∀ obs : State, P obs
  intros [obs a].Address: Type
EqDecision0: EqDecision Address
P: State → Type
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
obs: list Observation
a: Address
P (MkState obs a)
  induction obs using addObservation'_rect; [done |].Address: Type
EqDecision0: EqDecision Address
P: State → Type
Hempty: ∀ a : Address, P (MkState [] a)
Hadd: ∀ (ob : Observation) (s : State),
  P s → P (s <+> ob)
a: Address
ob: Observation
obs0: list Observation
IHobs: P (MkState obs0 a)
P (MkState (addObservation' ob obs0) a)
  by apply (Hadd ob) in IHobs.
Defined.

This induction principle is like addObservation_ind, but also provides an induction hypothesis for the State contained in the message of the added observation.

Definition addObservation_both_ind
  (P : State -> Prop)
  (Hinit : forall a, P (MkState [] a))
  (Hadd : forall [s l ms], P s -> P ms -> P (s <+> MkObservation l (MkMessage ms))) :
  forall s, P s :=
  fix rec s :=
    let '(MkState ol a) := s in
    let Hcons := fun '(MkObservation _ (MkMessage ms)) _ IHol' => Hadd IHol' (rec ms)
    in list_ind _ (Hinit a) Hcons ol.

A property on sizeState of addObservation. Useful because a Fixpoint can't be unfolded unless the argument is in the form of a constructor application.

Lemma addObservation_size s ob :
  sizeState (s <+> ob) = sizeState s + sizeObservation ob.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
sizeState (s <+> ob) =
sizeState s + sizeObservation ob
Proof.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
sizeState (s <+> ob) =
sizeState s + sizeObservation ob by destruct s; cbn; lia. Qed.

Definition addObservations (obs' : list Observation) (s : State) : State :=
  MkState (obs' ++ (obs s)) (adr s).

Notation "s <++> obs" := (addObservations obs s) (left associativity, at level 50).

Definition addObservationToMessage (ob : Observation) (m : Message) : Message :=
  MkMessage (state m <+> ob).

Notation "m <*> ob" := (addObservationToMessage ob m) (left associativity, at level 50).

Definition addObservationsToMessage (obs' : list Observation) (m : Message) : Message :=
  MkMessage (state m <++> obs').

Notation "m <**> obs" := (addObservationsToMessage obs m) (left associativity, at level 50).

<+> is injective in both arguments.

Lemma addObservation_inj :
  forall (ob1 ob2 : Observation) (s1 s2 : State),
    s1 <+> ob1 = s2 <+> ob2 -> ob1 = ob2 /\ s1 = s2.Address: Type
EqDecision0: EqDecision Address
∀ (ob1 ob2 : Observation) (s1 s2 : State),
  s1 <+> ob1 = s2 <+> ob2 → ob1 = ob2 ∧ s1 = s2
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (ob1 ob2 : Observation) (s1 s2 : State),
  s1 <+> ob1 = s2 <+> ob2 → ob1 = ob2 ∧ s1 = s2
  intros ob1 ob2 s1 s2 [= ->].Address: Type
EqDecision0: EqDecision Address
ob2: Observation
s1, s2: State
H0: obs s1 = obs s2
H1: adr s1 = adr s2
ob2 = ob2 ∧ s1 = s2
  by split; [| apply eq_State].
Qed.

Adding an observation to a state results in a different state.

Lemma addObservation_acyclic :
  forall (ob : Observation) (s : State),
    s <+> ob <> s.Address: Type
EqDecision0: EqDecision Address
∀ (ob : Observation) (s : State), s <+> ob ≠ s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (ob : Observation) (s : State), s <+> ob ≠ s
  intros ob [obs adr] [= Heq].Address: Type
EqDecision0: EqDecision Address
ob: Observation
obs: list Observation
adr: Address
Heq: addObservation' ob obs = obs
False
  unfold addObservation' in Heq.Address: Type
EqDecision0: EqDecision Address
ob: Observation
obs: list Observation
adr: Address
Heq: ob :: obs = obs
False
  by apply (app_inv_tail _ [ob] []) in Heq.
Qed.

Adding no observations does not change the state.

Lemma addObservations_nil :
  forall s : State,
    s <++> [] = s.Address: Type
EqDecision0: EqDecision Address
∀ s : State, s <++> [] = s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ s : State, s <++> [] = s
  by intros [].
Qed.

Adding a single observation is compatible with adding many observations at once, in the obvious way.

Lemma addObservations_app :
  forall (s : State) (ob : Observation) (obs' : list Observation),
    s <+> ob <++> obs' = s <++> (obs' ++ [ob]).Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (obs' : list
                                           Observation),
  s <+> ob <++> obs' = s <++> (obs' ++ [ob])
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (obs' : list
                                           Observation),
  s <+> ob <++> obs' = s <++> (obs' ++ [ob])
  intros s ob obs'.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
obs': list Observation
s <+> ob <++> obs' = s <++> (obs' ++ [ob])
  by apply eq_State; cbn; [rewrite <- app_assoc |].
Qed.

Lemma addObservation_cons :
  forall (s : State) (ob : Observation) (obs' : list Observation),
    s <++> obs' <+> ob = s <++> (ob :: obs').Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (obs' : list
                                           Observation),
  s <++> obs' <+> ob = s <++> (ob :: obs')
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (obs' : list
                                           Observation),
  s <++> obs' <+> ob = s <++> (ob :: obs')
  intros s ob obs'.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
obs': list Observation
s <++> obs' <+> ob = s <++> (ob :: obs')
  by apply eq_State; cbn.
Qed.

An observation in s <+> ob is either the added observation ob or an observation in the original state.

Lemma elem_of_addObservation :
  forall (s : State) (ob ob' : Observation),
    ob' ∈ obs (s <+> ob) <-> ob' = ob \/ ob' ∈ obs s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob ob' : Observation),
  ob' ∈ obs (s <+> ob) ↔ ob' = ob ∨ ob' ∈ obs s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob ob' : Observation),
  ob' ∈ obs (s <+> ob) ↔ ob' = ob ∨ ob' ∈ obs s
  intros [s_obs a] ob ob'.Address: Type
EqDecision0: EqDecision Address
s_obs: list Observation
a: Address
ob, ob': Observation
ob' ∈ obs (MkState s_obs a <+> ob)
↔ ob' = ob ∨ ob' ∈ obs (MkState s_obs a)
  cbn; unfold addObservation'.Address: Type
EqDecision0: EqDecision Address
s_obs: list Observation
a: Address
ob, ob': Observation
ob' ∈ ob :: s_obs ↔ ob' = ob ∨ ob' ∈ s_obs
  by apply elem_of_cons.
Qed.

The immediate substate relation. May be used to prove that a State does not contain itself.

Inductive immediate_substate : State -> State -> Prop :=
| substate_prev : forall s ob, immediate_substate s (s <+> ob)
| substate_new : forall s ob, immediate_substate (state (message ob)) (s <+> ob).

Lemma immediate_substate_wf : well_founded immediate_substate.Address: Type
EqDecision0: EqDecision Address
wf immediate_substate
Proof.Address: Type
EqDecision0: EqDecision Address
wf immediate_substate
  intro s; induction s using addObservation_both_ind; constructor.Address: Type
EqDecision0: EqDecision Address
a: Address
∀ y : State,
  immediate_substate y (MkState [] a)
  → Acc immediate_substate y
Address: Type
EqDecision0: EqDecision Address
s1: State
l: Label
s2: State
IHs1: Acc immediate_substate s1
IHs2: Acc immediate_substate s2
∀ y : State,
  immediate_substate y
    (s1 <+> MkObservation l (MkMessage s2))
  → Acc immediate_substate y
  -Address: Type
EqDecision0: EqDecision Address
a: Address
∀ y : State,
  immediate_substate y (MkState [] a)
  → Acc immediate_substate y by inversion 1.
  -Address: Type
EqDecision0: EqDecision Address
s1: State
l: Label
s2: State
IHs1: Acc immediate_substate s1
IHs2: Acc immediate_substate s2
∀ y : State,
  immediate_substate y
    (s1 <+> MkObservation l (MkMessage s2))
  → Acc immediate_substate y by inversion 1; [rewrite (eq_State y s1) | subst y].
Qed.

Messages sent and received by a State

Definition isSend (ob : Observation) : Prop :=
  match label ob with
  | Send => True
  | Receive => False
  end.

Definition isReceive (ob : Observation) : Prop :=
  match label ob with
  | Send => False
  | Receive => True
  end.

#[export] Instance isSend_dec (ob : Observation) : Decision (isSend ob).Address: Type
EqDecision0: EqDecision Address
ob: Observation
Decision (isSend ob)
Proof.Address: Type
EqDecision0: EqDecision Address
ob: Observation
Decision (isSend ob)
  by destruct ob as [[] m]; cbn; typeclasses eauto.
Defined.

#[export] Instance isReceive_dec (ob : Observation) : Decision (isReceive ob).Address: Type
EqDecision0: EqDecision Address
ob: Observation
Decision (isReceive ob)
Proof.Address: Type
EqDecision0: EqDecision Address
ob: Observation
Decision (isReceive ob)
  by destruct ob as [[] m]; cbn; typeclasses eauto.
Defined.

Definition messages' (obs : list Observation) : list Message :=
  map message obs.

Definition messages (st : State) : list Message :=
  messages' (obs st).

Definition sentMessages' (obs : list Observation) : list Message :=
  map message (filter isSend obs).

Definition sentMessages (st : State) : list Message :=
  sentMessages' (obs st).

Definition receivedMessages' (obs : list Observation) : list Message :=
  map message (filter isReceive obs).

Definition receivedMessages (st : State) : list Message :=
  receivedMessages' (obs st).

Definition receivedAddresses (st : State) : list Address :=
  map (fun m => adr (state m)) (receivedMessages st).

Lemma elem_of_map_filter_addObservation
  [B] (f : Observation -> B)
  (P : Observation -> Prop) {P_dec : forall a, Decision (P a)} :
  forall s ob v,
    v ∈ map f (filter P (obs (s <+> ob)))
      <->
    v = f ob /\ P ob \/ v ∈ map f (filter P (obs s)).Address: Type
EqDecision0: EqDecision Address
B: Type
f: Observation → B
P: Observation → Prop
P_dec: ∀ a : Observation, Decision (P a)
∀ (s : State) (ob : Observation) (v : B),
  v ∈ map f (filter P (obs (s <+> ob)))
  ↔ v = f ob ∧ P ob ∨ v ∈ map f (filter P (obs s))
Proof.Address: Type
EqDecision0: EqDecision Address
B: Type
f: Observation → B
P: Observation → Prop
P_dec: ∀ a : Observation, Decision (P a)
∀ (s : State) (ob : Observation) (v : B),
  v ∈ map f (filter P (obs (s <+> ob)))
  ↔ v = f ob ∧ P ob ∨ v ∈ map f (filter P (obs s))
  intros s ob v.Address: Type
EqDecision0: EqDecision Address
B: Type
f: Observation → B
P: Observation → Prop
P_dec: ∀ a : Observation, Decision (P a)
s: State
ob: Observation
v: B
v ∈ map f (filter P (obs (s <+> ob)))
↔ v = f ob ∧ P ob ∨ v ∈ map f (filter P (obs s))
  rewrite !elem_of_list_fmap.Address: Type
EqDecision0: EqDecision Address
B: Type
f: Observation → B
P: Observation → Prop
P_dec: ∀ a : Observation, Decision (P a)
s: State
ob: Observation
v: B
(∃ y : Observation,
   v = f y ∧ y ∈ filter P (obs (s <+> ob)))
↔ v = f ob ∧ P ob
  ∨ (∃ y : Observation, v = f y ∧ y ∈ filter P (obs s))
  setoid_rewrite elem_of_list_filter.Address: Type
EqDecision0: EqDecision Address
B: Type
f: Observation → B
P: Observation → Prop
P_dec: ∀ a : Observation, Decision (P a)
s: State
ob: Observation
v: B
(∃ y : Observation, v = f y ∧ P y ∧ y ∈ obs (s <+> ob))
↔ v = f ob ∧ P ob
  ∨ (∃ y : Observation, v = f y ∧ P y ∧ y ∈ obs s)
  cbn; unfold addObservation'.Address: Type
EqDecision0: EqDecision Address
B: Type
f: Observation → B
P: Observation → Prop
P_dec: ∀ a : Observation, Decision (P a)
s: State
ob: Observation
v: B
(∃ y : Observation, v = f y ∧ P y ∧ y ∈ ob :: obs s)
↔ v = f ob ∧ P ob
  ∨ (∃ y : Observation, v = f y ∧ P y ∧ y ∈ obs s)
  setoid_rewrite elem_of_cons.Address: Type
EqDecision0: EqDecision Address
B: Type
f: Observation → B
P: Observation → Prop
P_dec: ∀ a : Observation, Decision (P a)
s: State
ob: Observation
v: B
(∃ y : Observation,
   v = f y ∧ P y ∧ (y = ob ∨ y ∈ obs s))
↔ v = f ob ∧ P ob
  ∨ (∃ y : Observation, v = f y ∧ P y ∧ y ∈ obs s)
  by split; intros H; decompose [and or ex] H; subst; eauto.
Qed.

When a message belongs to the sentMessages of some state, then the state contains a corresponding observation which was sent. The converse also holds.

Lemma elem_of_sentMessages :
  forall (s : State) (m : Message),
    m ∈ sentMessages s <-> MkObservation Send m ∈ obs s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (m : Message),
  m ∈ sentMessages s ↔ MkObservation Send m ∈ obs s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (m : Message),
  m ∈ sentMessages s ↔ MkObservation Send m ∈ obs s
  intros; unfold sentMessages, sentMessages'.Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
m ∈ map message (filter isSend (obs s))
↔ MkObservation Send m ∈ obs s
  rewrite elem_of_list_fmap; setoid_rewrite elem_of_list_filter.Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
(∃ y : Observation,
   m = message y ∧ isSend y ∧ y ∈ obs s)
↔ MkObservation Send m ∈ obs s
  split; [| by firstorder].Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
(∃ y : Observation,
   m = message y ∧ isSend y ∧ y ∈ obs s)
→ MkObservation Send m ∈ obs s
  by intros ([[] ?] & -> & []); cbn in *.
Qed.

A message in sentMessages (s <+> ob) is either in sentMessages s or is the message in the new observation ob, and can only be the message from ob if that is a Send observation.

Lemma elem_of_sentMessages_addObservation :
  forall (s : State) (ob : Observation) (m : Message),
    m ∈ sentMessages (s <+> ob)
      <->
    m = message ob /\ isSend ob \/ m ∈ sentMessages s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (m : Message),
  m ∈ sentMessages (s <+> ob)
  ↔ m = message ob ∧ isSend ob ∨ m ∈ sentMessages s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (m : Message),
  m ∈ sentMessages (s <+> ob)
  ↔ m = message ob ∧ isSend ob ∨ m ∈ sentMessages s
  by apply elem_of_map_filter_addObservation.
Qed.

Lemma sentMessages_addObservation :
  forall (s : State) (ob : Observation),
    sentMessages (s <+> ob)
      =
    if decide (isSend ob) then message ob :: sentMessages s else sentMessages s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  sentMessages (s <+> ob) =
  (if decide (isSend ob)
   then message ob :: sentMessages s
   else sentMessages s)
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  sentMessages (s <+> ob) =
  (if decide (isSend ob)
   then message ob :: sentMessages s
   else sentMessages s)
  intros s ob.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
sentMessages (s <+> ob) =
(if decide (isSend ob)
 then message ob :: sentMessages s
 else sentMessages s)
  unfold sentMessages, sentMessages'; cbn.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
map message
  (if decide (isSend ob)
   then ob :: filter isSend (obs s)
   else filter isSend (obs s)) =
(if decide (isSend ob)
 then
  message ob :: map message (filter isSend (obs s))
 else map message (filter isSend (obs s)))
  by destruct (decide (isSend ob)).
Qed.

When a message belongs to the receivedMessages of some state, then the state contains a corresponding observation which was received. The converse also holds.

Lemma elem_of_receivedMessages :
  forall (s : State) (m : Message),
    m ∈ receivedMessages s <-> MkObservation Receive m ∈ obs s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (m : Message),
  m ∈ receivedMessages s
  ↔ MkObservation Receive m ∈ obs s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (m : Message),
  m ∈ receivedMessages s
  ↔ MkObservation Receive m ∈ obs s
  intros; unfold receivedMessages, receivedMessages'.Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
m ∈ map message (filter isReceive (obs s))
↔ MkObservation Receive m ∈ obs s
  rewrite elem_of_list_fmap; setoid_rewrite elem_of_list_filter.Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
(∃ y : Observation,
   m = message y ∧ isReceive y ∧ y ∈ obs s)
↔ MkObservation Receive m ∈ obs s
  split; [| by firstorder].Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
(∃ y : Observation,
   m = message y ∧ isReceive y ∧ y ∈ obs s)
→ MkObservation Receive m ∈ obs s
  by intros ([[] ?] & -> & []); cbn in *.
Qed.

A message in receivedMessages (s <+> ob) is either in receivedMessages s or is the message in the new observation ob, and can only be the message from ob if that is a Receive observation.

Lemma elem_of_receivedMessages_addObservation :
  forall (s : State) (ob : Observation) (m : Message),
    m ∈ receivedMessages (s <+> ob)
      <->
    m = message ob /\ isReceive ob \/ m ∈ receivedMessages s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (m : Message),
  m ∈ receivedMessages (s <+> ob)
  ↔ m = message ob ∧ isReceive ob
    ∨ m ∈ receivedMessages s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (m : Message),
  m ∈ receivedMessages (s <+> ob)
  ↔ m = message ob ∧ isReceive ob
    ∨ m ∈ receivedMessages s
  by apply elem_of_map_filter_addObservation.
Qed.

Lemma receivedMessages_addObservation :
  forall (s : State) (ob : Observation),
    receivedMessages (s <+> ob)
      =
    if decide (isReceive ob) then message ob :: receivedMessages s else receivedMessages s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  receivedMessages (s <+> ob) =
  (if decide (isReceive ob)
   then message ob :: receivedMessages s
   else receivedMessages s)
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  receivedMessages (s <+> ob) =
  (if decide (isReceive ob)
   then message ob :: receivedMessages s
   else receivedMessages s)
  intros s ob.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
receivedMessages (s <+> ob) =
(if decide (isReceive ob)
 then message ob :: receivedMessages s
 else receivedMessages s)
  unfold receivedMessages, receivedMessages'; cbn.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
map message
  (if decide (isReceive ob)
   then ob :: filter isReceive (obs s)
   else filter isReceive (obs s)) =
(if decide (isReceive ob)
 then
  message ob :: map message (filter isReceive (obs s))
 else map message (filter isReceive (obs s)))
  by destruct (decide (isReceive ob)).
Qed.

Lemma elem_of_messages :
  forall (s : State) (m : Message),
    m ∈ messages s <-> m ∈ sentMessages s \/ m ∈ receivedMessages s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (m : Message),
  m ∈ messages s
  ↔ m ∈ sentMessages s ∨ m ∈ receivedMessages s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (m : Message),
  m ∈ messages s
  ↔ m ∈ sentMessages s ∨ m ∈ receivedMessages s
  intros; unfold messages, messages'.Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
m ∈ map message (obs s)
↔ m ∈ sentMessages s ∨ m ∈ receivedMessages s
  rewrite elem_of_sentMessages, elem_of_receivedMessages, elem_of_list_fmap.Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
(∃ y : Observation, m = message y ∧ y ∈ obs s)
↔ MkObservation Send m ∈ obs s
  ∨ MkObservation Receive m ∈ obs s
  split.Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
(∃ y : Observation, m = message y ∧ y ∈ obs s)
→ MkObservation Send m ∈ obs s
  ∨ MkObservation Receive m ∈ obs s
Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
MkObservation Send m ∈ obs s
∨ MkObservation Receive m ∈ obs s
→ ∃ y : Observation, m = message y ∧ y ∈ obs s
  -Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
(∃ y : Observation, m = message y ∧ y ∈ obs s)
→ MkObservation Send m ∈ obs s
  ∨ MkObservation Receive m ∈ obs s by intros [[[]] [-> Hm]]; auto.
  -Address: Type
EqDecision0: EqDecision Address
s: State
m: Message
MkObservation Send m ∈ obs s
∨ MkObservation Receive m ∈ obs s
→ ∃ y : Observation, m = message y ∧ y ∈ obs s by intros []; (eexists; split; [| eauto]).
Qed.

A message in s <+> ob is either the message of the added observation ob or a message in the original state.

Lemma elem_of_messages_addObservation :
  forall (s : State) (ob : Observation) (m : Message),
    m ∈ messages (s <+> ob) <-> m = message ob \/ m ∈ messages s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (m : Message),
  m ∈ messages (s <+> ob)
  ↔ m = message ob ∨ m ∈ messages s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (m : Message),
  m ∈ messages (s <+> ob)
  ↔ m = message ob ∨ m ∈ messages s
  by intros; apply elem_of_cons.
Qed.

Lemma messages_addObservation :
  forall (s : State) (ob : Observation),
    messages (s <+> ob) = message ob :: messages s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  messages (s <+> ob) = message ob :: messages s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  messages (s <+> ob) = message ob :: messages s done. Qed.

An address in receivedAddresses (s <+> ob) is either in receivedAddresses s or is the address from the message in the new observation ob, and can only be from ob if that is a Receive observation.

Lemma elem_of_receivedAddresses :
  forall (s : State) (ob : Observation) (a : Address),
    a ∈ receivedAddresses (s <+> ob)
      <->
    a = adr (state (message ob)) /\ isReceive ob \/ a ∈ receivedAddresses s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (a : Address),
  a ∈ receivedAddresses (s <+> ob)
  ↔ a = adr (state (message ob)) ∧ isReceive ob
    ∨ a ∈ receivedAddresses s
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation) (a : Address),
  a ∈ receivedAddresses (s <+> ob)
  ↔ a = adr (state (message ob)) ∧ isReceive ob
    ∨ a ∈ receivedAddresses s
  intros s ob a.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
a: Address
a ∈ receivedAddresses (s <+> ob)
↔ a = adr (state (message ob)) ∧ isReceive ob
  ∨ a ∈ receivedAddresses s
  unfold receivedAddresses, receivedMessages, receivedMessages'.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
a: Address
a
∈ map (λ m : Message, adr (state m))
    (map message (filter isReceive (obs (s <+> ob))))
↔ a = adr (state (message ob)) ∧ isReceive ob
  ∨ a
    ∈ map (λ m : Message, adr (state m))
        (map message (filter isReceive (obs s)))
  by rewrite !map_map, elem_of_map_filter_addObservation.
Qed.

Lemma receivedAddresses_addObservation :
  forall (s : State) (ob : Observation),
    receivedAddresses (s <+> ob)
      =
    if decide (isReceive ob)
    then adr (state (message ob)) :: receivedAddresses s
    else receivedAddresses s.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  receivedAddresses (s <+> ob) =
  (if decide (isReceive ob)
   then
    adr (state (message ob)) :: receivedAddresses s
   else receivedAddresses s)
Proof.Address: Type
EqDecision0: EqDecision Address
∀ (s : State) (ob : Observation),
  receivedAddresses (s <+> ob) =
  (if decide (isReceive ob)
   then
    adr (state (message ob)) :: receivedAddresses s
   else receivedAddresses s)
  intros s ob.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
receivedAddresses (s <+> ob) =
(if decide (isReceive ob)
 then adr (state (message ob)) :: receivedAddresses s
 else receivedAddresses s)
  unfold receivedAddresses; cbn.Address: Type
EqDecision0: EqDecision Address
s: State
ob: Observation
map (λ m : Message, adr (state m))
  (map message
     (if decide (isReceive ob)
      then ob :: filter isReceive (obs s)
      else filter isReceive (obs s))) =
(if decide (isReceive ob)
 then
  adr (state (message ob))
  :: map (λ m : Message, adr (state m))
       (receivedMessages s)
 else
  map (λ m : Message, adr (state m))
    (receivedMessages s))
  by destruct (decide (isReceive ob)).
Qed.

End sec_base_ELMO.

Notation "s <+> ob" := (addObservation ob s) (left associativity, at level 50).
Notation "s <++> obs" := (addObservations obs s) (left associativity, at level 50).
Notation "m <*> ob" := (addObservationToMessage ob m) (left associativity, at level 50).
Notation "m <**> obs" := (addObservationsToMessage obs m) (left associativity, at level 50).

Section sec_BaseELMO_Observations.

Context
  {Address : Type}
  `{EqDecision Address}
  (State := @State Address)
  (Observation := @Observation Address)
  (Message := @Message Address)
  .

Definition ELMO_component_type : VLSMType Message :=
{|
  VLSM.state := State;
  VLSM.label := Label;
|}.

We can extract a trace from a list of Observations.

Fixpoint observations2trace (obs : list Observation) (adr : Address)
  : list (transition_item ELMO_component_type) :=
  match obs with
  | [] => []
  | MkObservation Send msg as ob :: obs =>
      let s'   := MkState obs adr in
      let msg' := MkMessage s' in
      let ob'  := MkObservation Send msg' in
      let obs' := addObservation' ob' obs in
      let dest := MkState obs' adr in
        observations2trace obs adr ++
          [Build_transition_item ELMO_component_type Send None dest (Some msg')]
  | MkObservation Receive msg as ob :: obs =>
      let dest := MkState (ob :: obs) adr in
        observations2trace obs adr ++
          [Build_transition_item ELMO_component_type Receive (Some msg) dest None]
  end.

A state contains a list of observations, so we can extract a trace from a state.

Definition state2trace (s : State) : list transition_item :=
  observations2trace (obs s) (adr s).

Observations and message dependencies

Lemma obs_sizeState :
  forall (s : State) (ob : Observation), ob ∈ obs s ->
    sizeState (state (message ob)) < sizeState s.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (ob : Observation),
  ob ∈ obs s
  → sizeState (state (message ob)) < sizeState s
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (ob : Observation),
  ob ∈ obs s
  → sizeState (state (message ob)) < sizeState s
  induction s using addObservation_ind; inversion 1; subst.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
ob: BaseELMO.Observation
s: BaseELMO.State
IHs: ∀ ob : Observation,
  ob ∈ obs s
  → sizeState (state (message ob)) < sizeState s
H: ob ∈ obs (s <+> ob)
sizeState (state (message ob)) < sizeState (s <+> ob)
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
ob: BaseELMO.Observation
s: BaseELMO.State
IHs: ∀ ob : Observation,
  ob ∈ obs s
  → sizeState (state (message ob)) < sizeState s
ob0: Observation
H: ob0 ∈ obs (s <+> ob)
H2: ob0 ∈ obs s
sizeState (state (message ob0)) < sizeState (s <+> ob)
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
ob: BaseELMO.Observation
s: BaseELMO.State
IHs: ∀ ob : Observation,
  ob ∈ obs s
  → sizeState (state (message ob)) < sizeState s
H: ob ∈ obs (s <+> ob)
sizeState (state (message ob)) < sizeState (s <+> ob) by destruct ob as [? []]; unfold sizeState; cbn; lia.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
ob: BaseELMO.Observation
s: BaseELMO.State
IHs: ∀ ob : Observation,
  ob ∈ obs s
  → sizeState (state (message ob)) < sizeState s
ob0: Observation
H: ob0 ∈ obs (s <+> ob)
H2: ob0 ∈ obs s
sizeState (state (message ob0)) < sizeState (s <+> ob) etransitivity; [by apply IHs |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
ob: BaseELMO.Observation
s: BaseELMO.State
IHs: ∀ ob : Observation,
  ob ∈ obs s
  → sizeState (state (message ob)) < sizeState s
ob0: Observation
H: ob0 ∈ obs (s <+> ob)
H2: ob0 ∈ obs s
sizeState s < sizeState (s <+> ob)
    by destruct s, ob as [? []]; unfold sizeState; cbn; lia.
Qed.

Lemma messages_sizeState :
  forall (s : State) (m : Message), m ∈ messages s ->
    sizeState (state m) < sizeState s.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (m : Message),
  m ∈ messages s → sizeState (state m) < sizeState s
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (m : Message),
  m ∈ messages s → sizeState (state m) < sizeState s
  intros s m Hm.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: State
m: Message
Hm: m ∈ messages s
sizeState (state m) < sizeState s
  apply elem_of_list_fmap in Hm as (o & -> & Hobs).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: State
o: BaseELMO.Observation
Hobs: o ∈ obs s
sizeState (state (message o)) < sizeState s
  by apply obs_sizeState.
Qed.

Inductive rec_obs : State -> Observation -> Prop :=
| rec_new :
    forall (s : State) (ob : Observation),
      rec_obs (s <+> ob) ob
| rec_prev :
    forall (s : State) (ob' ob : Observation),
      rec_obs s ob -> rec_obs (s <+> ob') ob
| rec_recv :
    forall (s : State) (m : Message) (ob : Observation),
      rec_obs (state m) ob -> rec_obs (s <+> MkObservation Receive m) ob.

Equations rec_obs_fn (s : State) : listset Observation by wf (sizeState s) lt :=
| {| obs := [] |} => ∅
| {| obs := o :: os; adr := a |} =>
  {[ o ]} ∪ rec_obs_fn (state (message o)) ∪ rec_obs_fn {| obs := os; adr := a |}.
Next Obligation.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (o : BaseELMO.Observation) (os : list
                                     BaseELMO.Observation) 
  (a : Address),
  (∀ x : State,
     sizeState x <
     sizeState {| obs := o :: os; adr := a |}
     → listset Observation)
  → sizeState (state (message o)) <
    sizeState {| obs := o :: os; adr := a |}
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (o : BaseELMO.Observation) (os : list
                                     BaseELMO.Observation) 
  (a : Address),
  (∀ x : State,
     sizeState x <
     sizeState {| obs := o :: os; adr := a |}
     → listset Observation)
  → sizeState (state (message o)) <
    sizeState {| obs := o :: os; adr := a |} by intros [? []] os a _; unfold sizeState; cbn; lia. Qed.
Next Obligation.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (o : BaseELMO.Observation) (os : list
                                     BaseELMO.Observation) 
  (a : Address),
  (∀ x : State,
     sizeState x <
     sizeState {| obs := o :: os; adr := a |}
     → listset Observation)
  → sizeState {| obs := os; adr := a |} <
    sizeState {| obs := o :: os; adr := a |}
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (o : BaseELMO.Observation) (os : list
                                     BaseELMO.Observation) 
  (a : Address),
  (∀ x : State,
     sizeState x <
     sizeState {| obs := o :: os; adr := a |}
     → listset Observation)
  → sizeState {| obs := os; adr := a |} <
    sizeState {| obs := o :: os; adr := a |} by intros [? []] os a _; unfold sizeState; cbn; lia. Qed.

Lemma elem_of_rec_obs_fn_1 :
  forall (s : State) (o : Observation),
    rec_obs s o -> o ∈ rec_obs_fn s.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (o : Observation),
  rec_obs s o → o ∈ rec_obs_fn s
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (o : Observation),
  rec_obs s o → o ∈ rec_obs_fn s
  intro s; apply_funelim (rec_obs_fn s); clear s; [by inversion 1 |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (o : BaseELMO.Observation) (os : list
                                     BaseELMO.Observation) 
  (a : Address),
  (∀ o0 : Observation,
     rec_obs (state (message o)) o0
     → o0 ∈ rec_obs_fn (state (message o)))
  → (∀ o0 : Observation,
       rec_obs {| obs := os; adr := a |} o0
       → o0 ∈ rec_obs_fn {| obs := os; adr := a |})
    → ∀ o0 : Observation,
        rec_obs {| obs := o :: os; adr := a |} o0
        → o0
          ∈ {[o]} ∪ rec_obs_fn (state (message o))
            ∪ rec_obs_fn {| obs := os; adr := a |}
  by intros [] os a Hindm Hindos o; inversion 1 as [[] ? | [] ? | [] ?]; subst;
    cbn in *; unfold Observation; rewrite !elem_of_union, ?elem_of_singleton; itauto.
Qed.

Lemma rec_obs_fn_sizeState :
  forall (s : State) (o : Observation), o ∈ rec_obs_fn s ->
    sizeState (state (message o)) < sizeState s.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (o : Observation),
  o ∈ rec_obs_fn s
  → sizeState (state (message o)) < sizeState s
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (s : State) (o : Observation),
  o ∈ rec_obs_fn s
  → sizeState (state (message o)) < sizeState s
  intro s; apply_funelim (rec_obs_fn s); clear s;
    [intros * Ho; contradict Ho; apply not_elem_of_empty |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ (o : BaseELMO.Observation) (os : list
                                     BaseELMO.Observation) 
  (a : Address),
  (∀ o0 : Observation,
     o0 ∈ rec_obs_fn (state (message o))
     → sizeState (state (message o0)) <
       sizeState (state (message o)))
  → (∀ o0 : Observation,
       o0 ∈ rec_obs_fn {| obs := os; adr := a |}
       → sizeState (state (message o0)) <
         sizeState {| obs := os; adr := a |})
    → ∀ o0 : Observation,
        o0
        ∈ {[o]} ∪ rec_obs_fn (state (message o))
          ∪ rec_obs_fn {| obs := os; adr := a |}
        → sizeState (state (message o0)) <
          sizeState {| obs := o :: os; adr := a |}
  intros o os a Hindo Hindos o0; rewrite !elem_of_union; intros [[Heq | Ho] | Hos].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Heq: o0 ∈ {[o]}
sizeState (state (message o0)) <
sizeState {| obs := o :: os; adr := a |}
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Ho: o0 ∈ rec_obs_fn (state (message o))
sizeState (state (message o0)) <
sizeState {| obs := o :: os; adr := a |}
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Hos: o0 ∈ rec_obs_fn {| obs := os; adr := a |}
sizeState (state (message o0)) <
sizeState {| obs := o :: os; adr := a |}
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Heq: o0 ∈ {[o]}
sizeState (state (message o0)) <
sizeState {| obs := o :: os; adr := a |} apply elem_of_singleton in Heq as ->.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
sizeState (state (message o)) <
sizeState {| obs := o :: os; adr := a |}
    by unfold sizeState; destruct o as [? []]; cbn; lia.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Ho: o0 ∈ rec_obs_fn (state (message o))
sizeState (state (message o0)) <
sizeState {| obs := o :: os; adr := a |} transitivity (sizeState (state (message o))); [by apply Hindo |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Ho: o0 ∈ rec_obs_fn (state (message o))
sizeState (state (message o)) <
sizeState {| obs := o :: os; adr := a |}
    by unfold sizeState; destruct o as [? []]; cbn; lia.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Hos: o0 ∈ rec_obs_fn {| obs := os; adr := a |}
sizeState (state (message o0)) <
sizeState {| obs := o :: os; adr := a |} transitivity (sizeState (MkState os a)); [by apply Hindos |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
o: BaseELMO.Observation
os: list BaseELMO.Observation
a: Address
Hindo: ∀ o0 : Observation,
  o0 ∈ rec_obs_fn (state (message o))
  → sizeState (state (message o0)) <
    sizeState (state (message o))
Hindos: ∀ o : Observation,
  o ∈ rec_obs_fn {| obs := os; adr := a |}
  → sizeState (state (message o)) <
    sizeState {| obs := os; adr := a |}
o0: Observation
Hos: o0 ∈ rec_obs_fn {| obs := os; adr := a |}
sizeState {| obs := os; adr := a |} <
sizeState {| obs := o :: os; adr := a |}
    by unfold sizeState; destruct o as [? []]; cbn; lia.
Qed.

Definition Message_dependencies (m : Message) : listset Message :=
  list_to_set (map message (obs (state m))).

Definition Message_full_dependencies (m : Message) : listset Message :=
  fin_sets.set_map message (rec_obs_fn (state m)).

Lemma Message_full_dependencies_sizeState (dm m : Message) :
  dm ∈ Message_full_dependencies m -> sizeState (state dm) < sizeState (state m).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
dm, m: Message
dm ∈ Message_full_dependencies m
→ sizeState (state dm) < sizeState (state m)
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
dm, m: Message
dm ∈ Message_full_dependencies m
→ sizeState (state dm) < sizeState (state m)
  unfold Message_full_dependencies; intro Hdm.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
dm, m: Message
Hdm: dm ∈ set_map message (rec_obs_fn (state m))
sizeState (state dm) < sizeState (state m)
  apply elem_of_map in Hdm as (o & -> & Ho).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
m: Message
o: BaseELMO.Observation
Ho: o ∈ rec_obs_fn (state m)
sizeState (state (message o)) < sizeState (state m)
  by apply rec_obs_fn_sizeState.
Qed.

#[export] Instance Message_FullMessageDependencies :
  FullMessageDependencies Message_dependencies Message_full_dependencies.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
FullMessageDependencies Message_dependencies
  Message_full_dependencies
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
FullMessageDependencies Message_dependencies
  Message_full_dependencies
  constructor; [| by intros m Hm; apply Message_full_dependencies_sizeState in Hm; lia].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
∀ dm m : Message,
  dm ∈ Message_full_dependencies m
  ↔ msg_dep_happens_before Message_dependencies dm m
  intros dm [s]; revert dm; unfold Message_full_dependencies; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
∀ dm : Message,
  dm ∈ set_map message (rec_obs_fn s)
  ↔ msg_dep_happens_before Message_dependencies dm
      {| state := s |}
  apply_funelim (rec_obs_fn s);
    [intros adr dm; split | intros [l m] os a Hindm Hindos dm; split].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
adr: Address
dm: Message
dm ∈ set_map message ∅
→ msg_dep_happens_before Message_dependencies dm
    {| state := {| obs := []; adr := adr |} |}
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
adr: Address
dm: Message
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := []; adr := adr |} |}
→ dm ∈ set_map message ∅
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
dm
∈ set_map message
    ({[{| label := l; message := m |}]}
     ∪ rec_obs_fn
         (state
            (message {| label := l; message := m |}))
     ∪ rec_obs_fn {| obs := os; adr := a |})
→ msg_dep_happens_before Message_dependencies dm
    {|
      state :=
        {|
          obs := {| label := l; message := m |} :: os;
          adr := a
        |}
    |}
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
msg_dep_happens_before Message_dependencies dm
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
→ dm
  ∈ set_map message
      ({[{| label := l; message := m |}]}
       ∪ rec_obs_fn
           (state
              (message {| label := l; message := m |}))
       ∪ rec_obs_fn {| obs := os; adr := a |})
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
adr: Address
dm: Message
dm ∈ set_map message ∅
→ msg_dep_happens_before Message_dependencies dm
    {| state := {| obs := []; adr := adr |} |} by rewrite set_map_empty, elem_of_empty.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
adr: Address
dm: Message
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := []; adr := adr |} |}
→ dm ∈ set_map message ∅ rewrite msg_dep_happens_before_iff_one; unfold msg_dep_rel; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
adr: Address
dm: Message
dm ∈ ∅
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies dm y
     ∧ y ∈ ∅) → dm ∈ set_map message ∅
    rewrite set_map_empty; setoid_rewrite elem_of_empty.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
adr: Address
dm: Message
False
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies dm y
     ∧ False) → False
    by firstorder.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
dm
∈ set_map message
    ({[{| label := l; message := m |}]}
     ∪ rec_obs_fn
         (state
            (message {| label := l; message := m |}))
     ∪ rec_obs_fn {| obs := os; adr := a |})
→ msg_dep_happens_before Message_dependencies dm
    {|
      state :=
        {|
          obs := {| label := l; message := m |} :: os;
          adr := a
        |}
    |} intros Hdm; apply elem_of_map in Hdm as (o & -> & Hdm).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hdm: o
∈ {[{| label := l; message := m |}]}
  ∪ rec_obs_fn
      (state
         (message {| label := l; message := m |}))
  ∪ rec_obs_fn {| obs := os; adr := a |}
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
    unfold Message in Hdm; rewrite !elem_of_union, !elem_of_singleton in Hdm; cbn in Hdm.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hdm: (o = {| label := l; message := m |}
 ∨ o ∈ rec_obs_fn (state m))
∨ o ∈ rec_obs_fn {| obs := os; adr := a |}
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
    destruct Hdm as [[-> | Hm] | Hos].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
msg_dep_happens_before Message_dependencies
  (message {| label := l; message := m |})
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
    +Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
msg_dep_happens_before Message_dependencies
  (message {| label := l; message := m |})
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |} apply msg_dep_happens_before_iff_one; left.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
msg_dep_rel Message_dependencies
  (message {| label := l; message := m |})
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
      unfold msg_dep_rel, compose; cbn; unfold Message.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
m ∈ {[m]} ∪ list_to_set (map message os)
      by rewrite elem_of_union, elem_of_singleton; left.
    +Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |} transitivity m; cbn in *.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm ∈ set_map message (rec_obs_fn (state m))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {| state := state m |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
msg_dep_happens_before Message_dependencies
  (message o) m
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm ∈ set_map message (rec_obs_fn (state m))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {| state := state m |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
msg_dep_happens_before Message_dependencies m
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
      *Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm ∈ set_map message (rec_obs_fn (state m))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {| state := state m |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
msg_dep_happens_before Message_dependencies
  (message o) m by destruct m; apply Hindm, elem_of_map; cbn; eexists; split.
      *Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm ∈ set_map message (rec_obs_fn (state m))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {| state := state m |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
msg_dep_happens_before Message_dependencies m
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |} apply msg_dep_happens_before_iff_one; left.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm ∈ set_map message (rec_obs_fn (state m))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {| state := state m |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
msg_dep_rel Message_dependencies m
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
        unfold msg_dep_rel, compose; cbn; unfold Message.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm ∈ set_map message (rec_obs_fn (state m))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {| state := state m |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hm: o ∈ rec_obs_fn (state m)
m ∈ {[m]} ∪ list_to_set (map message os)
        by rewrite elem_of_union, elem_of_singleton; left.
    +Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |} assert (Hmos : message o ∈@{listset Message} set_map message (rec_obs_fn (MkState os a)))
        by (apply elem_of_map; eexists; split; done).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: message o
∈ set_map message
    (rec_obs_fn {| obs := os; adr := a |})
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
      apply Hindos in Hmos.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: msg_dep_happens_before Message_dependencies
  (message o)
  {| state := {| obs := os; adr := a |} |}
msg_dep_happens_before Message_dependencies
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
      cut (forall dm,
        msg_dep_rel Message_dependencies dm (MkMessage (MkState os a)) ->
        msg_dep_rel Message_dependencies dm (MkMessage (MkState (MkObservation l m :: os) a))).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: msg_dep_happens_before Message_dependencies
  (message o)
  {| state := {| obs := os; adr := a |} |}
(∀ dm : Message,
   msg_dep_rel Message_dependencies dm
     {| state := {| obs := os; adr := a |} |}
   → msg_dep_rel Message_dependencies dm
       {|
         state :=
           {|
             obs :=
               {| label := l; message := m |} :: os;
             adr := a
           |}
       |})
→ msg_dep_happens_before Message_dependencies
    (message o)
    {|
      state :=
        {|
          obs := {| label := l; message := m |} :: os;
          adr := a
        |}
    |}
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: msg_dep_happens_before Message_dependencies
  (message o)
  {| state := {| obs := os; adr := a |} |}
∀ dm : Message,
  msg_dep_rel Message_dependencies dm
    {| state := {| obs := os; adr := a |} |}
  → msg_dep_rel Message_dependencies dm
      {|
        state :=
          {|
            obs :=
              {| label := l; message := m |} :: os;
            adr := a
          |}
      |}
      {Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: msg_dep_happens_before Message_dependencies
  (message o)
  {| state := {| obs := os; adr := a |} |}
(∀ dm : Message,
   msg_dep_rel Message_dependencies dm
     {| state := {| obs := os; adr := a |} |}
   → msg_dep_rel Message_dependencies dm
       {|
         state :=
           {|
             obs :=
               {| label := l; message := m |} :: os;
             adr := a
           |}
       |})
→ msg_dep_happens_before Message_dependencies
    (message o)
    {|
      state :=
        {|
          obs := {| label := l; message := m |} :: os;
          adr := a
        |}
    |}
        intro Hext; apply msg_dep_happens_before_iff_one.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: msg_dep_happens_before Message_dependencies
  (message o)
  {| state := {| obs := os; adr := a |} |}
Hext: ∀ dm : Message,
  msg_dep_rel Message_dependencies dm
    {| state := {| obs := os; adr := a |} |}
  → msg_dep_rel Message_dependencies dm
      {|
        state :=
          {|
            obs :=
              {| label := l; message := m |}
              :: os;
            adr := a
          |}
      |}
msg_dep_rel Message_dependencies (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies
       (message o) y
     ∧ msg_dep_rel Message_dependencies y
         {|
           state :=
             {|
               obs :=
                 {| label := l; message := m |} :: os;
               adr := a
             |}
         |})
        apply msg_dep_happens_before_iff_one in Hmos as [Hdep | (dm & Hhb & Hdep)].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hdep: msg_dep_rel Message_dependencies 
  (message o)
  {| state := {| obs := os; adr := a |} |}
Hext: ∀ dm : Message,
  msg_dep_rel Message_dependencies dm
    {| state := {| obs := os; adr := a |} |}
  → msg_dep_rel Message_dependencies dm
      {|
        state :=
          {|
            obs :=
              {| label := l; message := m |}
              :: os;
            adr := a
          |}
      |}
msg_dep_rel Message_dependencies (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies
       (message o) y
     ∧ msg_dep_rel Message_dependencies y
         {|
           state :=
             {|
               obs :=
                 {| label := l; message := m |} :: os;
               adr := a
             |}
         |})
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
dm: Message
Hhb: msg_dep_happens_before Message_dependencies
  (message o) dm
Hdep: msg_dep_rel Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
Hext: ∀ dm : Message,
  msg_dep_rel Message_dependencies dm
    {| state := {| obs := os; adr := a |} |}
  → msg_dep_rel Message_dependencies dm
      {|
        state :=
          {|
            obs :=
              {| label := l; message := m |}
              :: os;
            adr := a
          |}
      |}
msg_dep_rel Message_dependencies 
  (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies
       (message o) y
     ∧ msg_dep_rel Message_dependencies y
         {|
           state :=
             {|
               obs :=
                 {| label := l; message := m |} :: os;
               adr := a
             |}
         |})
        -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hdep: msg_dep_rel Message_dependencies 
  (message o)
  {| state := {| obs := os; adr := a |} |}
Hext: ∀ dm : Message,
  msg_dep_rel Message_dependencies dm
    {| state := {| obs := os; adr := a |} |}
  → msg_dep_rel Message_dependencies dm
      {|
        state :=
          {|
            obs :=
              {| label := l; message := m |}
              :: os;
            adr := a
          |}
      |}
msg_dep_rel Message_dependencies (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies
       (message o) y
     ∧ msg_dep_rel Message_dependencies y
         {|
           state :=
             {|
               obs :=
                 {| label := l; message := m |} :: os;
               adr := a
             |}
         |}) by left; apply Hext.
        -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
dm: Message
Hhb: msg_dep_happens_before Message_dependencies
  (message o) dm
Hdep: msg_dep_rel Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
Hext: ∀ dm : Message,
  msg_dep_rel Message_dependencies dm
    {| state := {| obs := os; adr := a |} |}
  → msg_dep_rel Message_dependencies dm
      {|
        state :=
          {|
            obs :=
              {| label := l; message := m |}
              :: os;
            adr := a
          |}
      |}
msg_dep_rel Message_dependencies (message o)
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies
       (message o) y
     ∧ msg_dep_rel Message_dependencies y
         {|
           state :=
             {|
               obs :=
                 {| label := l; message := m |} :: os;
               adr := a
             |}
         |}) by right; eexists; split; [| apply Hext].
      }Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: msg_dep_happens_before Message_dependencies
  (message o)
  {| state := {| obs := os; adr := a |} |}
∀ dm : Message,
  msg_dep_rel Message_dependencies dm
    {| state := {| obs := os; adr := a |} |}
  → msg_dep_rel Message_dependencies dm
      {|
        state :=
          {|
            obs :=
              {| label := l; message := m |} :: os;
            adr := a
          |}
      |}
      unfold msg_dep_rel; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
o: BaseELMO.Observation
Hos: o ∈ rec_obs_fn {| obs := os; adr := a |}
Hmos: msg_dep_happens_before Message_dependencies
  (message o)
  {| state := {| obs := os; adr := a |} |}
∀ dm : Message,
  dm ∈ list_to_set (map message os)
  → dm ∈ {[m]} ∪ list_to_set (map message os)
      by intros dm; rewrite elem_of_union; right.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
msg_dep_happens_before Message_dependencies dm
  {|
    state :=
      {|
        obs := {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
→ dm
  ∈ set_map message
      ({[{| label := l; message := m |}]}
       ∪ rec_obs_fn
           (state
              (message {| label := l; message := m |}))
       ∪ rec_obs_fn {| obs := os; adr := a |}) intros Hb; apply elem_of_map.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: msg_dep_happens_before Message_dependencies dm
  {|
    state :=
      {|
        obs :=
          {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ x
    ∈ {[{| label := l; message := m |}]}
      ∪ rec_obs_fn
          (state
             (message {| label := l; message := m |}))
      ∪ rec_obs_fn {| obs := os; adr := a |}
    do 2 setoid_rewrite elem_of_union; setoid_rewrite elem_of_singleton; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: msg_dep_happens_before Message_dependencies dm
  {|
    state :=
      {|
        obs :=
          {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
    apply msg_dep_happens_before_iff_one in Hb.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: msg_dep_rel Message_dependencies dm
  {|
    state :=
      {|
        obs :=
          {| label := l; message := m |} :: os;
        adr := a
      |}
  |}
∨ (∃ y : Message,
     msg_dep_happens_before Message_dependencies
       dm y
     ∧ msg_dep_rel Message_dependencies y
         {|
           state :=
             {|
               obs :=
                 {| label := l; message := m |}
                 :: os;
               adr := a
             |}
         |})
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
    unfold msg_dep_rel, compose in Hb; cbn in Hb; unfold Message in Hb.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: dm ∈ {[m]} ∪ list_to_set (map message os)
∨ (∃ y : BaseELMO.Message,
     msg_dep_happens_before Message_dependencies
       dm y
     ∧ y ∈ {[m]} ∪ list_to_set (map message os))
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
    setoid_rewrite elem_of_union in Hb;
      setoid_rewrite elem_of_singleton in Hb.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: (dm = m ∨ dm ∈ list_to_set (map message os))
∨ (∃ y : BaseELMO.Message,
     msg_dep_happens_before Message_dependencies
       dm y
     ∧ (y = m ∨ y ∈ list_to_set (map message os)))
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
    destruct Hb as [[-> | Hdm] | Hos].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
∃ x : BaseELMO.Observation,
  m = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hdm: dm ∈ list_to_set (map message os)
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hos: ∃ y : BaseELMO.Message,
  msg_dep_happens_before Message_dependencies dm
    y
  ∧ (y = m ∨ y ∈ list_to_set (map message os))
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
    +Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
∃ x : BaseELMO.Observation,
  m = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |}) by eexists; split; [| by left; left].
    +Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hdm: dm ∈ list_to_set (map message os)
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |}) cut (msg_dep_happens_before Message_dependencies dm (MkMessage (MkState os a))).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hdm: dm ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
→ ∃ x : BaseELMO.Observation,
    dm = message x
    ∧ ((x = {| label := l; message := m |}
        ∨ x ∈ rec_obs_fn (state m))
       ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hdm: dm ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
      {Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hdm: dm ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
→ ∃ x : BaseELMO.Observation,
    dm = message x
    ∧ ((x = {| label := l; message := m |}
        ∨ x ∈ rec_obs_fn (state m))
       ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
        intro Hb; apply Hindos, elem_of_map in Hb as (y & -> & Hy).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
y: BaseELMO.Observation
Hdm: message y ∈ list_to_set (map message os)
Hy: y ∈ rec_obs_fn {| obs := os; adr := a |}
∃ x : BaseELMO.Observation,
  message y = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
        by eexists; split; [| right].
      }Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hdm: dm ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
      by apply msg_dep_happens_before_iff_one; left.
    +Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hos: ∃ y : BaseELMO.Message,
  msg_dep_happens_before Message_dependencies dm
    y
  ∧ (y = m ∨ y ∈ list_to_set (map message os))
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |}) destruct Hos as (y & Hb & [-> | Hos]).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: msg_dep_happens_before Message_dependencies dm m
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
y: BaseELMO.Message
Hb: msg_dep_happens_before Message_dependencies dm y
Hos: y ∈ list_to_set (map message os)
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
      *Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: msg_dep_happens_before Message_dependencies dm m
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |}) destruct m as [state_m].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
state_m: BaseELMO.State
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {|
                 label := l;
                 message :=
                   {| state := state_m |}
               |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {|
                 label := l;
                 message :=
                   {| state := state_m |}
               |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
Hb: msg_dep_happens_before Message_dependencies dm
  {| state := state_m |}
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x =
      {|
        label := l; message := {| state := state_m |}
      |}
      ∨ x ∈ rec_obs_fn (state {| state := state_m |}))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
        apply Hindm, elem_of_map in Hb as (y & -> & Hy).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
state_m: BaseELMO.State
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {|
                 label := l;
                 message :=
                   {| state := state_m |}
               |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {|
                 label := l;
                 message :=
                   {| state := state_m |}
               |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
y: BaseELMO.Observation
Hy: y
∈ rec_obs_fn
    (state
       (message
          {|
            label := l;
            message := {| state := state_m |}
          |}))
∃ x : BaseELMO.Observation,
  message y = message x
  ∧ ((x =
      {|
        label := l; message := {| state := state_m |}
      |}
      ∨ x ∈ rec_obs_fn (state {| state := state_m |}))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
        by eexists; split; [| left; right].
      *Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
y: BaseELMO.Message
Hb: msg_dep_happens_before Message_dependencies dm y
Hos: y ∈ list_to_set (map message os)
∃ x : BaseELMO.Observation,
  dm = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |}) cut (msg_dep_happens_before Message_dependencies dm (MkMessage (MkState os a))).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
y: BaseELMO.Message
Hb: msg_dep_happens_before Message_dependencies dm y
Hos: y ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
→ ∃ x : BaseELMO.Observation,
    dm = message x
    ∧ ((x = {| label := l; message := m |}
        ∨ x ∈ rec_obs_fn (state m))
       ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
y: BaseELMO.Message
Hb: msg_dep_happens_before Message_dependencies dm y
Hos: y ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
        {Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
y: BaseELMO.Message
Hb: msg_dep_happens_before Message_dependencies dm y
Hos: y ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
→ ∃ x : BaseELMO.Observation,
    dm = message x
    ∧ ((x = {| label := l; message := m |}
        ∨ x ∈ rec_obs_fn (state m))
       ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
          intros (z & -> & Hz)%Hindos%elem_of_map.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
y: BaseELMO.Message
z: BaseELMO.Observation
Hb: msg_dep_happens_before Message_dependencies
  (message z) y
Hos: y ∈ list_to_set (map message os)
Hz: z ∈ rec_obs_fn {| obs := os; adr := a |}
∃ x : BaseELMO.Observation,
  message z = message x
  ∧ ((x = {| label := l; message := m |}
      ∨ x ∈ rec_obs_fn (state m))
     ∨ x ∈ rec_obs_fn {| obs := os; adr := a |})
          by eexists; split; [| right].
        }Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
y: BaseELMO.Message
Hb: msg_dep_happens_before Message_dependencies dm y
Hos: y ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies dm
  {| state := {| obs := os; adr := a |} |}
        transitivity y; [done |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
s: BaseELMO.State
l: Label
m: BaseELMO.Message
os: list BaseELMO.Observation
a: Address
Hindm: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn
         (state
            (message
               {| label := l; message := m |})))
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state :=
          state
            (message
               {| label := l; message := m |})
      |}
Hindos: ∀ dm : Message,
  dm
  ∈ set_map message
      (rec_obs_fn {| obs := os; adr := a |})
  ↔ msg_dep_happens_before
      Message_dependencies dm
      {|
        state := {| obs := os; adr := a |}
      |}
dm: Message
y: BaseELMO.Message
Hb: msg_dep_happens_before Message_dependencies dm y
Hos: y ∈ list_to_set (map message os)
msg_dep_happens_before Message_dependencies y
  {| state := {| obs := os; adr := a |} |}
        by apply msg_dep_happens_before_iff_one; left.
Qed.

Context
  `{finite.Finite index}
  `{Inhabited index}
  (idx : index -> Address)
  `{!Inj (=) (=) idx}
  .

Definition adr2idx (a : Address) : option index :=
  head (filter (fun i => idx i = a) (enum index)).

Lemma adr2idx_idx :
  forall (i : index),
    adr2idx (idx i) = Some i.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ i : index, adr2idx (idx i) = Some i
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ i : index, adr2idx (idx i) = Some i
  intro i; unfold adr2idx; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
head
  (filter (λ i0 : index, idx i0 = idx i) (enum index)) =
Some i
  replace (filter _ _) with [i]; [done |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
[i] =
filter (λ i0 : index, idx i0 = idx i) (enum index)
  generalize (enum index), (NoDup_enum index) as Hnodup, (elem_of_enum i) as Hi.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
∀ l : list index,
  NoDup l
  → i ∈ l
    → [i] = filter (λ i0 : index, idx i0 = idx i) l
  induction l; intros; [by inversion Hi |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
[i] = filter (λ i0 : index, idx i0 = idx i) (a :: l)
  inversion Hnodup; subst.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
[i] = filter (λ i0 : index, idx i0 = idx i) (a :: l)
  assert (Hnil : forall i, i ∉ l -> filter (fun i0 : index => idx i0 = idx i) l = []).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
∀ i : index,
  i ∉ l → filter (λ i0 : index, idx i0 = idx i) l = []
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
Hnil: ∀ i : index,
  i ∉ l
  → filter (λ i0 : index, idx i0 = idx i) l =
    []
[i] = filter (λ i0 : index, idx i0 = idx i) (a :: l)
  {Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
∀ i : index,
  i ∉ l → filter (λ i0 : index, idx i0 = idx i) l = []
    intros; apply Forall_filter_nil, Forall_forall.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
i0: index
H1: i0 ∉ l
∀ x : index, x ∈ l → idx x ≠ idx i0
    intros j Hj; contradict Hj.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
i0: index
H1: i0 ∉ l
j: index
Hj: idx j = idx i0
j ∉ l
    by eapply inj in Hj; [| done]; subst.
  }Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
Hnil: ∀ i : index,
  i ∉ l
  → filter (λ i0 : index, idx i0 = idx i) l =
    []
[i] = filter (λ i0 : index, idx i0 = idx i) (a :: l)
  inversion Hi; subst; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
a: index
l: list index
IHl: NoDup l
→ a ∈ l
  → [a] = filter (λ i : index, idx i = idx a) l
Hnodup: NoDup (a :: l)
Hi: a ∈ a :: l
H3: a ∉ l
H4: NoDup l
Hnil: ∀ i : index,
  i ∉ l
  → filter (λ i0 : index, idx i0 = idx i) l =
    []
[a] =
(if decide (idx a = idx a)
 then a :: filter (λ i : index, idx i = idx a) l
 else filter (λ i : index, idx i = idx a) l)
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
Hnil: ∀ i : index,
  i ∉ l
  → filter (λ i0 : index, idx i0 = idx i) l =
    []
H5: i ∈ l
[i] =
(if decide (idx a = idx i)
 then a :: filter (λ i0 : index, idx i0 = idx i) l
 else filter (λ i0 : index, idx i0 = idx i) l)
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
a: index
l: list index
IHl: NoDup l
→ a ∈ l
  → [a] = filter (λ i : index, idx i = idx a) l
Hnodup: NoDup (a :: l)
Hi: a ∈ a :: l
H3: a ∉ l
H4: NoDup l
Hnil: ∀ i : index,
  i ∉ l
  → filter (λ i0 : index, idx i0 = idx i) l =
    []
[a] =
(if decide (idx a = idx a)
 then a :: filter (λ i : index, idx i = idx a) l
 else filter (λ i : index, idx i = idx a) l) by rewrite decide_True, Hnil.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
Hnil: ∀ i : index,
  i ∉ l
  → filter (λ i0 : index, idx i0 = idx i) l =
    []
H5: i ∈ l
[i] =
(if decide (idx a = idx i)
 then a :: filter (λ i0 : index, idx i0 = idx i) l
 else filter (λ i0 : index, idx i0 = idx i) l) rewrite decide_False, IHl; [done.. |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i, a: index
l: list index
IHl: NoDup l
→ i ∈ l
  → [i] =
    filter (λ i0 : index, idx i0 = idx i) l
Hnodup: NoDup (a :: l)
Hi: i ∈ a :: l
H3: a ∉ l
H4: NoDup l
Hnil: ∀ i : index,
  i ∉ l
  → filter (λ i0 : index, idx i0 = idx i) l =
    []
H5: i ∈ l
idx a ≠ idx i
    by intro Hcontra; eapply inj in Hcontra; [| done]; subst.
Qed.

Lemma idx_adr2idx :
  forall (i : index) (adr : Address),
    adr2idx adr = Some i -> idx i = adr.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (i : index) (adr : Address),
  adr2idx adr = Some i → idx i = adr
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (i : index) (adr : Address),
  adr2idx adr = Some i → idx i = adr
  unfold adr2idx.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (i : index) (adr : Address),
  head
    (filter (λ i0 : index, idx i0 = adr) (enum index)) =
  Some i → idx i = adr
  intros i adr Heq.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
adr: Address
Heq: head
  (filter (λ i : index, idx i = adr)
     (enum index)) = Some i
idx i = adr
  apply (@elem_of_list_filter _ (fun i => idx i = adr) _ (enum index) i).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
adr: Address
Heq: head
  (filter (λ i : index, idx i = adr)
     (enum index)) = Some i
i ∈ filter (λ i : index, idx i = adr) (enum index)
  destruct (filter _ _); inversion Heq; subst.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
adr: Address
y: list index
Heq: head (i :: y) = Some i
i ∈ i :: y
  by left.
Qed.

Definition Message_validator : Type :=
  dsig (is_Some ∘ adr2idx).

Definition Message_sender (m : Message) : option Message_validator :=
  let a := adr (state m) in
  match decide (is_Some (adr2idx a)) with
  | left Ha => Some (dexist a Ha)
  | _ => None
  end.

Lemma Message_sender_Some_adr :
  forall (m : Message) (v : Message_validator),
    Message_sender m = Some v -> `v = adr (state m).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (m : Message) (v : Message_validator),
  Message_sender m = Some v → `v = adr (state m)
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (m : Message) (v : Message_validator),
  Message_sender m = Some v → `v = adr (state m)
  unfold Message_sender; intros v mv Hsender; case_decide; [| done].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
v: Message
mv: Message_validator
H1: is_Some (adr2idx (adr (state v)))
Hsender: Some (dexist (adr (state v)) H1) = Some mv
`mv = adr (state v)
  by inversion Hsender.
Qed.

Lemma Message_sender_Some_adr_iff :
  forall (m : Message) (v : Message_validator),
    Message_sender m = Some v <-> `v = adr (state m).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (m : Message) (v : Message_validator),
  Message_sender m = Some v ↔ `v = adr (state m)
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (m : Message) (v : Message_validator),
  Message_sender m = Some v ↔ `v = adr (state m)
  split; [by apply Message_sender_Some_adr |].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
v: Message_validator
`v = adr (state m) → Message_sender m = Some v
  unfold Message_sender; case_decide as Hdec; intros Hv.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
v: Message_validator
Hdec: is_Some (adr2idx (adr (state m)))
Hv: `v = adr (state m)
Some (dexist (adr (state m)) Hdec) = Some v
Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
v: Message_validator
Hdec: ¬ is_Some (adr2idx (adr (state m)))
Hv: `v = adr (state m)
None = Some v
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
v: Message_validator
Hdec: is_Some (adr2idx (adr (state m)))
Hv: `v = adr (state m)
Some (dexist (adr (state m)) Hdec) = Some v by f_equal; apply dsig_eq.
  -Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
v: Message_validator
Hdec: ¬ is_Some (adr2idx (adr (state m)))
Hv: `v = adr (state m)
None = Some v by destruct_dec_sig v a Ha Heq; subst v; cbn in Hv; subst a.
Qed.

Definition Message_sender_index (v : Message_validator) : index :=
  is_Some_proj (proj2_dsig v).

Definition Message_sender_index_inv_fn (i : index) : Message_validator :=
  dexist (idx i) (ex_intro _ i (adr2idx_idx i)).

Lemma Message_sender_index_inv :
  forall (i : index) (v : Message_validator),
    `v = idx i -> Message_sender_index v = i.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (i : index) (v : Message_validator),
  `v = idx i → Message_sender_index v = i
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (i : index) (v : Message_validator),
  `v = idx i → Message_sender_index v = i
  intros i v Hv.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
v: Message_validator
Hv: `v = idx i
Message_sender_index v = i
  destruct_dec_sig v a Ha Heq; subst v; cbn in Hv; subst a.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
i: index
Ha: (is_Some ∘ adr2idx) (idx i)
Message_sender_index (dexist (idx i) Ha) = i
  by apply is_Some_proj_elim, adr2idx_idx.
Qed.

Lemma Message_sender_index_address :
  forall (m : Message) (v : Message_validator),
    Message_sender m = Some v -> idx (Message_sender_index v) = adr (state m).Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (m : Message) (v : Message_validator),
  Message_sender m = Some v
  → idx (Message_sender_index v) = adr (state m)
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
∀ (m : Message) (v : Message_validator),
  Message_sender m = Some v
  → idx (Message_sender_index v) = adr (state m)
  intros m v Hsender.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
v: Message_validator
Hsender: Message_sender m = Some v
idx (Message_sender_index v) = adr (state m)
  apply Message_sender_Some_adr in Hsender.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
v: Message_validator
Hsender: `v = adr (state m)
idx (Message_sender_index v) = adr (state m)
  destruct_dec_sig v a Ha Heq; subst v.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
a: Address
Ha: (is_Some ∘ adr2idx) a
Hsender: `(dexist a Ha) = adr (state m)
idx (Message_sender_index (dexist a Ha)) =
adr (state m)
  cbn in Hsender; subst a.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
Ha: (is_Some ∘ adr2idx) (adr (state m))
idx (Message_sender_index (dexist (adr (state m)) Ha)) =
adr (state m)
  apply idx_adr2idx.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
Ha: (is_Some ∘ adr2idx) (adr (state m))
adr2idx (adr (state m)) =
Some
  (Message_sender_index (dexist (adr (state m)) Ha))
  destruct Ha as [a Heq].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
a: index
Heq: adr2idx (adr (state m)) = Some a
adr2idx (adr (state m)) =
Some
  (Message_sender_index
     (dexist (adr (state m))
        (ex_intro
           (λ x : index,
              adr2idx (adr (state m)) = Some x) a Heq)))
  rewrite Heq at 1.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
a: index
Heq: adr2idx (adr (state m)) = Some a
Some a =
Some
  (Message_sender_index
     (dexist (adr (state m))
        (ex_intro
           (λ x : index,
              adr2idx (adr (state m)) = Some x) a Heq)))
  f_equal; symmetry; apply Message_sender_index_inv; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
m: Message
a: index
Heq: adr2idx (adr (state m)) = Some a
adr (state m) = idx a
  by symmetry; apply idx_adr2idx.
Qed.

#[export] Instance Message_sender_index_inj : Inj (=) (=) Message_sender_index.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
Inj eq eq Message_sender_index
Proof.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
Inj eq eq Message_sender_index
  intros v1 v2.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
v1, v2: Message_validator
Message_sender_index v1 = Message_sender_index v2
→ v1 = v2
  destruct_dec_sig v1 a1 Ha1 Heq1; subst v1.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
v2: Message_validator
a1: Address
Ha1: (is_Some ∘ adr2idx) a1
Message_sender_index (dexist a1 Ha1) =
Message_sender_index v2 → dexist a1 Ha1 = v2
  destruct_dec_sig v2 a2 Ha2 Heq2; subst v2.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
a1: Address
Ha1: (is_Some ∘ adr2idx) a1
a2: Address
Ha2: (is_Some ∘ adr2idx) a2
Message_sender_index (dexist a1 Ha1) =
Message_sender_index (dexist a2 Ha2)
→ dexist a1 Ha1 = dexist a2 Ha2
  destruct Ha1 as [i1 Ha1], Ha2 as [i2 Ha2].Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
a1: Address
i1: index
Ha1: adr2idx a1 = Some i1
a2: Address
i2: index
Ha2: adr2idx a2 = Some i2
Message_sender_index
  (dexist a1
     (ex_intro (λ x : index, adr2idx a1 = Some x) i1
        Ha1)) =
Message_sender_index
  (dexist a2
     (ex_intro (λ x : index, adr2idx a2 = Some x) i2
        Ha2))
→ dexist a1
    (ex_intro (λ x : index, adr2idx a1 = Some x) i1
       Ha1) =
  dexist a2
    (ex_intro (λ x : index, adr2idx a2 = Some x) i2
       Ha2)
  unfold Message_sender_index; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
a1: Address
i1: index
Ha1: adr2idx a1 = Some i1
a2: Address
i2: index
Ha2: adr2idx a2 = Some i2
is_Some_proj
  (proj2_dsig
     (dexist a1
        (ex_intro (λ x : index, adr2idx a1 = Some x)
           i1 Ha1))) =
is_Some_proj
  (proj2_dsig
     (dexist a2
        (ex_intro (λ x : index, adr2idx a2 = Some x)
           i2 Ha2)))
→ dexist a1
    (ex_intro (λ x : index, adr2idx a1 = Some x) i1
       Ha1) =
  dexist a2
    (ex_intro (λ x : index, adr2idx a2 = Some x) i2
       Ha2)
  erewrite !is_Some_proj_elim by done.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
a1: Address
i1: index
Ha1: adr2idx a1 = Some i1
a2: Address
i2: index
Ha2: adr2idx a2 = Some i2
i1 = i2
→ dexist a1
    (ex_intro (λ x : index, adr2idx a1 = Some x) i1
       Ha1) =
  dexist a2
    (ex_intro (λ x : index, adr2idx a2 = Some x) i2
       Ha2)
  intros ->; apply dsig_eq; cbn.Address: Type
EqDecision0: EqDecision Address
State:= BaseELMO.State: Type
Observation:= BaseELMO.Observation: Type
Message:= BaseELMO.Message: Type
index: Type
EqDecision1: EqDecision index
H: finite.Finite index
H0: Inhabited index
idx: index → Address
Inj0: Inj eq eq idx
a1: Address
i2: index
Ha1: adr2idx a1 = Some i2
a2: Address
Ha2: adr2idx a2 = Some i2
a1 = a2
  by apply idx_adr2idx in Ha1, Ha2; subst.
Qed.

#[export] Instance Message_validator_measurable
  `{Measurable Address} : Measurable Message_validator :=
    fun v => weight (`v).

End sec_BaseELMO_Observations.

We want to display State, Observation and Message using constructors also outside of the current module.

Add Printing Constructor State Observation Message.