From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.
From Coq Require Import Eqdep Fin FunctionalExtensionality.
From VLSM.Lib Require Import Preamble.
From VLSM.Core Require Import VLSM PreloadedVLSM VLSMProjections Composition.

Core: VLSM Equivocation

An equivocator_vlsm for a given VLSM X is a VLSM which starts as a regular machine X, and then, at any moment:

can spawn a new machine in a (potentially) different initial state.
can perform valid transitions on any of its internal machines
can fork any of its internal machines by duplicating its state and then using the given label and message to transition on the new fork.

Note that we only allow forking if a transition is then taken on the neq fork.

Section sec_equivocator_vlsm.

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

The state of such a machine will be abstracted using

1. A natural n, stating the number of copies of the original machine 2. A state of X for each 1..n+1

#[local] Definition bounded_state_copies := {n : nat & Fin.t (S n) -> state X}.

To preserve determinism we need to enhance the labels to indicate what copy of the machine will be used for a transition. To achieve this, we'll define the following label variants:

Spawn s to extend the state with a new machine initialized with s
ContinueWith n l, to transition on copy n using label l
ForkWith n l, to extend the state with a new machine initialized with the current state of machine n and to transition on that copy using label l.

Inductive EquivocatorLabel : Type :=
| Spawn : state X -> EquivocatorLabel
| ContinueWith : nat -> label X -> EquivocatorLabel
| ForkWith : nat -> label X -> EquivocatorLabel.

Definition equivocator_type : VLSMType message :=
  {| state := bounded_state_copies ;
     label := EquivocatorLabel
  |}.

Definition equivocator_state : Type := state equivocator_type.
Definition equivocator_label : Type := label equivocator_type.

The number of machine copies in the given state.

Definition equivocator_state_n (es : equivocator_state) := S (projT1 es).

The index of the last machine copies in the given state.

Definition equivocator_state_last (es : equivocator_state) := projT1 es.
Definition equivocator_state_s (es : equivocator_state) := projT2 es.

Lemma equivocator_state_last_n es : equivocator_state_n es = S (equivocator_state_last es).message: Type
X: VLSM message
es: equivocator_state
equivocator_state_n es = S (equivocator_state_last es)
Proof.message: Type
X: VLSM message
es: equivocator_state
equivocator_state_n es = S (equivocator_state_last es) done. Qed.

Definition mk_singleton_state
  (s : state X)
  : equivocator_state
  :=
  existT 0 (fun _ => s).

#[local] Lemma equivocator_state_projection_irrel (s : equivocator_state)
  i (li : i < (equivocator_state_n s))
  j (lj : j < (equivocator_state_n s))
  (Heq : i = j)
  : equivocator_state_s s (nat_to_fin li) = equivocator_state_s s (nat_to_fin lj).message: Type
X: VLSM message
s: equivocator_state
i: nat
li: i < equivocator_state_n s
j: nat
lj: j < equivocator_state_n s
Heq: i = j
equivocator_state_s s (nat_to_fin li) =
equivocator_state_s s (nat_to_fin lj)
Proof.message: Type
X: VLSM message
s: equivocator_state
i: nat
li: i < equivocator_state_n s
j: nat
lj: j < equivocator_state_n s
Heq: i = j
equivocator_state_s s (nat_to_fin li) =
equivocator_state_s s (nat_to_fin lj)
  subst i.message: Type
X: VLSM message
s: equivocator_state
j: nat
li, lj: j < equivocator_state_n s
equivocator_state_s s (nat_to_fin li) =
equivocator_state_s s (nat_to_fin lj)
  by replace (nat_to_fin li) with (nat_to_fin lj) by apply of_nat_ext.
Qed.

#[local] Lemma equivocator_state_eq s (i1 i2 : fin (equivocator_state_n s))
  : fin_to_nat i1 = fin_to_nat i2 -> equivocator_state_s s i1 = equivocator_state_s s i2.message: Type
X: VLSM message
s: equivocator_state
i1, i2: fin (equivocator_state_n s)
i1 = i2
→ equivocator_state_s s i1 = equivocator_state_s s i2
Proof.message: Type
X: VLSM message
s: equivocator_state
i1, i2: fin (equivocator_state_n s)
i1 = i2
→ equivocator_state_s s i1 = equivocator_state_s s i2
  intro Heq.message: Type
X: VLSM message
s: equivocator_state
i1, i2: fin (equivocator_state_n s)
Heq: i1 = i2
equivocator_state_s s i1 = equivocator_state_s s i2
  replace i2 with i1; [done |].message: Type
X: VLSM message
s: equivocator_state
i1, i2: fin (equivocator_state_n s)
Heq: i1 = i2
i1 = i2
  by apply (inj fin_to_nat).
Qed.

Definition is_singleton_state
  (s : equivocator_state)
  : Prop
  := equivocator_state_n s = 1.

Lemma is_singleton_state_dec
  (s : equivocator_state)
  : Decision (is_singleton_state s).message: Type
X: VLSM message
s: equivocator_state
Decision (is_singleton_state s)
Proof.message: Type
X: VLSM message
s: equivocator_state
Decision (is_singleton_state s)
  by apply Nat.eq_dec.
Qed.

Definition is_equivocating_state
  (s : equivocator_state)
  : Prop
  := not (is_singleton_state s).

#[export] Instance is_equivocating_state_dec
  (s : equivocator_state)
  : Decision (is_equivocating_state s).message: Type
X: VLSM message
s: equivocator_state
Decision (is_equivocating_state s)
Proof.message: Type
X: VLSM message
s: equivocator_state
Decision (is_equivocating_state s)
  apply not_dec.message: Type
X: VLSM message
s: equivocator_state
Decision (is_singleton_state s)
  by apply is_singleton_state_dec.
Qed.

Attempts to obtain the state of the internal machine with index i from an equivocator_state. Fails when index i does not refer to a machine.

Definition equivocator_state_project
  (bs : equivocator_state)
  (i : nat)
  : option (state X)
  :=
  match (decide (i < equivocator_state_n bs)) with
  | left lt_in => Some (equivocator_state_s bs (of_nat_lt lt_in))
  | _ =>  None
  end.

#[local] Lemma equivocator_state_project_Some s i (Hi : i < equivocator_state_n s)
  : equivocator_state_project s i = Some (equivocator_state_s s (nat_to_fin Hi)).message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi: i < equivocator_state_n s
equivocator_state_project s i =
Some (equivocator_state_s s (nat_to_fin Hi))
Proof.message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi: i < equivocator_state_n s
equivocator_state_project s i =
Some (equivocator_state_s s (nat_to_fin Hi))
  unfold equivocator_state_project.message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi: i < equivocator_state_n s
match decide (i < equivocator_state_n s) with
| left lt_in =>
    Some (equivocator_state_s s (nat_to_fin lt_in))
| right _ => None
end = Some (equivocator_state_s s (nat_to_fin Hi))
  case_decide; [| lia].message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi, H: i < equivocator_state_n s
Some (equivocator_state_s s (nat_to_fin H)) =
Some (equivocator_state_s s (nat_to_fin Hi))
  f_equal.message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi, H: i < equivocator_state_n s
equivocator_state_s s (nat_to_fin H) =
equivocator_state_s s (nat_to_fin Hi) apply equivocator_state_eq.message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi, H: i < equivocator_state_n s
nat_to_fin H = nat_to_fin Hi
  by rewrite !fin_to_nat_to_fin.
Qed.

#[local] Lemma equivocator_state_project_None s i (Hi : ~ i < equivocator_state_n s)
  : equivocator_state_project s i = None.message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi: ¬ i < equivocator_state_n s
equivocator_state_project s i = None
Proof.message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi: ¬ i < equivocator_state_n s
equivocator_state_project s i = None
  unfold equivocator_state_project.message: Type
X: VLSM message
s: equivocator_state
i: nat
Hi: ¬ i < equivocator_state_n s
match decide (i < equivocator_state_n s) with
| left lt_in =>
    Some (equivocator_state_s s (nat_to_fin lt_in))
| right _ => None
end = None
  by case_decide; [lia |].
Qed.

Lemma equivocator_state_project_Some_rev s i si
  : equivocator_state_project s i = Some si -> i < equivocator_state_n s.message: Type
X: VLSM message
s: equivocator_state
i: nat
si: state X
equivocator_state_project s i = Some si
→ i < equivocator_state_n s
Proof.message: Type
X: VLSM message
s: equivocator_state
i: nat
si: state X
equivocator_state_project s i = Some si
→ i < equivocator_state_n s
  by unfold equivocator_state_project; case_decide.
Qed.

Lemma equivocator_state_project_None_rev s i
  : equivocator_state_project s i = None -> ~ i < equivocator_state_n s.message: Type
X: VLSM message
s: equivocator_state
i: nat
equivocator_state_project s i = None
→ ¬ i < equivocator_state_n s
Proof.message: Type
X: VLSM message
s: equivocator_state
i: nat
equivocator_state_project s i = None
→ ¬ i < equivocator_state_n s
  unfold equivocator_state_project.message: Type
X: VLSM message
s: equivocator_state
i: nat
match decide (i < equivocator_state_n s) with
| left lt_in =>
    Some (equivocator_state_s s (nat_to_fin lt_in))
| right _ => None
end = None → ¬ i < equivocator_state_n s
  by case_decide; [congruence | intro; lia].
Qed.

#[local] Ltac destruct_equivocator_state_project' es i si Hi Hpr :=
  destruct (equivocator_state_project es i) as [si |] eqn: Hpr
  ; [specialize (equivocator_state_project_Some_rev _ _ _ Hpr) as Hi
    | specialize (equivocator_state_project_None_rev _ _ Hpr) as Hi].

#[local] Ltac destruct_equivocator_state_project es i si Hi :=
  let Hpr := fresh "Hpr" in
  destruct_equivocator_state_project' es i si Hi Hpr
  ; clear Hpr.

Extensionality result, reducing the proof of the equality of two equivocator_states to the equality of their projections.

Lemma equivocator_state_project_ext es1 es2
  (Hext : forall i, equivocator_state_project es1 i = equivocator_state_project es2 i)
  : es1 = es2.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
es1 = es2
Proof.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
es1 = es2
  assert (equivocator_state_last es1 = equivocator_state_last es2).message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
equivocator_state_last es1 =
equivocator_state_last es2
message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
H: equivocator_state_last es1 =
equivocator_state_last es2
es1 = es2
  {message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
equivocator_state_last es1 =
equivocator_state_last es2 specialize (equivocator_state_last_n es1) as Hlst1.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
equivocator_state_last es1 =
equivocator_state_last es2
    specialize (equivocator_state_last_n es2) as Hlst2.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
equivocator_state_last es1 =
equivocator_state_last es2
    specialize (Hext (equivocator_state_last es1)) as Hlst_es1.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
Hlst_es1: equivocator_state_project es1
  (equivocator_state_last es1) =
equivocator_state_project es2
  (equivocator_state_last es1)
equivocator_state_last es1 =
equivocator_state_last es2
    specialize (Hext (equivocator_state_last es2)) as Hlst_es2.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
Hlst_es1: equivocator_state_project es1
  (equivocator_state_last es1) =
equivocator_state_project es2
  (equivocator_state_last es1)
Hlst_es2: equivocator_state_project es1
  (equivocator_state_last es2) =
equivocator_state_project es2
  (equivocator_state_last es2)
equivocator_state_last es1 =
equivocator_state_last es2
    clear Hext.message: Type
X: VLSM message
es1, es2: equivocator_state
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
Hlst_es1: equivocator_state_project es1
  (equivocator_state_last es1) =
equivocator_state_project es2
  (equivocator_state_last es1)
Hlst_es2: equivocator_state_project es1
  (equivocator_state_last es2) =
equivocator_state_project es2
  (equivocator_state_last es2)
equivocator_state_last es1 =
equivocator_state_last es2
    symmetry in Hlst_es1.message: Type
X: VLSM message
es1, es2: equivocator_state
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
Hlst_es1: equivocator_state_project es2
  (equivocator_state_last es1) =
equivocator_state_project es1
  (equivocator_state_last es1)
Hlst_es2: equivocator_state_project es1
  (equivocator_state_last es2) =
equivocator_state_project es2
  (equivocator_state_last es2)
equivocator_state_last es1 =
equivocator_state_last es2
    destruct_equivocator_state_project es1 (equivocator_state_last es1) lst1 Hi1; [| lia].message: Type
X: VLSM message
es1, es2: equivocator_state
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
lst1: state X
Hlst_es1: equivocator_state_project es2
  (equivocator_state_last es1) = 
Some lst1
Hlst_es2: equivocator_state_project es1
  (equivocator_state_last es2) =
equivocator_state_project es2
  (equivocator_state_last es2)
Hi1: equivocator_state_last es1 <
equivocator_state_n es1
equivocator_state_last es1 =
equivocator_state_last es2
    destruct_equivocator_state_project es2 (equivocator_state_last es2) lst2 Hi2; [| lia].message: Type
X: VLSM message
es1, es2: equivocator_state
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
lst1: state X
Hlst_es1: equivocator_state_project es2
  (equivocator_state_last es1) = 
Some lst1
lst2: state X
Hlst_es2: equivocator_state_project es1
  (equivocator_state_last es2) = 
Some lst2
Hi1: equivocator_state_last es1 <
equivocator_state_n es1
Hi2: equivocator_state_last es2 <
equivocator_state_n es2
equivocator_state_last es1 =
equivocator_state_last es2
    apply equivocator_state_project_Some_rev in Hlst_es1.message: Type
X: VLSM message
es1, es2: equivocator_state
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
lst1: state X
Hlst_es1: equivocator_state_last es1 <
equivocator_state_n es2
lst2: state X
Hlst_es2: equivocator_state_project es1
  (equivocator_state_last es2) = 
Some lst2
Hi1: equivocator_state_last es1 <
equivocator_state_n es1
Hi2: equivocator_state_last es2 <
equivocator_state_n es2
equivocator_state_last es1 =
equivocator_state_last es2
    apply equivocator_state_project_Some_rev in Hlst_es2.message: Type
X: VLSM message
es1, es2: equivocator_state
Hlst1: equivocator_state_n es1 =
S (equivocator_state_last es1)
Hlst2: equivocator_state_n es2 =
S (equivocator_state_last es2)
lst1: state X
Hlst_es1: equivocator_state_last es1 <
equivocator_state_n es2
lst2: state X
Hlst_es2: equivocator_state_last es2 <
equivocator_state_n es1
Hi1: equivocator_state_last es1 <
equivocator_state_n es1
Hi2: equivocator_state_last es2 <
equivocator_state_n es2
equivocator_state_last es1 =
equivocator_state_last es2
    lia.
  }message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
H: equivocator_state_last es1 =
equivocator_state_last es2
es1 = es2
  apply eq_sigT_uncurried.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
H: equivocator_state_last es1 =
equivocator_state_last es2
{p : projT1 es1 = projT1 es2 &
eq_rect (projT1 es1) (λ a : nat, fin (S a) → state X)
  (projT2 es1) (projT1 es2) p = projT2 es2}
  exists H.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
H: equivocator_state_last es1 =
equivocator_state_last es2
eq_rect (projT1 es1) (λ a : nat, fin (S a) → state X)
  (projT2 es1) (projT1 es2) H = projT2 es2
  extensionality x.message: Type
X: VLSM message
es1, es2: equivocator_state
Hext: ∀ i : nat,
  equivocator_state_project es1 i =
  equivocator_state_project es2 i
H: equivocator_state_last es1 =
equivocator_state_last es2
x: fin (S (projT1 es2))
eq_rect (projT1 es1) (λ a : nat, fin (S a) → state X)
  (projT2 es1) (projT1 es2) H x = projT2 es2 x
  specialize (Hext x).message: Type
X: VLSM message
es1, es2: equivocator_state
x: fin (S (projT1 es2))
Hext: equivocator_state_project es1 x =
equivocator_state_project es2 x
H: equivocator_state_last es1 =
equivocator_state_last es2
eq_rect (projT1 es1) (λ a : nat, fin (S a) → state X)
  (projT2 es1) (projT1 es2) H x = projT2 es2 x
  specialize (fin_to_nat_lt x) as Hx.message: Type
X: VLSM message
es1, es2: equivocator_state
x: fin (S (projT1 es2))
Hext: equivocator_state_project es1 x =
equivocator_state_project es2 x
H: equivocator_state_last es1 =
equivocator_state_last es2
Hx: x < S (projT1 es2)
eq_rect (projT1 es1) (λ a : nat, fin (S a) → state X)
  (projT2 es1) (projT1 es2) H x = projT2 es2 x
  rewrite (equivocator_state_project_Some es2 x Hx) in Hext.message: Type
X: VLSM message
es1, es2: equivocator_state
x: fin (S (projT1 es2))
Hx: x < S (projT1 es2)
Hext: equivocator_state_project es1 x =
Some (equivocator_state_s es2 (nat_to_fin Hx))
H: equivocator_state_last es1 =
equivocator_state_last es2
eq_rect (projT1 es1) (λ a : nat, fin (S a) → state X)
  (projT2 es1) (projT1 es2) H x = projT2 es2 x
  rewrite <- !(@nat_to_fin_to_nat _ x Hx).message: Type
X: VLSM message
es1, es2: equivocator_state
x: fin (S (projT1 es2))
Hx: x < S (projT1 es2)
Hext: equivocator_state_project es1 x =
Some (equivocator_state_s es2 (nat_to_fin Hx))
H: equivocator_state_last es1 =
equivocator_state_last es2
eq_rect (projT1 es1) (λ a : nat, fin (S a) → state X)
  (projT2 es1) (projT1 es2) H (nat_to_fin Hx) =
projT2 es2 (nat_to_fin Hx)
  destruct es1 as [x1 s1], es2 as [x2 s2]; simpl in *; subst; simpl.message: Type
X: VLSM message
x2: nat
s1, s2: fin (S x2) → state X
x: fin (S x2)
Hx: x < S x2
Hext: equivocator_state_project (existT x2 s1) x =
Some (s2 (nat_to_fin Hx))
s1 (nat_to_fin Hx) = s2 (nat_to_fin Hx)
  rewrite (equivocator_state_project_Some (existT x2 s1) x Hx) in Hext.message: Type
X: VLSM message
x2: nat
s1, s2: fin (S x2) → state X
x: fin (S x2)
Hx: x < S x2
Hext: Some
  (equivocator_state_s 
     (existT x2 s1) (nat_to_fin Hx)) =
Some (s2 (nat_to_fin Hx))
s1 (nat_to_fin Hx) = s2 (nat_to_fin Hx)
  by inversion Hext.
Qed.

The original state index is present in any equivocator state.

Lemma Hzero (s : equivocator_state) : 0 < equivocator_state_n s.message: Type
X: VLSM message
s: equivocator_state
0 < equivocator_state_n s
Proof.message: Type
X: VLSM message
s: equivocator_state
0 < equivocator_state_n s by pose proof (equivocator_state_last_n s); lia. Qed.

Definition equivocator_state_zero (es : equivocator_state) : state X :=
  equivocator_state_s es (nat_to_fin (Hzero es)).

Lemma equivocator_state_project_zero (es : equivocator_state)
  : equivocator_state_project es 0 = Some (equivocator_state_zero es).message: Type
X: VLSM message
es: equivocator_state
equivocator_state_project es 0 =
Some (equivocator_state_zero es)
Proof.message: Type
X: VLSM message
es: equivocator_state
equivocator_state_project es 0 =
Some (equivocator_state_zero es)
  unfold equivocator_state_project, equivocator_state_n.message: Type
X: VLSM message
es: equivocator_state
match decide (0 < S (projT1 es)) with
| left lt_in =>
    Some (equivocator_state_s es (nat_to_fin lt_in))
| right _ => None
end = Some (equivocator_state_zero es)
  by case_decide; [| lia].
Qed.

Definition equivocator_state_update
  (bs : equivocator_state)
  (i : nat)
  (si : state X)
  : equivocator_state
  :=
  @existT nat (fun n => Fin.t (S n) -> state X)
    (equivocator_state_last bs)
	  (fun j => if  decide (i = j) then si else equivocator_state_s bs j).

Some basic properties for equivocator_state_update.

Lemma equivocator_state_update_size bs i si
  : equivocator_state_n (equivocator_state_update bs i si) = equivocator_state_n bs.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
equivocator_state_n (equivocator_state_update bs i si) =
equivocator_state_n bs
Proof.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
equivocator_state_n (equivocator_state_update bs i si) =
equivocator_state_n bs done. Qed.

Lemma equivocator_state_update_lst bs i si
  : equivocator_state_last (equivocator_state_update bs i si) = equivocator_state_last bs.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
equivocator_state_last
  (equivocator_state_update bs i si) =
equivocator_state_last bs
Proof.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
equivocator_state_last
  (equivocator_state_update bs i si) =
equivocator_state_last bs done. Qed.

Lemma equivocator_state_update_project_eq bs i si j
  (Hj : j < equivocator_state_n bs)
  (Hij : i = j)
  : equivocator_state_project (equivocator_state_update bs i si) j = Some si.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hj: j < equivocator_state_n bs
Hij: i = j
equivocator_state_project
  (equivocator_state_update bs i si) j = Some si
Proof.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hj: j < equivocator_state_n bs
Hij: i = j
equivocator_state_project
  (equivocator_state_update bs i si) j = Some si
  pose proof (equivocator_state_update_size bs i si) as Heq.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hj: j < equivocator_state_n bs
Hij: i = j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
equivocator_state_project
  (equivocator_state_update bs i si) j = Some si
  destruct_equivocator_state_project' (equivocator_state_update bs i si) j sj Hi' Hpr ; [| lia].message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hj: j < equivocator_state_n bs
Hij: i = j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = 
Some sj
Hi': j <
equivocator_state_n
  (equivocator_state_update bs i si)
Some sj = Some si
  rewrite <- Hpr.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hj: j < equivocator_state_n bs
Hij: i = j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = 
Some sj
Hi': j <
equivocator_state_n
  (equivocator_state_update bs i si)
equivocator_state_project
  (equivocator_state_update bs i si) j = Some si
  rewrite (equivocator_state_project_Some _ _ Hi').message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hj: j < equivocator_state_n bs
Hij: i = j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = 
Some sj
Hi': j <
equivocator_state_n
  (equivocator_state_update bs i si)
Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hi')) = Some si
  f_equal; subst; clear; simpl.message: Type
X: VLSM message
bs: equivocator_state
si: state X
j: nat
Hi': j <
equivocator_state_n
  (equivocator_state_update bs j si)
(if decide (j = nat_to_fin Hi')
 then si
 else equivocator_state_s bs (nat_to_fin Hi')) = si
  rewrite decide_True; [done |].message: Type
X: VLSM message
bs: equivocator_state
si: state X
j: nat
Hi': j <
equivocator_state_n
  (equivocator_state_update bs j si)
j = nat_to_fin Hi'
  by rewrite fin_to_nat_to_fin.
Qed.

Lemma equivocator_state_update_project_neq bs i si j
  (Hij : i <> j)
  : equivocator_state_project (equivocator_state_update bs i si) j = equivocator_state_project bs j.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
equivocator_state_project
  (equivocator_state_update bs i si) j =
equivocator_state_project bs j
Proof.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
equivocator_state_project
  (equivocator_state_update bs i si) j =
equivocator_state_project bs j
  pose proof (equivocator_state_update_size bs i si) as Heq.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
equivocator_state_project
  (equivocator_state_update bs i si) j =
equivocator_state_project bs j
  destruct_equivocator_state_project' (equivocator_state_update bs i si) j sj Hj Hpr.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = 
Some sj
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Some sj = equivocator_state_project bs j
message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = None
Hj: ¬ j <
  equivocator_state_n
    (equivocator_state_update bs i si)
None = equivocator_state_project bs j
  -message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = 
Some sj
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Some sj = equivocator_state_project bs j assert (Hj' := Hj).message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = 
Some sj
Hj, Hj': j <
equivocator_state_n
  (equivocator_state_update bs i si)
Some sj = equivocator_state_project bs j
    rewrite Heq in Hj'.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = 
Some sj
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hj': j < equivocator_state_n bs
Some sj = equivocator_state_project bs j
    rewrite (equivocator_state_project_Some _ _ Hj) in Hpr.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
Some sj = equivocator_state_project bs j
    rewrite (equivocator_state_project_Some _ _ Hj').message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
Some sj =
Some (equivocator_state_s bs (nat_to_fin Hj'))
    f_equal.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
sj = equivocator_state_s bs (nat_to_fin Hj')
    inversion Hpr.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
H0: (if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
sj
(if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
equivocator_state_s bs (nat_to_fin Hj')
    rewrite decide_False.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
H0: (if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
sj
equivocator_state_s bs (nat_to_fin Hj) =
equivocator_state_s bs (nat_to_fin Hj')
message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
H0: (if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
sj
i ≠ nat_to_fin Hj
    +message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
H0: (if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
sj
equivocator_state_s bs (nat_to_fin Hj) =
equivocator_state_s bs (nat_to_fin Hj') apply equivocator_state_eq.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
H0: (if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
sj
nat_to_fin Hj = nat_to_fin Hj'
      by rewrite !fin_to_nat_to_fin.
    +message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
H0: (if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
sj
i ≠ nat_to_fin Hj intro Hcontra.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
sj: state X
Hj: j <
equivocator_state_n
  (equivocator_state_update bs i si)
Hpr: Some
  (equivocator_state_s
     (equivocator_state_update bs i si)
     (nat_to_fin Hj)) = 
Some sj
Hj': j < equivocator_state_n bs
H0: (if decide (i = nat_to_fin Hj)
 then si
 else equivocator_state_s bs (nat_to_fin Hj)) =
sj
Hcontra: i = nat_to_fin Hj
False
      by rewrite !fin_to_nat_to_fin in Hcontra; congruence.
  -message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = None
Hj: ¬ j <
  equivocator_state_n
    (equivocator_state_update bs i si)
None = equivocator_state_project bs j rewrite Heq in Hj.message: Type
X: VLSM message
bs: equivocator_state
i: nat
si: state X
j: nat
Hij: i ≠ j
Heq: equivocator_state_n
  (equivocator_state_update bs i si) =
equivocator_state_n bs
Hpr: equivocator_state_project
  (equivocator_state_update bs i si) j = None
Hj: ¬ j < equivocator_state_n bs
None = equivocator_state_project bs j
    by rewrite (equivocator_state_project_None _ _ Hj).
Qed.

#[local] Ltac destruct_equivocator_state_update_project' es i s j Hj Hij Hpr :=
  let Hsize := fresh "Hsize" in
  pose proof (equivocator_state_update_size es i s) as Hsize
  ; destruct (decide (j < equivocator_state_n es)) as [Hj | Hj]
  ; [destruct (decide (i = j)) as [Hij | Hij]
    ; [specialize (equivocator_state_update_project_eq es i s j Hj Hij) as Hpr
      | specialize (equivocator_state_update_project_neq es i s j Hij) as Hpr]
    | specialize (equivocator_state_project_None (equivocator_state_update es i s) j Hj) as Hpr]
  ; rewrite Hpr in *
  ; clear Hsize.

#[local] Ltac destruct_equivocator_state_update_project es i s j Hj Hij :=
  let Hpr := fresh "Hpr" in
  destruct_equivocator_state_update_project' es i s j Hj Hij Hpr
  ; clear Hpr.

Extends an equivocator_state with a new state of the original machine.

Program Definition equivocator_state_extend
  (bs : equivocator_state)
  (s : state X)
  : equivocator_state
  :=
  existT (S (equivocator_state_last bs))
    (fun j => if decide (S (equivocator_state_last bs) = j)
              then s else equivocator_state_s bs (@of_nat_lt j (S (equivocator_state_last bs)) _)).
Next Obligation.message: Type
X: VLSM message
∀ bs : equivocator_state,
  state X
  → ∀ j : fin (S (S (equivocator_state_last bs))),
      S (equivocator_state_last bs) ≠ j
      → j < S (equivocator_state_last bs)
Proof.message: Type
X: VLSM message
∀ bs : equivocator_state,
  state X
  → ∀ j : fin (S (S (equivocator_state_last bs))),
      S (equivocator_state_last bs) ≠ j
      → j < S (equivocator_state_last bs)
  by intros; specialize (fin_to_nat_lt j);  lia.
Qed.

Lemma equivocator_state_extend_size bs s
  : equivocator_state_n (equivocator_state_extend bs s) = S (equivocator_state_n bs).message: Type
X: VLSM message
bs: equivocator_state
s: state X
equivocator_state_n (equivocator_state_extend bs s) =
S (equivocator_state_n bs)
Proof.message: Type
X: VLSM message
bs: equivocator_state
s: state X
equivocator_state_n (equivocator_state_extend bs s) =
S (equivocator_state_n bs) done. Qed.

Lemma equivocator_state_extend_lst bs s
  : equivocator_state_last (equivocator_state_extend bs s) = equivocator_state_n bs.message: Type
X: VLSM message
bs: equivocator_state
s: state X
equivocator_state_last (equivocator_state_extend bs s) =
equivocator_state_n bs
Proof.message: Type
X: VLSM message
bs: equivocator_state
s: state X
equivocator_state_last (equivocator_state_extend bs s) =
equivocator_state_n bs done. Qed.

Lemma equivocator_state_extend_project_1 es s i (Hi : i < equivocator_state_n es)
  : equivocator_state_project (equivocator_state_extend es s) i = equivocator_state_project es i.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
equivocator_state_project
  (equivocator_state_extend es s) i =
equivocator_state_project es i
Proof.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
equivocator_state_project
  (equivocator_state_extend es s) i =
equivocator_state_project es i
  rewrite (equivocator_state_project_Some _ _ Hi).message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
equivocator_state_project
  (equivocator_state_extend es s) i =
Some (equivocator_state_s es (nat_to_fin Hi))
  specialize (equivocator_state_extend_size es s) as Hsize.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
equivocator_state_project
  (equivocator_state_extend es s) i =
Some (equivocator_state_s es (nat_to_fin Hi))
  assert (Hi' : i < equivocator_state_n (equivocator_state_extend es s))
    by lia.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
equivocator_state_project
  (equivocator_state_extend es s) i =
Some (equivocator_state_s es (nat_to_fin Hi))
  rewrite (equivocator_state_project_Some _ _ Hi').message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Some
  (equivocator_state_s (equivocator_state_extend es s)
     (nat_to_fin Hi')) =
Some (equivocator_state_s es (nat_to_fin Hi))
  f_equal.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
equivocator_state_s (equivocator_state_extend es s)
  (nat_to_fin Hi') =
equivocator_state_s es (nat_to_fin Hi)
  cbn.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
match
  decide
    (S (equivocator_state_last es) = nat_to_fin Hi')
with
| left _ => s
| right x =>
    equivocator_state_s es
      (nat_to_fin
         (equivocator_state_extend_obligation_1 es
            (nat_to_fin Hi') x))
end = equivocator_state_s es (nat_to_fin Hi)
  specialize (equivocator_state_last_n es) as Hes_size.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Hes_size: equivocator_state_n es =
S (equivocator_state_last es)
match
  decide
    (S (equivocator_state_last es) = nat_to_fin Hi')
with
| left _ => s
| right x =>
    equivocator_state_s es
      (nat_to_fin
         (equivocator_state_extend_obligation_1 es
            (nat_to_fin Hi') x))
end = equivocator_state_s es (nat_to_fin Hi)
  destruct (decide _).message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Hes_size: equivocator_state_n es =
S (equivocator_state_last es)
e: S (equivocator_state_last es) = nat_to_fin Hi'
s = equivocator_state_s es (nat_to_fin Hi)
message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Hes_size: equivocator_state_n es =
S (equivocator_state_last es)
n: S (equivocator_state_last es) ≠ nat_to_fin Hi'
equivocator_state_s es
  (nat_to_fin
     (equivocator_state_extend_obligation_1 es
        (nat_to_fin Hi') n)) =
equivocator_state_s es (nat_to_fin Hi)
  -message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Hes_size: equivocator_state_n es =
S (equivocator_state_last es)
e: S (equivocator_state_last es) = nat_to_fin Hi'
s = equivocator_state_s es (nat_to_fin Hi) by rewrite fin_to_nat_to_fin in e; lia.
  -message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Hes_size: equivocator_state_n es =
S (equivocator_state_last es)
n: S (equivocator_state_last es) ≠ nat_to_fin Hi'
equivocator_state_s es
  (nat_to_fin
     (equivocator_state_extend_obligation_1 es
        (nat_to_fin Hi') n)) =
equivocator_state_s es (nat_to_fin Hi) apply equivocator_state_eq.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Hes_size: equivocator_state_n es =
S (equivocator_state_last es)
n: S (equivocator_state_last es) ≠ nat_to_fin Hi'
nat_to_fin
  (equivocator_state_extend_obligation_1 es
     (nat_to_fin Hi') n) = nat_to_fin Hi
    by rewrite !fin_to_nat_to_fin.
Qed.

Lemma equivocator_state_extend_project_2 es s i (Hi : i = equivocator_state_n es)
  : equivocator_state_project (equivocator_state_extend es s) i = Some s.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
equivocator_state_project
  (equivocator_state_extend es s) i = Some s
Proof.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
equivocator_state_project
  (equivocator_state_extend es s) i = Some s
  specialize (equivocator_state_extend_size es s) as Hsize.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
equivocator_state_project
  (equivocator_state_extend es s) i = Some s
  assert (Hi' : i < equivocator_state_n (equivocator_state_extend es s))
    by lia.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
equivocator_state_project
  (equivocator_state_extend es s) i = Some s
  rewrite (equivocator_state_project_Some _ _ Hi').message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
Some
  (equivocator_state_s (equivocator_state_extend es s)
     (nat_to_fin Hi')) = Some s
  f_equal.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
equivocator_state_s (equivocator_state_extend es s)
  (nat_to_fin Hi') = s
  cbn.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
match
  decide
    (S (equivocator_state_last es) = nat_to_fin Hi')
with
| left _ => s
| right x =>
    equivocator_state_s es
      (nat_to_fin
         (equivocator_state_extend_obligation_1 es
            (nat_to_fin Hi') x))
end = s
  destruct (decide _); [done |].message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
n: S (equivocator_state_last es) ≠ nat_to_fin Hi'
equivocator_state_s es
  (nat_to_fin
     (equivocator_state_extend_obligation_1 es
        (nat_to_fin Hi') n)) = s
  elim n.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
n: S (equivocator_state_last es) ≠ nat_to_fin Hi'
S (equivocator_state_last es) = nat_to_fin Hi'
  rewrite fin_to_nat_to_fin.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: i = equivocator_state_n es
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
Hi': i <
equivocator_state_n
  (equivocator_state_extend es s)
n: S (equivocator_state_last es) ≠ nat_to_fin Hi'
S (equivocator_state_last es) = i
  by specialize (equivocator_state_last_n es) as Hes_size; lia.
Qed.

Lemma equivocator_state_extend_project_3 es s i (Hi : equivocator_state_n es < i)
  : equivocator_state_project (equivocator_state_extend es s) i = None.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: equivocator_state_n es < i
equivocator_state_project
  (equivocator_state_extend es s) i = None
Proof.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: equivocator_state_n es < i
equivocator_state_project
  (equivocator_state_extend es s) i = None
  remember (equivocator_state_extend _ _) as ex.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: equivocator_state_n es < i
ex: equivocator_state
Heqex: ex = equivocator_state_extend es s
equivocator_state_project ex i = None
  specialize (equivocator_state_extend_size es s) as Hsize.message: Type
X: VLSM message
es: equivocator_state
s: state X
i: nat
Hi: equivocator_state_n es < i
ex: equivocator_state
Heqex: ex = equivocator_state_extend es s
Hsize: equivocator_state_n
  (equivocator_state_extend es s) =
S (equivocator_state_n es)
equivocator_state_project ex i = None
  by destruct_equivocator_state_project ex i si Hi''; subst; [lia |].
Qed.

#[local] Ltac destruct_equivocator_state_extend_project' es s i Hi Hpr :=
  let Hni := fresh "Hni" in
  let Hni' := fresh "Hni" in
  destruct (decide (i < equivocator_state_n es)) as [Hi | Hni]
  ; [| destruct (decide (i = equivocator_state_n es)) as [Hi | Hni']]
  ; [| | assert (Hi : equivocator_state_n es < i) by lia]
  ; [specialize (equivocator_state_extend_project_1 es s i Hi) as Hpr
    | specialize (equivocator_state_extend_project_2 es s i Hi) as Hpr
    | specialize (equivocator_state_extend_project_3 es s i Hi) as Hpr]
  ; rewrite Hpr in *.

#[local] Ltac destruct_equivocator_state_extend_project es s i Hi :=
  let Hpr := fresh "Hpr" in
  destruct_equivocator_state_extend_project' es s i Hi Hpr
  ; clear Hpr.

Program Definition equivocator_state_append
  (es1 es2 : equivocator_state)
  : equivocator_state
  :=
  existT (equivocator_state_n es1 + equivocator_state_last es2)
    (fun j =>
      let (nj, Hnj) := to_nat j in
      match decide (nj < equivocator_state_n es1) with
      | left lt_in => equivocator_state_s es1 (of_nat_lt lt_in)
      | right ge_in =>
        let (k, Hk) := not_lt_plus_dec ge_in in
        equivocator_state_s es2 (@of_nat_lt k (equivocator_state_n es2) _)
      end).
Next Obligation.message: Type
X: VLSM message
∀ es1 es2 : equivocator_state,
  fin
    (S
       (equivocator_state_n es1 +
        equivocator_state_last es2))
  → ∀ nj : nat,
      nj <
      S
        (equivocator_state_n es1 +
         equivocator_state_last es2)
      → ∀ (filtered_var :=
           decide (nj < equivocator_state_n es1)) 
          (ge_in : ¬ nj < equivocator_state_n es1),
          right ge_in = filtered_var
          → ∀ k : nat,
              k + equivocator_state_n es1 = nj
              → k < equivocator_state_n es2
Proof.message: Type
X: VLSM message
∀ es1 es2 : equivocator_state,
  fin
    (S
       (equivocator_state_n es1 +
        equivocator_state_last es2))
  → ∀ nj : nat,
      nj <
      S
        (equivocator_state_n es1 +
         equivocator_state_last es2)
      → ∀ (filtered_var :=
           decide (nj < equivocator_state_n es1)) 
          (ge_in : ¬ nj < equivocator_state_n es1),
          right ge_in = filtered_var
          → ∀ k : nat,
              k + equivocator_state_n es1 = nj
              → k < equivocator_state_n es2
  by intros; specialize (equivocator_state_last_n es2) as Hlst_es2; lia.
Qed.

Lemma equivocator_state_append_size es1 es2
  : equivocator_state_n (equivocator_state_append es1 es2) =
    equivocator_state_n es1 + equivocator_state_n es2.message: Type
X: VLSM message
es1, es2: equivocator_state
equivocator_state_n (equivocator_state_append es1 es2) =
equivocator_state_n es1 + equivocator_state_n es2
Proof.message: Type
X: VLSM message
es1, es2: equivocator_state
equivocator_state_n (equivocator_state_append es1 es2) =
equivocator_state_n es1 + equivocator_state_n es2
  by destruct es1, es2; unfold equivocator_state_n; cbn; lia.
Qed.

Lemma equivocator_state_append_lst es1 es2
  : equivocator_state_last (equivocator_state_append es1 es2) =
    equivocator_state_last es2 + equivocator_state_n es1.message: Type
X: VLSM message
es1, es2: equivocator_state
equivocator_state_last
  (equivocator_state_append es1 es2) =
equivocator_state_last es2 + equivocator_state_n es1
Proof.message: Type
X: VLSM message
es1, es2: equivocator_state
equivocator_state_last
  (equivocator_state_append es1 es2) =
equivocator_state_last es2 + equivocator_state_n es1
  by destruct es1, es2; unfold equivocator_state_n; cbn; lia.
Qed.

Lemma equivocator_state_append_project_1 s s' i (Hi : i < equivocator_state_n s)
  : equivocator_state_project (equivocator_state_append s s') i = equivocator_state_project s i.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
equivocator_state_project
  (equivocator_state_append s s') i =
equivocator_state_project s i
Proof.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
equivocator_state_project
  (equivocator_state_append s s') i =
equivocator_state_project s i
  specialize (equivocator_state_projection_irrel s) as Hpi.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s) 
  (j : nat) (lj : j < equivocator_state_n s),
  i = j
  → equivocator_state_s s (nat_to_fin li) =
    equivocator_state_s s (nat_to_fin lj)
equivocator_state_project
  (equivocator_state_append s s') i =
equivocator_state_project s i
  rewrite (equivocator_state_project_Some _ _ Hi).message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s) 
  (j : nat) (lj : j < equivocator_state_n s),
  i = j
  → equivocator_state_s s (nat_to_fin li) =
    equivocator_state_s s (nat_to_fin lj)
equivocator_state_project
  (equivocator_state_append s s') i =
Some (equivocator_state_s s (nat_to_fin Hi))
  specialize (equivocator_state_append_size s s') as Hsize.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s) 
  (j : nat) (lj : j < equivocator_state_n s),
  i = j
  → equivocator_state_s s (nat_to_fin li) =
    equivocator_state_s s (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append s s') =
equivocator_state_n s + equivocator_state_n s'
equivocator_state_project
  (equivocator_state_append s s') i =
Some (equivocator_state_s s (nat_to_fin Hi))
  assert (Hi' : i < equivocator_state_n (equivocator_state_append s s')) by lia.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s) 
  (j : nat) (lj : j < equivocator_state_n s),
  i = j
  → equivocator_state_s s (nat_to_fin li) =
    equivocator_state_s s (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append s s') =
equivocator_state_n s + equivocator_state_n s'
Hi': i <
equivocator_state_n
  (equivocator_state_append s s')
equivocator_state_project
  (equivocator_state_append s s') i =
Some (equivocator_state_s s (nat_to_fin Hi))
  rewrite (equivocator_state_project_Some _ _ Hi').message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s) 
  (j : nat) (lj : j < equivocator_state_n s),
  i = j
  → equivocator_state_s s (nat_to_fin li) =
    equivocator_state_s s (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append s s') =
equivocator_state_n s + equivocator_state_n s'
Hi': i <
equivocator_state_n
  (equivocator_state_append s s')
Some
  (equivocator_state_s (equivocator_state_append s s')
     (nat_to_fin Hi')) =
Some (equivocator_state_s s (nat_to_fin Hi))
  f_equal.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: i < equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s) 
  (j : nat) (lj : j < equivocator_state_n s),
  i = j
  → equivocator_state_s s (nat_to_fin li) =
    equivocator_state_s s (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append s s') =
equivocator_state_n s + equivocator_state_n s'
Hi': i <
equivocator_state_n
  (equivocator_state_append s s')
equivocator_state_s (equivocator_state_append s s')
  (nat_to_fin Hi') =
equivocator_state_s s (nat_to_fin Hi)
  destruct s as (n1, bs1).message: Type
X: VLSM message
n1: nat
bs1: fin (S n1) → state X
s': equivocator_state
i: nat
Hi: i < equivocator_state_n (existT n1 bs1)
Hpi: ∀ (i : nat) (li : i <
                  equivocator_state_n
                    (existT n1 bs1)) 
  (j : nat) (lj : j <
                  equivocator_state_n
                    (existT n1 bs1)),
  i = j
  → equivocator_state_s 
      (existT n1 bs1) (nat_to_fin li) =
    equivocator_state_s 
      (existT n1 bs1) (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append (existT n1 bs1) s') =
equivocator_state_n (existT n1 bs1) +
equivocator_state_n s'
Hi': i <
equivocator_state_n
  (equivocator_state_append (existT n1 bs1) s')
equivocator_state_s
  (equivocator_state_append (existT n1 bs1) s')
  (nat_to_fin Hi') =
equivocator_state_s (existT n1 bs1) (nat_to_fin Hi)
  destruct s' as (n2, bs2).message: Type
X: VLSM message
n1: nat
bs1: fin (S n1) → state X
n2: nat
bs2: fin (S n2) → state X
i: nat
Hi: i < equivocator_state_n (existT n1 bs1)
Hpi: ∀ (i : nat) (li : i <
                  equivocator_state_n
                    (existT n1 bs1)) 
  (j : nat) (lj : j <
                  equivocator_state_n
                    (existT n1 bs1)),
  i = j
  → equivocator_state_s 
      (existT n1 bs1) (nat_to_fin li) =
    equivocator_state_s 
      (existT n1 bs1) (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append 
     (existT n1 bs1) (existT n2 bs2)) =
equivocator_state_n (existT n1 bs1) +
equivocator_state_n (existT n2 bs2)
Hi': i <
equivocator_state_n
  (equivocator_state_append 
     (existT n1 bs1) (existT n2 bs2))
equivocator_state_s
  (equivocator_state_append (existT n1 bs1)
     (existT n2 bs2)) (nat_to_fin Hi') =
equivocator_state_s (existT n1 bs1) (nat_to_fin Hi)
  unfold equivocator_state_n in *.message: Type
X: VLSM message
n1: nat
bs1: fin (S n1) → state X
n2: nat
bs2: fin (S n2) → state X
i: nat
Hi: i < S (projT1 (existT n1 bs1))
Hpi: ∀ (i : nat) (li : i < S (projT1 (existT n1 bs1))) 
  (j : nat) (lj : j < S (projT1 (existT n1 bs1))),
  i = j
  → equivocator_state_s 
      (existT n1 bs1) (nat_to_fin li) =
    equivocator_state_s 
      (existT n1 bs1) (nat_to_fin lj)
Hsize: S
  (projT1
     (equivocator_state_append 
        (existT n1 bs1) 
        (existT n2 bs2))) =
S (projT1 (existT n1 bs1)) +
S (projT1 (existT n2 bs2))
Hi': i <
S
  (projT1
     (equivocator_state_append 
        (existT n1 bs1) 
        (existT n2 bs2)))
equivocator_state_s
  (equivocator_state_append (existT n1 bs1)
     (existT n2 bs2)) (nat_to_fin Hi') =
equivocator_state_s (existT n1 bs1) (nat_to_fin Hi)
  simpl in *.message: Type
X: VLSM message
n1: nat
bs1: fin (S n1) → state X
n2: nat
bs2: fin (S n2) → state X
i: nat
Hi: i < S n1
Hpi: ∀ (i : nat) (li : i < S n1) 
  (j : nat) (lj : j < S n1),
  i = j
  → bs1 (nat_to_fin li) = bs1 (nat_to_fin lj)
Hsize: S (S (n1 + n2)) = S (n1 + S n2)
Hi': i < S (S (n1 + n2))
(let (nj, Hnj) := to_nat (nat_to_fin Hi') in
 match
   decide (nj < equivocator_state_n (existT n1 bs1))
   as anonymous'
   return
     (anonymous' =
      decide
        (nj < equivocator_state_n (existT n1 bs1))
      → state X)
 with
 | left lt_in =>
     λ _ : left lt_in =
           decide
             (nj < equivocator_state_n (existT n1 bs1)),
       bs1 (nat_to_fin lt_in)
 | right ge_in =>
     λ _ : right ge_in =
           decide
             (nj < equivocator_state_n (existT n1 bs1)),
       bs2
         (nat_to_fin
            (equivocator_state_append_obligation_1
               (existT n1 bs1) (existT n2 bs2) nj Hnj
               ge_in
               (nj -
                equivocator_state_n (existT n1 bs1))
               (Preamble.not_lt_plus_dec_obligation_1
                  (equivocator_state_n (existT n1 bs1))
                  nj ge_in)))
 end eq_refl) = bs1 (nat_to_fin Hi)
  rewrite to_nat_of_nat.message: Type
X: VLSM message
n1: nat
bs1: fin (S n1) → state X
n2: nat
bs2: fin (S n2) → state X
i: nat
Hi: i < S n1
Hpi: ∀ (i : nat) (li : i < S n1) 
  (j : nat) (lj : j < S n1),
  i = j
  → bs1 (nat_to_fin li) = bs1 (nat_to_fin lj)
Hsize: S (S (n1 + n2)) = S (n1 + S n2)
Hi': i < S (S (n1 + n2))
match
  decide (i < equivocator_state_n (existT n1 bs1)) as
  anonymous'
  return
    (anonymous' =
     decide (i < equivocator_state_n (existT n1 bs1))
     → state X)
with
| left lt_in =>
    λ _ : left lt_in =
          decide
            (i < equivocator_state_n (existT n1 bs1)),
      bs1 (nat_to_fin lt_in)
| right ge_in =>
    λ _ : right ge_in =
          decide
            (i < equivocator_state_n (existT n1 bs1)),
      bs2
        (nat_to_fin
           (equivocator_state_append_obligation_1
              (existT n1 bs1) (existT n2 bs2) i Hi'
              ge_in
              (i - equivocator_state_n (existT n1 bs1))
              (Preamble.not_lt_plus_dec_obligation_1
                 (equivocator_state_n (existT n1 bs1))
                 i ge_in)))
end eq_refl = bs1 (nat_to_fin Hi)
  unfold equivocator_state_n.message: Type
X: VLSM message
n1: nat
bs1: fin (S n1) → state X
n2: nat
bs2: fin (S n2) → state X
i: nat
Hi: i < S n1
Hpi: ∀ (i : nat) (li : i < S n1) 
  (j : nat) (lj : j < S n1),
  i = j
  → bs1 (nat_to_fin li) = bs1 (nat_to_fin lj)
Hsize: S (S (n1 + n2)) = S (n1 + S n2)
Hi': i < S (S (n1 + n2))
match
  decide (i < S (projT1 (existT n1 bs1))) as
  anonymous'
  return
    (anonymous' =
     decide (i < S (projT1 (existT n1 bs1))) → state X)
with
| left lt_in =>
    λ _ : left lt_in =
          decide (i < S (projT1 (existT n1 bs1))),
      bs1 (nat_to_fin lt_in)
| right ge_in =>
    λ _ : right ge_in =
          decide (i < S (projT1 (existT n1 bs1))),
      bs2
        (nat_to_fin
           (equivocator_state_append_obligation_1
              (existT n1 bs1) (existT n2 bs2) i Hi'
              ge_in (i - S (projT1 (existT n1 bs1)))
              (Preamble.not_lt_plus_dec_obligation_1
                 (S (projT1 (existT n1 bs1))) i ge_in)))
end eq_refl = bs1 (nat_to_fin Hi) simpl.message: Type
X: VLSM message
n1: nat
bs1: fin (S n1) → state X
n2: nat
bs2: fin (S n2) → state X
i: nat
Hi: i < S n1
Hpi: ∀ (i : nat) (li : i < S n1) 
  (j : nat) (lj : j < S n1),
  i = j
  → bs1 (nat_to_fin li) = bs1 (nat_to_fin lj)
Hsize: S (S (n1 + n2)) = S (n1 + S n2)
Hi': i < S (S (n1 + n2))
match
  decide (i < S n1) as anonymous'
  return (anonymous' = decide (i < S n1) → state X)
with
| left lt_in =>
    λ _ : left lt_in = decide (i < S n1),
      bs1 (nat_to_fin lt_in)
| right ge_in =>
    λ _ : right ge_in = decide (i < S n1),
      bs2
        (nat_to_fin
           (equivocator_state_append_obligation_1
              (existT n1 bs1) (existT n2 bs2) i Hi'
              ge_in (i - S n1)
              (Preamble.not_lt_plus_dec_obligation_1
                 (S n1) i ge_in)))
end eq_refl = bs1 (nat_to_fin Hi)
  by case_decide; [apply Hpi | lia].
Qed.

Lemma equivocator_state_append_project_2 s s' i k (Hi : i = k + equivocator_state_n s)
  : equivocator_state_project (equivocator_state_append s s') i = equivocator_state_project s' k.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
equivocator_state_project
  (equivocator_state_append s s') i =
equivocator_state_project s' k
Proof.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
equivocator_state_project
  (equivocator_state_append s s') i =
equivocator_state_project s' k
  specialize (equivocator_state_projection_irrel s') as Hpi.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
equivocator_state_project
  (equivocator_state_append s s') i =
equivocator_state_project s' k
  specialize (equivocator_state_append_size s s') as Hsize.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append s s') =
equivocator_state_n s + equivocator_state_n s'
equivocator_state_project
  (equivocator_state_append s s') i =
equivocator_state_project s' k
  remember (equivocator_state_append s s') as append.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
append: equivocator_state
Heqappend: append = equivocator_state_append s s'
Hsize: equivocator_state_n append =
equivocator_state_n s + equivocator_state_n s'
equivocator_state_project append i =
equivocator_state_project s' k
  destruct_equivocator_state_project' s' k s'k Hk Hprs'
  ; destruct_equivocator_state_project' append i appendi Hi' Hprapp
  ; [| lia | lia | done].message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
append: equivocator_state
Heqappend: append = equivocator_state_append s s'
Hsize: equivocator_state_n append =
equivocator_state_n s + equivocator_state_n s'
s'k: state X
Hprs': equivocator_state_project s' k = Some s'k
Hk: k < equivocator_state_n s'
appendi: state X
Hprapp: equivocator_state_project append i =
Some appendi
Hi': i < equivocator_state_n append
Some appendi = Some s'k
  f_equal.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
append: equivocator_state
Heqappend: append = equivocator_state_append s s'
Hsize: equivocator_state_n append =
equivocator_state_n s + equivocator_state_n s'
s'k: state X
Hprs': equivocator_state_project s' k = Some s'k
Hk: k < equivocator_state_n s'
appendi: state X
Hprapp: equivocator_state_project append i =
Some appendi
Hi': i < equivocator_state_n append
appendi = s'k
  rewrite (equivocator_state_project_Some _ _ Hi') in Hprapp.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
append: equivocator_state
Heqappend: append = equivocator_state_append s s'
Hsize: equivocator_state_n append =
equivocator_state_n s + equivocator_state_n s'
s'k: state X
Hprs': equivocator_state_project s' k = Some s'k
Hk: k < equivocator_state_n s'
appendi: state X
Hi': i < equivocator_state_n append
Hprapp: Some
  (equivocator_state_s append
     (nat_to_fin Hi')) = 
Some appendi
appendi = s'k
  inversion_clear Hprapp.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
append: equivocator_state
Heqappend: append = equivocator_state_append s s'
Hsize: equivocator_state_n append =
equivocator_state_n s + equivocator_state_n s'
s'k: state X
Hprs': equivocator_state_project s' k = Some s'k
Hk: k < equivocator_state_n s'
appendi: state X
Hi': i < equivocator_state_n append
equivocator_state_s append (nat_to_fin Hi') = s'k
  rewrite (equivocator_state_project_Some _ _ Hk) in Hprs'.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
append: equivocator_state
Heqappend: append = equivocator_state_append s s'
Hsize: equivocator_state_n append =
equivocator_state_n s + equivocator_state_n s'
s'k: state X
Hk: k < equivocator_state_n s'
Hprs': Some (equivocator_state_s s' (nat_to_fin Hk)) =
Some s'k
appendi: state X
Hi': i < equivocator_state_n append
equivocator_state_s append (nat_to_fin Hi') = s'k
  inversion_clear Hprs'.message: Type
X: VLSM message
s, s': equivocator_state
i, k: nat
Hi: i = k + equivocator_state_n s
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
append: equivocator_state
Heqappend: append = equivocator_state_append s s'
Hsize: equivocator_state_n append =
equivocator_state_n s + equivocator_state_n s'
s'k: state X
Hk: k < equivocator_state_n s'
appendi: state X
Hi': i < equivocator_state_n append
equivocator_state_s append (nat_to_fin Hi') =
equivocator_state_s s' (nat_to_fin Hk)
  subst.message: Type
X: VLSM message
s, s': equivocator_state
k: nat
Hpi: ∀ (i : nat) (li : i < equivocator_state_n s') 
  (j : nat) (lj : j < equivocator_state_n s'),
  i = j
  → equivocator_state_s s' (nat_to_fin li) =
    equivocator_state_s s' (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append s s') =
equivocator_state_n s + equivocator_state_n s'
s'k: state X
Hk: k < equivocator_state_n s'
appendi: state X
Hi': k + equivocator_state_n s <
equivocator_state_n
  (equivocator_state_append s s')
equivocator_state_s (equivocator_state_append s s')
  (nat_to_fin Hi') =
equivocator_state_s s' (nat_to_fin Hk)
  destruct s, s'.message: Type
X: VLSM message
x: nat
s: fin (S x) → state X
x0: nat
s0: fin (S x0) → state X
k: nat
Hpi: ∀ (i : nat) (li : i <
                  equivocator_state_n
                    (existT x0 s0)) 
  (j : nat) (lj : j <
                  equivocator_state_n
                    (existT x0 s0)),
  i = j
  → equivocator_state_s 
      (existT x0 s0) (nat_to_fin li) =
    equivocator_state_s 
      (existT x0 s0) (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append 
     (existT x s) (existT x0 s0)) =
equivocator_state_n (existT x s) +
equivocator_state_n (existT x0 s0)
s'k: state X
Hk: k < equivocator_state_n (existT x0 s0)
appendi: state X
Hi': k + equivocator_state_n (existT x s) <
equivocator_state_n
  (equivocator_state_append 
     (existT x s) (existT x0 s0))
equivocator_state_s
  (equivocator_state_append (existT x s)
     (existT x0 s0)) (nat_to_fin Hi') =
equivocator_state_s (existT x0 s0) (nat_to_fin Hk) simpl in *.message: Type
X: VLSM message
x: nat
s: fin (S x) → state X
x0: nat
s0: fin (S x0) → state X
k: nat
Hpi: ∀ (i : nat) (li : i <
                  equivocator_state_n
                    (existT x0 s0)) 
  (j : nat) (lj : j <
                  equivocator_state_n
                    (existT x0 s0)),
  i = j
  → s0 (nat_to_fin li) = s0 (nat_to_fin lj)
Hsize: equivocator_state_n
  (equivocator_state_append 
     (existT x s) (existT x0 s0)) =
S (x + equivocator_state_n (existT x0 s0))
s'k: state X
Hk: k < equivocator_state_n (existT x0 s0)
appendi: state X
Hi': k + equivocator_state_n (existT x s) <
equivocator_state_n
  (equivocator_state_append 
     (existT x s) (existT x0 s0))
(let (nj, Hnj) := to_nat (nat_to_fin Hi') in
 match
   decide (nj < equivocator_state_n (existT x s)) as
   anonymous'
   return
     (anonymous' =
      decide (nj < equivocator_state_n (existT x s))
      → state X)
 with
 | left lt_in =>
     λ _ : left lt_in =
           decide
             (nj < equivocator_state_n (existT x s)),
       s (nat_to_fin lt_in)
 | right ge_in =>
     λ _ : right ge_in =
           decide
             (nj < equivocator_state_n (existT x s)),
       s0
         (nat_to_fin
            (equivocator_state_append_obligation_1
               (existT x s) (existT x0 s0) nj Hnj
               ge_in
               (nj - equivocator_state_n (existT x s))
               (Preamble.not_lt_plus_dec_obligation_1
                  (equivocator_state_n (existT x s))
                  nj ge_in)))
 end eq_refl) = s0 (nat_to_fin Hk) unfold equivocator_state_n in *.message: Type
X: VLSM message
x: nat
s: fin (S x) → state X
x0: nat
s0: fin (S x0) → state X
k: nat
Hpi: ∀ (i : nat) (li : i < S (projT1 (existT x0 s0))) 
  (j : nat) (lj : j < S (projT1 (existT x0 s0))),
  i = j
  → s0 (nat_to_fin li) = s0 (nat_to_fin lj)
Hsize: S
  (projT1
     (equivocator_state_append 
        (existT x s) (existT x0 s0))) =
S (x + S (projT1 (existT x0 s0)))
s'k: state X
Hk: k < S (projT1 (existT x0 s0))
appendi: state X
Hi': k + S (projT1 (existT x s)) <
S
  (projT1
     (equivocator_state_append 
        (existT x s) (existT x0 s0)))
(let (nj, Hnj) := to_nat (nat_to_fin Hi') in
 match
   decide (nj < S (projT1 (existT x s))) as anonymous'
   return
     (anonymous' =
      decide (nj < S (projT1 (existT x s))) → state X)
 with
 | left lt_in =>
     λ _ : left lt_in =
           decide (nj < S (projT1 (existT x s))),
       s (nat_to_fin lt_in)
 | right ge_in =>
     λ _ : right ge_in =
           decide (nj < S (projT1 (existT x s))),
       s0
         (nat_to_fin
            (equivocator_state_append_obligation_1
               (existT x s) (existT x0 s0) nj Hnj
               ge_in (nj - S (projT1 (existT x s)))
               (Preamble.not_lt_plus_dec_obligation_1
                  (S (projT1 (existT x s))) nj ge_in)))
 end eq_refl) = s0 (nat_to_fin Hk) simpl in *.message: Type
X: VLSM message
x: nat
s: fin (S x) → state X
x0: nat
s0: fin (S x0) → state X
k: nat
Hpi: ∀ (i : nat) (li : i < S x0) 
  (j : nat) (lj : j < S x0),
  i = j
  → s0 (nat_to_fin li) = s0 (nat_to_fin lj)
Hsize: S (S (x + x0)) = S (x + S x0)
s'k: state X
Hk: k < S x0
appendi: state X
Hi': k + S x < S (S (x + x0))
(let (nj, Hnj) := to_nat (nat_to_fin Hi') in
 match
   decide (nj < S x) as anonymous'
   return (anonymous' = decide (nj < S x) → state X)
 with
 | left lt_in =>
     λ _ : left lt_in = decide (nj < S x),
       s (nat_to_fin lt_in)
 | right ge_in =>
     λ _ : right ge_in = decide (nj < S x),
       s0
         (nat_to_fin
            (equivocator_state_append_obligation_1
               (existT x s) (existT x0 s0) nj Hnj
               ge_in (nj - S x)
               (Preamble.not_lt_plus_dec_obligation_1
                  (S x) nj ge_in)))
 end eq_refl) = s0 (nat_to_fin Hk)
  rewrite to_nat_of_nat.message: Type
X: VLSM message
x: nat
s: fin (S x) → state X
x0: nat
s0: fin (S x0) → state X
k: nat
Hpi: ∀ (i : nat) (li : i < S x0) 
  (j : nat) (lj : j < S x0),
  i = j
  → s0 (nat_to_fin li) = s0 (nat_to_fin lj)
Hsize: S (S (x + x0)) = S (x + S x0)
s'k: state X
Hk: k < S x0
appendi: state X
Hi': k + S x < S (S (x + x0))
match
  decide (k + S x < S x) as anonymous'
  return
    (anonymous' = decide (k + S x < S x) → state X)
with
| left lt_in =>
    λ _ : left lt_in = decide (k + S x < S x),
      s (nat_to_fin lt_in)
| right ge_in =>
    λ _ : right ge_in = decide (k + S x < S x),
      s0
        (nat_to_fin
           (equivocator_state_append_obligation_1
              (existT x s) (existT x0 s0) (k + S x)
              Hi' ge_in (k + S x - S x)
              (Preamble.not_lt_plus_dec_obligation_1
                 (S x) (k + S x) ge_in)))
end eq_refl = s0 (nat_to_fin Hk)
  by case_decide; [| apply Hpi]; lia.
Qed.

Lemma equivocator_state_append_project_3
  s s' i (Hi : ~ i < equivocator_state_n s + equivocator_state_n s')
  : equivocator_state_project (equivocator_state_append s s') i = None.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: ¬ i <
  equivocator_state_n s + equivocator_state_n s'
equivocator_state_project
  (equivocator_state_append s s') i = None
Proof.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: ¬ i <
  equivocator_state_n s + equivocator_state_n s'
equivocator_state_project
  (equivocator_state_append s s') i = None
  apply equivocator_state_project_None.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: ¬ i <
  equivocator_state_n s + equivocator_state_n s'
¬ i <
  equivocator_state_n (equivocator_state_append s s')
  unfold equivocator_state_n, equivocator_state_append, equivocator_state_last in *.message: Type
X: VLSM message
s, s': equivocator_state
i: nat
Hi: ¬ i < S (projT1 s) + S (projT1 s')
¬ i <
  S
    (projT1
       (existT (equivocator_state_n s + projT1 s')
          (λ j : fin
                   (S
                      (equivocator_state_n s +
                       projT1 s')),
             let (nj, Hnj) := to_nat j in
             match
               decide (nj < equivocator_state_n s) as
               anonymous'
               return
                 (anonymous' =
                  decide (nj < equivocator_state_n s)
                  → state X)
             with
             | left lt_in =>
                 λ _ : left lt_in =
                       decide
                         (nj < equivocator_state_n s),
                   equivocator_state_s s
                     (nat_to_fin lt_in)
             | right ge_in =>
                 λ _ : right ge_in =
                       decide
                         (nj < equivocator_state_n s),
                   let (k, Hk) :=
                     not_lt_plus_dec ge_in in
                   equivocator_state_s s'
                     (nat_to_fin
                        (equivocator_state_append_obligation_1
                           s s' nj Hnj ge_in k Hk))
             end eq_refl)))
  by cbn in *; lia.
Qed.

#[local] Ltac destruct_equivocator_state_append_project' es es' i Hi k Hk Hpr :=
  let Hi' := fresh "Hi" in
  destruct (decide (i < equivocator_state_n es)) as [Hi | Hi']; swap 1 2;
  [destruct (decide (i < equivocator_state_n es + equivocator_state_n es')) as [Hi | Hi];
    swap 1 2;
    [specialize (equivocator_state_append_project_3 es es' i Hi) as Hpr
    | apply not_lt_plus_dec in Hi' as [k Hk];
      specialize (equivocator_state_append_project_2 es es' i k (eq_sym Hk)) as Hpr]
  | specialize (equivocator_state_append_project_1 es es' i Hi) as Hpr]
  ; rewrite Hpr in *
  .

#[local] Ltac destruct_equivocator_state_append_project es es' i Hi k Hk :=
  let Hpr := fresh "Hpr" in
  destruct_equivocator_state_append_project' es es' i Hi k Hk Hpr
  ; clear Hpr.

Lemma equivocator_state_append_singleton_is_extend
  (es1 es2 : equivocator_state)
  (Hsingleton : is_singleton_state es2)
  : equivocator_state_append es1 es2 = equivocator_state_extend es1 (equivocator_state_zero es2).message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: is_singleton_state es2
equivocator_state_append es1 es2 =
equivocator_state_extend es1
  (equivocator_state_zero es2)
Proof.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: is_singleton_state es2
equivocator_state_append es1 es2 =
equivocator_state_extend es1
  (equivocator_state_zero es2)
  apply equivocator_state_project_ext.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: is_singleton_state es2
∀ i : nat,
  equivocator_state_project
    (equivocator_state_append es1 es2) i =
  equivocator_state_project
    (equivocator_state_extend es1
       (equivocator_state_zero es2)) i
  intro i.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: is_singleton_state es2
i: nat
equivocator_state_project
  (equivocator_state_append es1 es2) i =
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i
  symmetry.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: is_singleton_state es2
i: nat
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i =
equivocator_state_project
  (equivocator_state_append es1 es2) i
  unfold is_singleton_state in Hsingleton.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i: nat
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i =
equivocator_state_project
  (equivocator_state_append es1 es2) i
  destruct_equivocator_state_append_project es1 es2 i Hi k Hk.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i = None
message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 + equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i =
equivocator_state_project es2 k
message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i =
equivocator_state_project es1 i
  -message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i = None by apply equivocator_state_extend_project_3; lia.
  -message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 + equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i =
equivocator_state_project es2 k rewrite equivocator_state_extend_project_2 by lia.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 + equivocator_state_n es2
Some (equivocator_state_zero es2) =
equivocator_state_project es2 k
    rewrite <- equivocator_state_project_zero.message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 + equivocator_state_n es2
equivocator_state_project es2 0 =
equivocator_state_project es2 k
    by f_equal; lia.
  -message: Type
X: VLSM message
es1, es2: equivocator_state
Hsingleton: equivocator_state_n es2 = 1
i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_extend es1
     (equivocator_state_zero es2)) i =
equivocator_state_project es1 i by rewrite equivocator_state_extend_project_1 by lia.
Qed.

Lemma equivocator_state_append_extend_commute
  (es1 es2 : equivocator_state)
  (s : state X)
  : equivocator_state_extend (equivocator_state_append es1 es2) s =
    equivocator_state_append es1 (equivocator_state_extend es2 s).message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
equivocator_state_extend
  (equivocator_state_append es1 es2) s =
equivocator_state_append es1
  (equivocator_state_extend es2 s)
Proof.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
equivocator_state_extend
  (equivocator_state_append es1 es2) s =
equivocator_state_append es1
  (equivocator_state_extend es2 s)
  apply equivocator_state_project_ext.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
∀ i : nat,
  equivocator_state_project
    (equivocator_state_extend
       (equivocator_state_append es1 es2) s) i =
  equivocator_state_project
    (equivocator_state_append es1
       (equivocator_state_extend es2 s)) i
  intro i.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i =
equivocator_state_project
  (equivocator_state_append es1
     (equivocator_state_extend es2 s)) i
  destruct_equivocator_state_append_project es1 (equivocator_state_extend es2 s) i Hi k Hk.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  equivocator_state_n
    (equivocator_state_extend es2 s)
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i = None
message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_extend es2 s)
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i =
equivocator_state_project
  (equivocator_state_extend es2 s) k
message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i =
equivocator_state_project es1 i
  -message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  equivocator_state_n
    (equivocator_state_extend es2 s)
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i = None rewrite equivocator_state_extend_size in Hi.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  S (equivocator_state_n es2)
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i = None
    apply equivocator_state_extend_project_3.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  S (equivocator_state_n es2)
equivocator_state_n (equivocator_state_append es1 es2) <
i
    by rewrite equivocator_state_append_size; lia.
  -message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_extend es2 s)
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i =
equivocator_state_project
  (equivocator_state_extend es2 s) k subst; rewrite equivocator_state_extend_size in Hi.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s)
  (k + equivocator_state_n es1) =
equivocator_state_project
  (equivocator_state_extend es2 s) k
    destruct (decide (k = equivocator_state_n es2)).message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
e: k = equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s)
  (k + equivocator_state_n es1) =
equivocator_state_project
  (equivocator_state_extend es2 s) k
message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
n: k ≠ equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s)
  (k + equivocator_state_n es1) =
equivocator_state_project
  (equivocator_state_extend es2 s) k
    +message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
e: k = equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s)
  (k + equivocator_state_n es1) =
equivocator_state_project
  (equivocator_state_extend es2 s) k subst.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
Hi: equivocator_state_n es2 + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s)
  (equivocator_state_n es2 + equivocator_state_n es1) =
equivocator_state_project
  (equivocator_state_extend es2 s)
  (equivocator_state_n es2)
      rewrite !equivocator_state_extend_project_2
      ; [done | done |].message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
Hi: equivocator_state_n es2 + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
equivocator_state_n es2 + equivocator_state_n es1 =
equivocator_state_n (equivocator_state_append es1 es2)
      by rewrite equivocator_state_append_size; lia.
    +message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
n: k ≠ equivocator_state_n es2
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s)
  (k + equivocator_state_n es1) =
equivocator_state_project
  (equivocator_state_extend es2 s) k rewrite !equivocator_state_extend_project_1
      ; [rewrite equivocator_state_append_project_2 with (k := k) | lia |]
      ; [done | done |].message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 +
S (equivocator_state_n es2)
n: k ≠ equivocator_state_n es2
k + equivocator_state_n es1 <
equivocator_state_n (equivocator_state_append es1 es2)
      by rewrite equivocator_state_append_size; lia.
  -message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_extend
     (equivocator_state_append es1 es2) s) i =
equivocator_state_project es1 i rewrite equivocator_state_extend_project_1.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_append es1 es2) i =
equivocator_state_project es1 i
message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es1
i <
equivocator_state_n (equivocator_state_append es1 es2)
    +message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_append es1 es2) i =
equivocator_state_project es1 i by rewrite equivocator_state_append_project_1.
    +message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
i: nat
Hi: i < equivocator_state_n es1
i <
equivocator_state_n (equivocator_state_append es1 es2) by rewrite equivocator_state_append_size; lia.
Qed.

Lemma equivocator_state_append_update_commute es1 es2 s n
  : equivocator_state_update (equivocator_state_append es1 es2) (n + equivocator_state_n es1) s =
    equivocator_state_append es1 (equivocator_state_update es2 n s).message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n: nat
equivocator_state_update
  (equivocator_state_append es1 es2)
  (n + equivocator_state_n es1) s =
equivocator_state_append es1
  (equivocator_state_update es2 n s)
Proof.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n: nat
equivocator_state_update
  (equivocator_state_append es1 es2)
  (n + equivocator_state_n es1) s =
equivocator_state_append es1
  (equivocator_state_update es2 n s)
  apply equivocator_state_project_ext.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n: nat
∀ i : nat,
  equivocator_state_project
    (equivocator_state_update
       (equivocator_state_append es1 es2)
       (n + equivocator_state_n es1) s) i =
  equivocator_state_project
    (equivocator_state_append es1
       (equivocator_state_update es2 n s)) i
  intro i.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i: nat
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project
  (equivocator_state_append es1
     (equivocator_state_update es2 n s)) i
  destruct_equivocator_state_append_project es1 (equivocator_state_update es2 n s) i Hi k Hk.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  equivocator_state_n
    (equivocator_state_update es2 n s)
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i = None
message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_update es2 n s)
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project
  (equivocator_state_update es2 n s) k
message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project es1 i
  -message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  equivocator_state_n
    (equivocator_state_update es2 n s)
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i = None apply equivocator_state_project_None.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i: nat
Hi0: ¬ i < equivocator_state_n es1
Hi: ¬ i <
  equivocator_state_n es1 +
  equivocator_state_n
    (equivocator_state_update es2 n s)
¬ i <
  equivocator_state_n
    (equivocator_state_update
       (equivocator_state_append es1 es2)
       (n + equivocator_state_n es1) s)
    by rewrite equivocator_state_update_size, equivocator_state_append_size in *; lia.
  -message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_update es2 n s)
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project
  (equivocator_state_update es2 n s) k destruct (decide (n = k)).message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_update es2 n s)
e: n = k
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project
  (equivocator_state_update es2 n s) k
message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_update es2 n s)
n0: n ≠ k
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project
  (equivocator_state_update es2 n s) k
    +message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_update es2 n s)
e: n = k
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project
  (equivocator_state_update es2 n s) k subst; rewrite equivocator_state_update_size in Hi.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 + equivocator_state_n es2
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (k + equivocator_state_n es1) s)
  (k + equivocator_state_n es1) =
equivocator_state_project
  (equivocator_state_update es2 k s) k
      rewrite equivocator_state_update_project_eq;
      [| rewrite equivocator_state_append_size; lia | done].message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
k: nat
Hi: k + equivocator_state_n es1 <
equivocator_state_n es1 + equivocator_state_n es2
Some s =
equivocator_state_project
  (equivocator_state_update es2 k s) k
      by rewrite equivocator_state_update_project_eq; [| lia |].
    +message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_update es2 n s)
n0: n ≠ k
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project
  (equivocator_state_update es2 n s) k rewrite !equivocator_state_update_project_neq by lia.message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i, k: nat
Hk: k + equivocator_state_n es1 = i
Hi: i <
equivocator_state_n es1 +
equivocator_state_n
  (equivocator_state_update es2 n s)
n0: n ≠ k
equivocator_state_project
  (equivocator_state_append es1 es2) i =
equivocator_state_project es2 k
      by apply equivocator_state_append_project_2 with (k := k).
  -message: Type
X: VLSM message
es1, es2: equivocator_state
s: state X
n, i: nat
Hi: i < equivocator_state_n es1
equivocator_state_project
  (equivocator_state_update
     (equivocator_state_append es1 es2)
     (n + equivocator_state_n es1) s) i =
equivocator_state_project es1 i by rewrite equivocator_state_update_project_neq,
      equivocator_state_append_project_1 by lia.
Qed.

(*
  An [equivocator_state] has the [initial_state_prop]erty if it only
  contains one state of original machine, and that state is initial.
*)
Definition equivocator_initial_state_prop
  (bs : equivocator_state)
  : Prop
  := is_singleton_state bs /\ initial_state_prop X (equivocator_state_zero bs).

Definition equivocator_initial_state : Type :=
  {bs : equivocator_state | equivocator_initial_state_prop bs}.

Program Definition equivocator_s0 : equivocator_initial_state :=
  exist _ (mk_singleton_state (proj1_sig (vs0 X))) _.
Next Obligation.message: Type
X: VLSM message
(λ bs : equivocator_state,
   equivocator_initial_state_prop bs)
  (mk_singleton_state (`(vs0 X)))
Proof.message: Type
X: VLSM message
(λ bs : equivocator_state,
   equivocator_initial_state_prop bs)
  (mk_singleton_state (`(vs0 X)))
  unfold mk_singleton_state, equivocator_initial_state_prop; cbn.message: Type
X: VLSM message
is_singleton_state (existT 0 (λ _ : fin 1, `(vs0 X)))
∧ initial_state_prop (`(vs0 X))
  by split; [| destruct (vs0 X)].
Defined.

#[export] Instance equivocator_initial_state_inh : Inhabited equivocator_initial_state :=
  populate equivocator_s0.

Definition equivocator_transition
  (bl : equivocator_label)
  (bsom : equivocator_state * option message)
  : equivocator_state * option message
  :=
  match bl with
  | Spawn sn  => (* creating a new machine with initial state sn*)
    (equivocator_state_extend bsom.1 sn, None)
  | ContinueWith i l =>
    match equivocator_state_project bsom.1 i with
    | None => bsom
    | Some si =>
      let (si', om') := transition X l (si, bsom.2) in
      (equivocator_state_update bsom.1 i si', om')
    end
  | ForkWith i l =>
    match equivocator_state_project bsom.1 i with
    | None => bsom
    | Some si =>
      let (si', om') := transition X l (si, bsom.2) in
      (equivocator_state_extend bsom.1 si', om')
    end
  end.

Definition equivocator_valid
  (bl : equivocator_label)
  (bsom : equivocator_state * option message)
  : Prop
  :=
  match bl with
  | Spawn sn  => (* state is initial *)
    initial_state_prop X sn /\ bsom.2 = None
  | ContinueWith i l | ForkWith i l =>
    match equivocator_state_project bsom.1 i with
    | Some si => valid X l (si, bsom.2)
    | None => False
    end
  end.

Definition equivocator_vlsm_machine
  : VLSMMachine equivocator_type
  :=
  {|  initial_state_prop := equivocator_initial_state_prop
   ;  initial_message_prop := @initial_message_prop _ _ X
   ;  transition := equivocator_transition
   ;  valid := equivocator_valid
  |}.

Definition equivocator_vlsm
  : VLSM message
  :=
  mk_vlsm equivocator_vlsm_machine.

Lemma equivocator_vlsm_initial_message_preservation
  : strong_embedding_initial_message_preservation X equivocator_vlsm.message: Type
X: VLSM message
strong_embedding_initial_message_preservation X
  equivocator_vlsm
Proof.message: Type
X: VLSM message
strong_embedding_initial_message_preservation X
  equivocator_vlsm by intro. Qed.

Lemma equivocator_vlsm_initial_message_preservation_rev
  : strong_embedding_initial_message_preservation equivocator_vlsm X.message: Type
X: VLSM message
strong_embedding_initial_message_preservation
  equivocator_vlsm X
Proof.message: Type
X: VLSM message
strong_embedding_initial_message_preservation
  equivocator_vlsm X by intro. Qed.

Lemma equivocator_vlsm_initial_state_preservation_rev is i s
  (Hs : equivocator_state_project is i = Some s)
  : initial_state_prop equivocator_vlsm is -> initial_state_prop X s.message: Type
X: VLSM message
is: equivocator_state
i: nat
s: state X
Hs: equivocator_state_project is i = Some s
initial_state_prop is → initial_state_prop s
Proof.message: Type
X: VLSM message
is: equivocator_state
i: nat
s: state X
Hs: equivocator_state_project is i = Some s
initial_state_prop is → initial_state_prop s
  intros [Hzero Hinit].message: Type
X: VLSM message
is: equivocator_state
i: nat
s: state X
Hs: equivocator_state_project is i = Some s
Hzero: is_singleton_state is
Hinit: initial_state_prop (equivocator_state_zero is)
initial_state_prop s
  apply equivocator_state_project_Some_rev in Hs as Hlt_i.message: Type
X: VLSM message
is: equivocator_state
i: nat
s: state X
Hs: equivocator_state_project is i = Some s
Hzero: is_singleton_state is
Hinit: initial_state_prop (equivocator_state_zero is)
Hlt_i: i < equivocator_state_n is
initial_state_prop s
  replace i with 0 in * by (cbv in *; lia).message: Type
X: VLSM message
is: equivocator_state
i: nat
s: state X
Hs: equivocator_state_project is 0 = Some s
Hzero: is_singleton_state is
Hinit: initial_state_prop (equivocator_state_zero is)
Hlt_i: 0 < equivocator_state_n is
initial_state_prop s
  by rewrite equivocator_state_project_zero in Hs; inversion Hs.
Qed.

Lemma mk_singleton_initial_state
  (s : state X)
  : initial_state_prop X s ->
    initial_state_prop equivocator_vlsm (mk_singleton_state s).message: Type
X: VLSM message
s: state X
initial_state_prop s
→ initial_state_prop (mk_singleton_state s)
Proof.message: Type
X: VLSM message
s: state X
initial_state_prop s
→ initial_state_prop (mk_singleton_state s) done. Qed.

End sec_equivocator_vlsm.

#[export] Hint Rewrite @equivocator_state_update_size : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_update_lst : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_update_project_eq using first [done | lia]
  : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_update_project_neq using first [done | lia]
  : equivocator_state_update.

#[export] Hint Rewrite @equivocator_state_extend_size using done : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_extend_lst using done : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_extend_project_1 using first [done | lia]
  : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_extend_project_2 using first [done | lia]
  : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_extend_project_3 using first [done | lia]
  : equivocator_state_update.

#[export] Hint Rewrite @equivocator_state_append_size using done : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_append_lst using done : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_append_project_1 using first [done | lia]
  : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_append_project_2 using first [done | lia]
  : equivocator_state_update.
#[export] Hint Rewrite @equivocator_state_append_project_3 using first [done | lia]
  : equivocator_state_update.

Ltac equivocator_state_update_simpl :=
  autounfold with state_update in *;
  autorewrite with equivocator_state_update state_update in *.

Arguments Spawn {_ _} _ : assert.
Arguments ContinueWith {_ _} _ _ : assert.
Arguments ForkWith {_ _} _ _ : assert.
Arguments equivocator_state_n {_ _} _ : assert.
Arguments equivocator_state_last {_ _} _ : assert.
Arguments equivocator_state_zero {_ _} _ : assert.
Arguments equivocator_state_s {_ _} _ _ : assert.
Arguments equivocator_state_project {_ _} _ _ : assert.
Arguments equivocator_state_update {_ _} _ _ _ : assert.
Arguments equivocator_state_extend {_ _} _ _ : assert.
Arguments equivocator_state_append {_ _} _ _ : assert.

Ltac destruct_equivocator_state_project' es i si Hi Hpr :=
  destruct (equivocator_state_project es i) as [si |] eqn: Hpr
  ; [specialize (equivocator_state_project_Some_rev _ _ _ _ Hpr) as Hi
    | specialize (equivocator_state_project_None_rev _ _ _ Hpr) as Hi].

Ltac destruct_equivocator_state_project es i si Hi :=
  let Hpr := fresh "Hpr" in
  destruct_equivocator_state_project' es i si Hi Hpr
  ; clear Hpr.

Ltac destruct_equivocator_state_update_project' es i s j Hj Hij Hpr :=
  let Hsize := fresh "Hsize" in
  pose proof (equivocator_state_update_size _ es i s) as Hsize
  ; destruct (decide (j < equivocator_state_n es)) as [Hj | Hj]; swap 1 2
  ; [specialize (equivocator_state_project_None _ (equivocator_state_update es i s) j Hj) as Hpr
    | destruct (decide (i = j)) as [Hij | Hij]
    ; [specialize (equivocator_state_update_project_eq _ es i s j Hj Hij) as Hpr
      | specialize (equivocator_state_update_project_neq _ es i s j Hij) as Hpr]]
  ; rewrite Hpr in *
  ; clear Hsize.

Ltac destruct_equivocator_state_update_project es i s j Hj Hij :=
  let Hpr := fresh "Hpr" in
  destruct_equivocator_state_update_project' es i s j Hj Hij Hpr
  ; clear Hpr.

Ltac destruct_equivocator_state_extend_project' es s i Hi Hpr :=
  let Hni := fresh "Hni" in
  let Hni' := fresh "Hni" in
  destruct (decide (i < equivocator_state_n es)) as [Hi | Hni]
  ; [| destruct (decide (i = equivocator_state_n es)) as [Hi | Hni']]
  ; [| | assert (Hi : equivocator_state_n es < i) by lia]
  ; [specialize (equivocator_state_extend_project_1 _ es s i Hi) as Hpr
    | specialize (equivocator_state_extend_project_2 _ es s i Hi) as Hpr
    | specialize (equivocator_state_extend_project_3 _ es s i Hi) as Hpr]
  ; rewrite Hpr in *.

Ltac destruct_equivocator_state_extend_project es s i Hi :=
  let Hpr := fresh "Hpr" in
  destruct_equivocator_state_extend_project' es s i Hi Hpr
  ; clear Hpr.

Section sec_equivocator_vlsm_valid_state_projections.

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

When projecting an equivocator trace on one copy, we start from its final state and trace back transitions, making sure to follow ForkWith transitions back to their original copy and to stop on Spawn transitions.

To do that we need to track the current copy, or whether we already reached the initial state.

NewMachine s indicates that a Spawn s was already reached for the copy being tracked
Existing i indicates that we're currently tracking copy i

Inductive MachineDescriptor : Type :=
| NewMachine : state X -> MachineDescriptor
| Existing : nat -> MachineDescriptor.

The MachineDescriptor associated to an equivocator_label tells us which copy should we continue with if the current transition is relevant for the copy we're tracking.

Definition equivocator_label_descriptor (l : equivocator_label X) : MachineDescriptor :=
  match l with
  | Spawn sn => NewMachine sn
  | ContinueWith i _ | ForkWith i _ => Existing i
  end.

Definition is_newmachine_descriptor (d : MachineDescriptor) : Prop
  := match d with
    | NewMachine _ => True
    | _ => False
  end.

Lemma newmachine_descriptor_dec (d : MachineDescriptor)
  : Decision (is_newmachine_descriptor d).message: Type
X: VLSM message
d: MachineDescriptor
Decision (is_newmachine_descriptor d)
Proof.message: Type
X: VLSM message
d: MachineDescriptor
Decision (is_newmachine_descriptor d)
  destruct d.message: Type
X: VLSM message
s: state X
Decision (is_newmachine_descriptor (NewMachine s))
message: Type
X: VLSM message
n: nat
Decision (is_newmachine_descriptor (Existing n))
  -message: Type
X: VLSM message
s: state X
Decision (is_newmachine_descriptor (NewMachine s)) by left.
  -message: Type
X: VLSM message
n: nat
Decision (is_newmachine_descriptor (Existing n)) by right; itauto.
Qed.

Projecting an equivocator_state over a MachineDescriptor.

Definition equivocator_state_descriptor_project
  (s : equivocator_state X)
  (descriptor : MachineDescriptor)
  : state X
  :=
  match descriptor with
  | NewMachine sn => sn
  | Existing j => default (equivocator_state_zero s) (equivocator_state_project s j)
  end.

Whether a MachineDescriptor can be used to project an equivocator_state to a regular state. The NewMachine descriptor signals that an equivocation has occurred starting a new machine, thus we require the argument to be initial. For an Existing descriptor, the index of the descriptor must refer to an existing machine in the current state.

Definition proper_descriptor
  (d : MachineDescriptor)
  (s : state (equivocator_vlsm X))
  :=
  match d with
  | NewMachine sn => initial_state_prop X sn
  | Existing i => is_Some (equivocator_state_project s i)
  end.

Definition proper_equivocator_label
  (l : equivocator_label X)
  (s : equivocator_state X)
  := proper_descriptor (equivocator_label_descriptor l) s.

Existing-only descriptor.

Definition existing_descriptor
  (d : MachineDescriptor)
  (s : state (equivocator_vlsm X))
  :=
  match d with
  | Existing i => is_Some (equivocator_state_project s i)
  | _ => False
  end.

#[local] Instance  existing_descriptor_dec : RelDecision existing_descriptor.message: Type
X: VLSM message
RelDecision existing_descriptor
Proof.message: Type
X: VLSM message
RelDecision existing_descriptor
  intros d s.message: Type
X: VLSM message
d: MachineDescriptor
s: state (equivocator_vlsm X)
Decision (existing_descriptor d s) destruct d; simpl.message: Type
X: VLSM message
s0: state X
s: state (equivocator_vlsm X)
Decision False
message: Type
X: VLSM message
n: nat
s: state (equivocator_vlsm X)
Decision (is_Some (equivocator_state_project s n))
  -message: Type
X: VLSM message
s0: state X
s: state (equivocator_vlsm X)
Decision False by right; itauto.
  -message: Type
X: VLSM message
n: nat
s: state (equivocator_vlsm X)
Decision (is_Some (equivocator_state_project s n)) destruct_equivocator_state_project s n _sn Hn.message: Type
X: VLSM message
n: nat
s: state (equivocator_vlsm X)
_sn: state X
Hn: n < equivocator_state_n s
Decision (is_Some (Some _sn))
message: Type
X: VLSM message
n: nat
s: state (equivocator_vlsm X)
Hn: ¬ n < equivocator_state_n s
Decision (is_Some None)
    +message: Type
X: VLSM message
n: nat
s: state (equivocator_vlsm X)
_sn: state X
Hn: n < equivocator_state_n s
Decision (is_Some (Some _sn)) by left.
    +message: Type
X: VLSM message
n: nat
s: state (equivocator_vlsm X)
Hn: ¬ n < equivocator_state_n s
Decision (is_Some None) by right; intros [si Hi]; congruence.
Qed.

Definition existing_equivocator_label
  (l : equivocator_label X)
  := match l with Spawn _ => False | _ => True end.

Definition existing_equivocator_label_extract
  (l : equivocator_label X)
  (Hs : existing_equivocator_label l)
  : label X.message: Type
X: VLSM message
l: equivocator_label X
Hs: existing_equivocator_label l
label X
Proof.message: Type
X: VLSM message
l: equivocator_label X
Hs: existing_equivocator_label l
label X
  by destruct l.
Defined.

Definition proper_existing_equivocator_label
  (l : equivocator_label X)
  (s : equivocator_state X)
  := existing_descriptor (equivocator_label_descriptor l) s.

Lemma existing_equivocator_label_forget_proper
  {l : equivocator_label X}
  {s : equivocator_state X}
  (Hs : proper_existing_equivocator_label l s)
  : existing_equivocator_label l.message: Type
X: VLSM message
l: equivocator_label X
s: equivocator_state X
Hs: proper_existing_equivocator_label l s
existing_equivocator_label l
Proof.message: Type
X: VLSM message
l: equivocator_label X
s: equivocator_state X
Hs: proper_existing_equivocator_label l s
existing_equivocator_label l
  by destruct l; [inversion Hs | ..].
Qed.

Lemma existing_descriptor_proper
  (d : MachineDescriptor)
  (s : state (equivocator_vlsm X))
  (Hned : existing_descriptor d s)
  : proper_descriptor d s.message: Type
X: VLSM message
d: MachineDescriptor
s: state (equivocator_vlsm X)
Hned: existing_descriptor d s
proper_descriptor d s
Proof.message: Type
X: VLSM message
d: MachineDescriptor
s: state (equivocator_vlsm X)
Hned: existing_descriptor d s
proper_descriptor d s by destruct d. Qed.

(*
  TODO: derive some some simpler lemmas about the equivocator operations,
  or a simpler way of defining the equivocator_transition - it's not nice
  to need to pick apart these cases from inside equivocator_transition inside
  of so many proofs.
*)

If the state obtained after one transition has no equivocation, then the descriptor of the label of the transition must be Existing 0 false

Lemma equivocator_transition_no_equivocation_zero_descriptor
  (iom oom : option message)
  (l : label (equivocator_vlsm X))
  (s s' : state (equivocator_vlsm X))
  (Hv : valid (equivocator_vlsm X) l (s, iom))
  (Ht : transition (equivocator_vlsm X) l (s, iom) = (s', oom))
  (Hs' : is_singleton_state X s')
  : exists li, l = ContinueWith 0 li.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Hv: valid l (s, iom)
Ht: transition l (s, iom) = (s', oom)
Hs': is_singleton_state X s'
∃ li : label X, l = ContinueWith 0 li
Proof.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Hv: valid l (s, iom)
Ht: transition l (s, iom) = (s', oom)
Hs': is_singleton_state X s'
∃ li : label X, l = ContinueWith 0 li
  unfold is_singleton_state in Hs'.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Hv: valid l (s, iom)
Ht: transition l (s, iom) = (s', oom)
Hs': equivocator_state_n s' = 1
∃ li : label X, l = ContinueWith 0 li
  destruct l as [sn | ei l | ei l]
  ; [inversion Ht; subst; rewrite equivocator_state_extend_size in Hs'; cbv in Hs'; lia | ..]
  ; cbn in Hv, Ht;  destruct_equivocator_state_project s ei sei Hei; [| done | | done]
  ; destruct (transition _ _ _) as (si', om')
  ; inversion Ht; subst; equivocator_state_update_simpl.message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
sei: state X
Hv: valid l (sei, iom)
si': state X
Hs': equivocator_state_n s = 1
Ht: (equivocator_state_update s ei si', oom) =
(equivocator_state_update s ei si', oom)
Hei: ei < equivocator_state_n s
∃ li : label X, ContinueWith ei l = ContinueWith 0 li
message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
sei: state X
Hv: valid l (sei, iom)
si': state X
Hs': S (equivocator_state_n s) = 1
Ht: (equivocator_state_extend s si', oom) =
(equivocator_state_extend s si', oom)
Hei: ei < equivocator_state_n s
∃ li : label X, ForkWith ei l = ContinueWith 0 li
  -message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
sei: state X
Hv: valid l (sei, iom)
si': state X
Hs': equivocator_state_n s = 1
Ht: (equivocator_state_update s ei si', oom) =
(equivocator_state_update s ei si', oom)
Hei: ei < equivocator_state_n s
∃ li : label X, ContinueWith ei l = ContinueWith 0 li by exists l; f_equal; lia.
  -message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
sei: state X
Hv: valid l (sei, iom)
si': state X
Hs': S (equivocator_state_n s) = 1
Ht: (equivocator_state_extend s si', oom) =
(equivocator_state_extend s si', oom)
Hei: ei < equivocator_state_n s
∃ li : label X, ForkWith ei l = ContinueWith 0 li by lia.
Qed.

If the state obtained after one transition has no equivocation, then the state prior to the transition has no equivocation as well.

Lemma equivocator_transition_reflects_singleton_state
  (iom oom : option message)
  (l : label (equivocator_vlsm X))
  (s s' : state (equivocator_vlsm X))
  (Ht : equivocator_transition X l (s, iom) = (s', oom))
  : is_singleton_state X s' -> is_singleton_state X s.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
is_singleton_state X s' → is_singleton_state X s
Proof.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
is_singleton_state X s' → is_singleton_state X s
  unfold is_singleton_state.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
equivocator_state_n s' = 1 → equivocator_state_n s = 1
  by destruct l as [sn | ei l | ei l]; cbn in Ht
  ; [inversion Ht; rewrite equivocator_state_extend_size; cbv; lia | ..]
  ; destruct (equivocator_state_project _ _)
  ; [| by inversion Ht | | by inversion Ht]
  ; destruct (transition _ _ _) as (si', om')
  ; inversion Ht; subst; clear Ht; equivocator_state_update_simpl.
Qed.

Lemma equivocator_transition_cannot_decrease_state_size
  (iom oom : option message)
  (l : label (equivocator_vlsm X))
  (s s' : state (equivocator_vlsm X))
  (Ht : equivocator_transition X l (s, iom) = (s', oom))
  : equivocator_state_n s <= equivocator_state_n s'.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
equivocator_state_n s ≤ equivocator_state_n s'
Proof.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
equivocator_state_n s ≤ equivocator_state_n s'
  specialize (equivocator_state_extend_size X s) as Hex_size.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
Hex_size: ∀ s0 : state X,
  equivocator_state_n
    (equivocator_state_extend s s0) =
  S (equivocator_state_n s)
equivocator_state_n s ≤ equivocator_state_n s'
  destruct l as [sn | ei l | ei l]
  ; [inversion Ht; rewrite Hex_size; lia | ..]
  ; cbn in Ht
  ; destruct (equivocator_state_project _ _)
  ; [| by inversion Ht; lia | | by inversion Ht; lia]
  ; destruct (transition _ _ _) as (si', om')
  ; inversion Ht; subst; clear Ht.message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
s0, si': state X
Hex_size: ∀ s0 : state X,
  equivocator_state_n
    (equivocator_state_extend s s0) =
  S (equivocator_state_n s)
equivocator_state_n s
≤ equivocator_state_n
    (equivocator_state_update s ei si')
message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
s0, si': state X
Hex_size: ∀ s0 : state X,
  equivocator_state_n
    (equivocator_state_extend s s0) =
  S (equivocator_state_n s)
equivocator_state_n s
≤ equivocator_state_n (equivocator_state_extend s si')
  -message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
s0, si': state X
Hex_size: ∀ s0 : state X,
  equivocator_state_n
    (equivocator_state_extend s s0) =
  S (equivocator_state_n s)
equivocator_state_n s
≤ equivocator_state_n
    (equivocator_state_update s ei si') by equivocator_state_update_simpl.
  -message: Type
X: VLSM message
iom, oom: option message
ei: nat
l: label X
s: state (equivocator_vlsm X)
s0, si': state X
Hex_size: ∀ s0 : state X,
  equivocator_state_n
    (equivocator_state_extend s s0) =
  S (equivocator_state_n s)
equivocator_state_n s
≤ equivocator_state_n (equivocator_state_extend s si') by rewrite Hex_size; lia.
Qed.

Lemma equivocator_transition_preserves_equivocating_state
  (iom oom : option message)
  (l : label (equivocator_vlsm X))
  (s s' : state (equivocator_vlsm X))
  (Ht : equivocator_transition X l (s, iom) = (s', oom))
  : is_equivocating_state X s -> is_equivocating_state X s'.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
is_equivocating_state X s → is_equivocating_state X s'
Proof.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
is_equivocating_state X s → is_equivocating_state X s'
  intros Hs Hs'.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
Hs: is_equivocating_state X s
Hs': is_singleton_state X s'
False elim Hs.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
Hs: is_equivocating_state X s
Hs': is_singleton_state X s'
is_singleton_state X s clear Hs.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
Hs': is_singleton_state X s'
is_singleton_state X s revert Ht Hs' .message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
equivocator_transition X l (s, iom) = (s', oom)
→ is_singleton_state X s' → is_singleton_state X s
  by apply equivocator_transition_reflects_singleton_state.
Qed.

Lemma zero_descriptor_transition_reflects_equivocating_state
  (iom oom : option message)
  (l : label (equivocator_vlsm X))
  (s s' : state (equivocator_vlsm X))
  (Ht : equivocator_transition X l (s, iom) = (s', oom))
  li
  (Hzero : l = ContinueWith 0 li)
  : is_equivocating_state X s' -> is_equivocating_state X s.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
li: label X
Hzero: l = ContinueWith 0 li
is_equivocating_state X s' → is_equivocating_state X s
Proof.message: Type
X: VLSM message
iom, oom: option message
l: label (equivocator_vlsm X)
s, s': state (equivocator_vlsm X)
Ht: equivocator_transition X l (s, iom) = (s', oom)
li: label X
Hzero: l = ContinueWith 0 li
is_equivocating_state X s' → is_equivocating_state X s
  subst.message: Type
X: VLSM message
iom, oom: option message
s, s': state (equivocator_vlsm X)
li: label X
Ht: equivocator_transition X 
  (ContinueWith 0 li) (
  s, iom) = (s', oom)
is_equivocating_state X s' → is_equivocating_state X s
  cbn in Ht.message: Type
X: VLSM message
iom, oom: option message
s, s': state (equivocator_vlsm X)
li: label X
Ht: match equivocator_state_project s 0 with
| Some si =>
    let (si', om') := transition li (si, iom) in
    (equivocator_state_update s 0 si', om')
| None => (s, iom)
end = (s', oom)
is_equivocating_state X s' → is_equivocating_state X s
  rewrite equivocator_state_project_zero in Ht.message: Type
X: VLSM message
iom, oom: option message
s, s': state (equivocator_vlsm X)
li: label X
Ht: (let (si', om') :=
   transition li (equivocator_state_zero s, iom) in
 (equivocator_state_update s 0 si', om')) =
(s', oom)
is_equivocating_state X s' → is_equivocating_state X s
  destruct (transition _ _ _).message: Type
X: VLSM message
iom, oom: option message
s, s': state (equivocator_vlsm X)
li: label X
s0: state X
o: option message
Ht: (equivocator_state_update s 0 s0, o) = (s', oom)
is_equivocating_state X s' → is_equivocating_state X s
  inversion Ht.message: Type
X: VLSM message
iom, oom: option message
s, s': state (equivocator_vlsm X)
li: label X
s0: state X
o: option message
Ht: (equivocator_state_update s 0 s0, o) = (s', oom)
H0: equivocator_state_update s 0 s0 = s'
H1: o = oom
is_equivocating_state X
  (equivocator_state_update s 0 s0)
→ is_equivocating_state X s subst.message: Type
X: VLSM message
iom, oom: option message
s: state (equivocator_vlsm X)
li: label X
s0: state X
Ht: (equivocator_state_update s 0 s0, oom) =
(equivocator_state_update s 0 s0, oom)
is_equivocating_state X
  (equivocator_state_update s 0 s0)
→ is_equivocating_state X s
  unfold is_equivocating_state, is_singleton_state.message: Type
X: VLSM message
iom, oom: option message
s: state (equivocator_vlsm X)
li: label X
s0: state X
Ht: (equivocator_state_update s 0 s0, oom) =
(equivocator_state_update s 0 s0, oom)
equivocator_state_n (equivocator_state_update s 0 s0)
≠ 1 → equivocator_state_n s ≠ 1
  by equivocator_state_update_simpl.
Qed.

Valid messages in the equivocator_vlsm are also valid in the original machine. All components of a valid state in the equivocator_vlsm are also valid in the original machine.

Lemma preloaded_equivocator_state_projection_preserves_validity
  (seed : message -> Prop)
  (bs : state (equivocator_vlsm X))
  (om : option message)
  (Hbs : valid_state_message_prop (preloaded_vlsm (equivocator_vlsm X) seed) bs om)
  : option_valid_message_prop (preloaded_vlsm X seed) om /\
    forall i si,
      equivocator_state_project bs i = Some si ->
      valid_state_prop (preloaded_vlsm X seed) si.message: Type
X: VLSM message
seed: message → Prop
bs: state (equivocator_vlsm X)
om: option message
Hbs: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) bs
  om
option_valid_message_prop (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project bs i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si)
Proof.message: Type
X: VLSM message
seed: message → Prop
bs: state (equivocator_vlsm X)
om: option message
Hbs: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) bs
  om
option_valid_message_prop (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project bs i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si)
  induction Hbs.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
option_valid_message_prop (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si)
message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
Hv: valid l (s, om)
s': state (preloaded_vlsm (equivocator_vlsm X) seed)
om': option message
Ht: transition l (s, om) = (s', om')
IHHbs1: option_valid_message_prop
  (preloaded_vlsm X seed) _om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s i = Some si
     → valid_state_prop
         (preloaded_vlsm X seed) si)
IHHbs2: option_valid_message_prop
  (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project _s i = Some si
     → valid_state_prop
         (preloaded_vlsm X seed) si)
option_valid_message_prop (preloaded_vlsm X seed) om'
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s' i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si)
  -message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
option_valid_message_prop (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si) split; [by apply option_initial_message_is_valid |].message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed) si
    intros.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hs: initial_state_prop s
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
i: nat
si: state X
H: equivocator_state_project s i = Some si
valid_state_prop (preloaded_vlsm X seed) si
    destruct Hs as [Hn0 Hinit].message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hn0: is_singleton_state X s
Hinit: initial_state_prop (equivocator_state_zero s)
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
i: nat
si: state X
H: equivocator_state_project s i = Some si
valid_state_prop (preloaded_vlsm X seed) si
    apply equivocator_state_project_Some_rev in H as Hi.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hn0: is_singleton_state X s
Hinit: initial_state_prop (equivocator_state_zero s)
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
i: nat
si: state X
H: equivocator_state_project s i = Some si
Hi: i < equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si
    unfold is_singleton_state in Hn0.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hn0: equivocator_state_n s = 1
Hinit: initial_state_prop (equivocator_state_zero s)
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
i: nat
si: state X
H: equivocator_state_project s i = Some si
Hi: i < equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si
    replace i with 0 in * by lia.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hn0: equivocator_state_n s = 1
Hinit: initial_state_prop (equivocator_state_zero s)
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
i: nat
si: state X
H: equivocator_state_project s 0 = Some si
Hi: 0 < equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si
    rewrite equivocator_state_project_zero in H; inversion H.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hn0: equivocator_state_n s = 1
Hinit: initial_state_prop (equivocator_state_zero s)
om: option message
Hom: option_initial_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
i: nat
si: state X
H: Some (equivocator_state_zero s) = Some si
Hi: 0 < equivocator_state_n s
H1: equivocator_state_zero s = si
valid_state_prop (preloaded_vlsm X seed)
  (equivocator_state_zero s)
    by apply initial_state_is_valid.
  -message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
Hv: valid l (s, om)
s': state (preloaded_vlsm (equivocator_vlsm X) seed)
om': option message
Ht: transition l (s, om) = (s', om')
IHHbs1: option_valid_message_prop
  (preloaded_vlsm X seed) _om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s i = Some si
     → valid_state_prop
         (preloaded_vlsm X seed) si)
IHHbs2: option_valid_message_prop
  (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project _s i = Some si
     → valid_state_prop
         (preloaded_vlsm X seed) si)
option_valid_message_prop (preloaded_vlsm X seed) om'
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s' i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si) specialize (valid_generated_state_message (preloaded_vlsm X seed)) as Hgen.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
Hv: valid l (s, om)
s': state (preloaded_vlsm (equivocator_vlsm X) seed)
om': option message
Ht: transition l (s, om) = (s', om')
IHHbs1: option_valid_message_prop
  (preloaded_vlsm X seed) _om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s i = Some si
     → valid_state_prop
         (preloaded_vlsm X seed) si)
IHHbs2: option_valid_message_prop
  (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project _s i = Some si
     → valid_state_prop
         (preloaded_vlsm X seed) si)
Hgen: ∀ (s : state (preloaded_vlsm X seed)) 
  (_om : option message),
  valid_state_message_prop
    (preloaded_vlsm X seed) s _om
  → ∀ (_s : state (preloaded_vlsm X seed)) 
      (om : option message),
      valid_state_message_prop
        (preloaded_vlsm X seed) _s om
      → ∀ l : label (preloaded_vlsm X seed),
          valid l (s, om)
          → ∀ (s' : state
                      (preloaded_vlsm X seed)) 
              (om' : option message),
              transition l (s, om) = (s', om')
              → valid_state_message_prop
                  (preloaded_vlsm X seed) s'
                  om'
option_valid_message_prop (preloaded_vlsm X seed) om'
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s' i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si)
    apply proj2 in IHHbs1.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
Hv: valid l (s, om)
s': state (preloaded_vlsm (equivocator_vlsm X) seed)
om': option message
Ht: transition l (s, om) = (s', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
IHHbs2: option_valid_message_prop
  (preloaded_vlsm X seed) om
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project _s i = Some si
     → valid_state_prop
         (preloaded_vlsm X seed) si)
Hgen: ∀ (s : state (preloaded_vlsm X seed)) 
  (_om : option message),
  valid_state_message_prop
    (preloaded_vlsm X seed) s _om
  → ∀ (_s : state (preloaded_vlsm X seed)) 
      (om : option message),
      valid_state_message_prop
        (preloaded_vlsm X seed) _s om
      → ∀ l : label (preloaded_vlsm X seed),
          valid l (s, om)
          → ∀ (s' : state
                      (preloaded_vlsm X seed)) 
              (om' : option message),
              transition l (s, om) = (s', om')
              → valid_state_message_prop
                  (preloaded_vlsm X seed) s'
                  om'
option_valid_message_prop (preloaded_vlsm X seed) om'
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s' i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si) apply proj1 in IHHbs2.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
l: label (preloaded_vlsm (equivocator_vlsm X) seed)
Hv: valid l (s, om)
s': state (preloaded_vlsm (equivocator_vlsm X) seed)
om': option message
Ht: transition l (s, om) = (s', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
IHHbs2: option_valid_message_prop
  (preloaded_vlsm X seed) om
Hgen: ∀ (s : state (preloaded_vlsm X seed)) 
  (_om : option message),
  valid_state_message_prop
    (preloaded_vlsm X seed) s _om
  → ∀ (_s : state (preloaded_vlsm X seed)) 
      (om : option message),
      valid_state_message_prop
        (preloaded_vlsm X seed) _s om
      → ∀ l : label (preloaded_vlsm X seed),
          valid l (s, om)
          → ∀ (s' : state
                      (preloaded_vlsm X seed)) 
              (om' : option message),
              transition l (s, om) = (s', om')
              → valid_state_message_prop
                  (preloaded_vlsm X seed) s'
                  om'
option_valid_message_prop (preloaded_vlsm X seed) om'
∧ (∀ (i : nat) (si : state X),
     equivocator_state_project s' i = Some si
     → valid_state_prop (preloaded_vlsm X seed) si)

    (*
      destruction tactic for a valid equivocator transition
      transition (equivocator_vlsm X) l (s, om) = (s', om')
    *)
    destruct l as [sn | i l | i l]
    ; [inversion_clear Ht; split; [by apply option_valid_message_None |]
      ; intros
      ; destruct_equivocator_state_extend_project s sn i Hi
      ; [by apply IHHbs1 in H
      | inversion H; subst; apply initial_state_is_valid; apply Hv
      | done]
      | ..]
    ; cbn in Hv, Ht
    ; destruct_equivocator_state_project' s i si Hi Hpr; [| done | | done]
    ; destruct (transition _ _ _) as (si', _om') eqn: Hti
    ; inversion Ht; subst s' _om'; clear Ht

    (* I wish I could solve this goal, then apply the composed tactic for the remaining two goals. *)
    (* common tactic for the last two goals. *)
    ; apply IHHbs1 in Hpr as [_omi Hsi]
      ; destruct IHHbs2 as [_som Hom]
      ; specialize (Hgen _ _ Hsi _ _ Hom _ Hv _ _ Hti)
      ; split; [by eexists | | by eexists |]; intros.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project
  (equivocator_state_update s i si') i0 = 
Some si0
valid_state_prop (preloaded_vlsm X seed) si0
message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project
  (equivocator_state_extend s si') i0 = 
Some si0
valid_state_prop (preloaded_vlsm X seed) si0
    +message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project
  (equivocator_state_update s i si') i0 = 
Some si0
valid_state_prop (preloaded_vlsm X seed) si0 destruct_equivocator_state_update_project s i si' i0 Hi0 Hij.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: None = Some si0
Hi0: ¬ i0 < equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si0
message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: Some si' = Some si0
Hi0: i0 < equivocator_state_n s
Hij: i = i0
valid_state_prop (preloaded_vlsm X seed) si0
message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project s i0 = Some si0
Hi0: i0 < equivocator_state_n s
Hij: i ≠ i0
valid_state_prop (preloaded_vlsm X seed) si0
      *message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: None = Some si0
Hi0: ¬ i0 < equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si0 done.
      *message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: Some si' = Some si0
Hi0: i0 < equivocator_state_n s
Hij: i = i0
valid_state_prop (preloaded_vlsm X seed) si0 by inversion H; subst; eexists.
      *message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project s i0 = Some si0
Hi0: i0 < equivocator_state_n s
Hij: i ≠ i0
valid_state_prop (preloaded_vlsm X seed) si0 by apply IHHbs1 in H.
    +message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project
  (equivocator_state_extend s si') i0 = 
Some si0
valid_state_prop (preloaded_vlsm X seed) si0 destruct_equivocator_state_extend_project s si' i0 Hi0.message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project s i0 = Some si0
Hi0: i0 < equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si0
message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: Some si' = Some si0
Hni: ¬ i0 < equivocator_state_n s
Hi0: i0 = equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si0
message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: None = Some si0
Hni: ¬ i0 < equivocator_state_n s
Hni0: i0 ≠ equivocator_state_n s
Hi0: equivocator_state_n s < i0
valid_state_prop (preloaded_vlsm X seed) si0
      *message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: equivocator_state_project s i0 = Some si0
Hi0: i0 < equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si0 by apply IHHbs1 in H.
      *message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: Some si' = Some si0
Hni: ¬ i0 < equivocator_state_n s
Hi0: i0 = equivocator_state_n s
valid_state_prop (preloaded_vlsm X seed) si0 by inversion H; subst; eexists.
      *message: Type
X: VLSM message
seed: message → Prop
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
_om: option message
Hbs1: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s
  _om
_s: state (preloaded_vlsm (equivocator_vlsm X) seed)
om: option message
Hbs2: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) _s
  om
i: nat
l: label X
si: state X
_omi: option message
Hsi: valid_state_message_prop 
  (preloaded_vlsm X seed) si _omi
Hv: valid l (si, om)
om': option message
si': state X
Hti: transition l (si, om) = (si', om')
IHHbs1: ∀ (i : nat) (si : state X),
  equivocator_state_project s i = Some si
  → valid_state_prop (preloaded_vlsm X seed)
      si
_som: state (preloaded_vlsm X seed)
Hom: valid_state_message_prop 
  (preloaded_vlsm X seed) _som om
Hgen: valid_state_message_prop
  (preloaded_vlsm X seed) si' om'
Hi: i < equivocator_state_n s
i0: nat
si0: state X
H: None = Some si0
Hni: ¬ i0 < equivocator_state_n s
Hni0: i0 ≠ equivocator_state_n s
Hi0: equivocator_state_n s < i0
valid_state_prop (preloaded_vlsm X seed) si0 done.
Qed.

Lemma preloaded_with_equivocator_state_project_valid_state
  (seed : message -> Prop)
  (bs : state (equivocator_vlsm X))
  (Hbs : valid_state_prop (preloaded_vlsm (equivocator_vlsm X) seed) bs)
  : forall i si,
    equivocator_state_project bs i = Some si ->
    valid_state_prop (preloaded_vlsm X seed) si.message: Type
X: VLSM message
seed: message → Prop
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) bs
∀ (i : nat) (si : state X),
  equivocator_state_project bs i = Some si
  → valid_state_prop (preloaded_vlsm X seed) si
Proof.message: Type
X: VLSM message
seed: message → Prop
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) bs
∀ (i : nat) (si : state X),
  equivocator_state_project bs i = Some si
  → valid_state_prop (preloaded_vlsm X seed) si
  destruct Hbs as [om  Hbs].message: Type
X: VLSM message
seed: message → Prop
bs: state (equivocator_vlsm X)
om: option message
Hbs: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) bs
  om
∀ (i : nat) (si : state X),
  equivocator_state_project bs i = Some si
  → valid_state_prop (preloaded_vlsm X seed) si
  by apply preloaded_equivocator_state_projection_preserves_validity, proj2 in Hbs.
Qed.

Lemma preloaded_with_equivocator_state_project_valid_message
  (seed : message -> Prop)
  (om : option message)
  (Hom : option_valid_message_prop (preloaded_vlsm (equivocator_vlsm X) seed) om)
  :
  option_valid_message_prop (preloaded_vlsm X seed) om.message: Type
X: VLSM message
seed: message → Prop
om: option message
Hom: option_valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
option_valid_message_prop (preloaded_vlsm X seed) om
Proof.message: Type
X: VLSM message
seed: message → Prop
om: option message
Hom: option_valid_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) om
option_valid_message_prop (preloaded_vlsm X seed) om
  destruct Hom as [s Hm].message: Type
X: VLSM message
seed: message → Prop
om: option message
s: state (preloaded_vlsm (equivocator_vlsm X) seed)
Hm: valid_state_message_prop
  (preloaded_vlsm (equivocator_vlsm X) seed) s om
option_valid_message_prop (preloaded_vlsm X seed) om
  by apply preloaded_equivocator_state_projection_preserves_validity, proj1 in Hm.
Qed.

Lemma equivocator_state_project_valid_state
  (bs : state (equivocator_vlsm X))
  (Hbs : valid_state_prop (equivocator_vlsm X) bs)
  : forall i si,
    equivocator_state_project bs i = Some si -> valid_state_prop X si.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop (equivocator_vlsm X) bs
∀ (i : nat) (si : state X),
  equivocator_state_project bs i = Some si
  → valid_state_prop X si
Proof.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop (equivocator_vlsm X) bs
∀ (i : nat) (si : state X),
  equivocator_state_project bs i = Some si
  → valid_state_prop X si
  intros i si Hpr.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop (equivocator_vlsm X) bs
i: nat
si: state X
Hpr: equivocator_state_project bs i = Some si
valid_state_prop X si
  apply (VLSM_eq_valid_state (vlsm_is_preloaded_with_False (equivocator_vlsm X))) in Hbs.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop
  {|
    vlsm_type := equivocator_vlsm X;
    vlsm_machine :=
      preloaded_vlsm (equivocator_vlsm X)
        (λ _ : message, False)
  |} bs
i: nat
si: state X
Hpr: equivocator_state_project bs i = Some si
valid_state_prop X si
  specialize (preloaded_with_equivocator_state_project_valid_state _ _ Hbs _ _ Hpr) as Hsi.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop
  {|
    vlsm_type := equivocator_vlsm X;
    vlsm_machine :=
      preloaded_vlsm (equivocator_vlsm X)
        (λ _ : message, False)
  |} bs
i: nat
si: state X
Hpr: equivocator_state_project bs i = Some si
Hsi: valid_state_prop
  (preloaded_vlsm X (λ _ : message, False)) si
valid_state_prop X si
  apply (VLSM_eq_valid_state (vlsm_is_preloaded_with_False X)) in Hsi.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: valid_state_prop
  {|
    vlsm_type := equivocator_vlsm X;
    vlsm_machine :=
      preloaded_vlsm (equivocator_vlsm X)
        (λ _ : message, False)
  |} bs
i: nat
si: state X
Hpr: equivocator_state_project bs i = Some si
Hsi: valid_state_prop
  {| vlsm_type := X; vlsm_machine := X |} si
valid_state_prop X si
  by destruct X.
Qed.

Lemma equivocator_state_project_valid_message
  (om : option message)
  (Hom : option_valid_message_prop (equivocator_vlsm X) om)
  :
  option_valid_message_prop X om.message: Type
X: VLSM message
om: option message
Hom: option_valid_message_prop 
  (equivocator_vlsm X) om
option_valid_message_prop X om
Proof.message: Type
X: VLSM message
om: option message
Hom: option_valid_message_prop 
  (equivocator_vlsm X) om
option_valid_message_prop X om
  destruct om as [m |]; [| by apply option_valid_message_None].message: Type
X: VLSM message
m: message
Hom: option_valid_message_prop 
  (equivocator_vlsm X) 
  (Some m)
option_valid_message_prop X (Some m)
  specialize (vlsm_is_preloaded_with_False_initial_message (equivocator_vlsm X)) as Hinit.message: Type
X: VLSM message
m: message
Hom: option_valid_message_prop 
  (equivocator_vlsm X) 
  (Some m)
Hinit: strong_embedding_initial_message_preservation
  (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
option_valid_message_prop X (Some m)
  apply (VLSM_incl_valid_message (proj1 (vlsm_is_preloaded_with_False (equivocator_vlsm X))))
    in Hom; [| done].message: Type
X: VLSM message
m: message
Hom: valid_message_prop
  {|
    vlsm_type :=
      {|
        vlsm_type := equivocator_vlsm X;
        vlsm_machine := equivocator_vlsm X
      |};
    vlsm_machine :=
      {|
        vlsm_type := equivocator_vlsm X;
        vlsm_machine :=
          preloaded_vlsm 
            (equivocator_vlsm X)
            (λ _ : message, False)
      |}
  |} m
Hinit: strong_embedding_initial_message_preservation
  (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
option_valid_message_prop X (Some m)
  apply preloaded_with_equivocator_state_project_valid_message in Hom.message: Type
X: VLSM message
m: message
Hom: option_valid_message_prop
  (preloaded_vlsm X (λ _ : message, False))
  (Some m)
Hinit: strong_embedding_initial_message_preservation
  (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
option_valid_message_prop X (Some m)
  specialize (vlsm_is_preloaded_with_False_initial_message_rev X) as Hinit_rev.message: Type
X: VLSM message
m: message
Hom: option_valid_message_prop
  (preloaded_vlsm X (λ _ : message, False))
  (Some m)
Hinit: strong_embedding_initial_message_preservation
  (equivocator_vlsm X)
  (preloaded_vlsm (equivocator_vlsm X)
     (λ _ : message, False))
Hinit_rev: strong_embedding_initial_message_preservation
  (preloaded_vlsm X (λ _ : message, False))
  X
option_valid_message_prop X (Some m)
  by apply (VLSM_incl_valid_message (proj2 (vlsm_is_preloaded_with_False X))) in Hom
  ; destruct X.
Qed.

All components of valid states of the preloaded_with_all_messages_vlsm corresponding to an equivocator_vlsm are also valid for the preloaded_with_all_messages_vlsm corresponding to the original machine.

Lemma preloaded_equivocator_state_project_valid_state
  (bs : state (equivocator_vlsm X))
  (Hbs : constrained_state_prop (equivocator_vlsm X) bs)
  : forall i si,
    equivocator_state_project bs i = Some si ->
      constrained_state_prop X si.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: constrained_state_prop (equivocator_vlsm X) bs
∀ (i : nat) (si : state X),
  equivocator_state_project bs i = Some si
  → constrained_state_prop X si
Proof.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: constrained_state_prop (equivocator_vlsm X) bs
∀ (i : nat) (si : state X),
  equivocator_state_project bs i = Some si
  → constrained_state_prop X si
  intros i si Hpr.message: Type
X: VLSM message
bs: state (equivocator_vlsm X)
Hbs: constrained_state_prop (equivocator_vlsm X) bs
i: nat
si: state X
Hpr: equivocator_state_project bs i = Some si
constrained_state_prop X si
  by apply (preloaded_with_equivocator_state_project_valid_state _ _ Hbs _ _ Hpr).
Qed.

Next couple of lemmas characterize the projections of a equivocator_state after taking a transition in terms of the preceding state.

These are simpler version of the results concerning the projection of states from the composition of equivocators over equivocation_descriptors.

These results are used for characterizing the projection of the destination of a transition_item in an equivocator trace in equivocator_transition_item_project_proper_characterization.

Lemma new_machine_label_equivocator_transition_size
  {sn s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (Spawn sn) (s, oin) = (s', oout))
  : equivocator_state_n s' = S (equivocator_state_n s).message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (Spawn sn) (s, oin) = (s', oout)
equivocator_state_n s' = S (equivocator_state_n s)
Proof.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (Spawn sn) (s, oin) = (s', oout)
equivocator_state_n s' = S (equivocator_state_n s)
  inversion_clear Ht.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
equivocator_state_n (equivocator_state_extend s sn) =
S (equivocator_state_n s)
  by apply equivocator_state_extend_size.
Qed.

Lemma existing_true_label_equivocator_transition_size
  {ieqvi li s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (ForkWith ieqvi li) (s, oin) = (s', oout))
  si
  (Hv : equivocator_state_project s ieqvi = Some si)
  : equivocator_state_n s' = S (equivocator_state_n s).message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ForkWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = S (equivocator_state_n s)
Proof.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ForkWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = S (equivocator_state_n s)
  cbn in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: match equivocator_state_project s ieqvi with
| Some si =>
    let (si', om') := transition li (si, oin) in
    (equivocator_state_extend s si', om')
| None => (s, oin)
end = (s', oout)
si: state X
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = S (equivocator_state_n s)
  rewrite Hv in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_extend s si', om')) =
(s', oout)
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = S (equivocator_state_n s)
  destruct (transition _ _ _).message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, s0: state X
o: option message
Ht: (equivocator_state_extend s s0, o) = (s', oout)
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = S (equivocator_state_n s)
  inversion Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, s0: state X
o: option message
Ht: (equivocator_state_extend s s0, o) = (s', oout)
Hv: equivocator_state_project s ieqvi = Some si
H0: equivocator_state_extend s s0 = s'
H1: o = oout
equivocator_state_n (equivocator_state_extend s s0) =
S (equivocator_state_n s) subst.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, s0: state X
Ht: (equivocator_state_extend s s0, oout) =
(equivocator_state_extend s s0, oout)
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n (equivocator_state_extend s s0) =
S (equivocator_state_n s)
  by apply equivocator_state_extend_size.
Qed.

Lemma existing_false_label_equivocator_transition_size
  {ieqvi li s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (ContinueWith ieqvi li) (s, oin) = (s', oout))
  si
  (Hv : equivocator_state_project s ieqvi = Some si)
  : equivocator_state_n s' = equivocator_state_n s.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ContinueWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = equivocator_state_n s
Proof.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ContinueWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = equivocator_state_n s
  cbn in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: match equivocator_state_project s ieqvi with
| Some si =>
    let (si', om') := transition li (si, oin) in
    (equivocator_state_update s ieqvi si', om')
| None => (s, oin)
end = (s', oout)
si: state X
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = equivocator_state_n s
  rewrite Hv in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_update s ieqvi si', om')) =
(s', oout)
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = equivocator_state_n s
  destruct (transition _ _ _).message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, s0: state X
o: option message
Ht: (equivocator_state_update s ieqvi s0, o) =
(s', oout)
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n s' = equivocator_state_n s
  inversion Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, s0: state X
o: option message
Ht: (equivocator_state_update s ieqvi s0, o) =
(s', oout)
Hv: equivocator_state_project s ieqvi = Some si
H0: equivocator_state_update s ieqvi s0 = s'
H1: o = oout
equivocator_state_n
  (equivocator_state_update s ieqvi s0) =
equivocator_state_n s subst.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, s0: state X
Ht: (equivocator_state_update s ieqvi s0, oout) =
(equivocator_state_update s ieqvi s0, oout)
Hv: equivocator_state_project s ieqvi = Some si
equivocator_state_n
  (equivocator_state_update s ieqvi s0) =
equivocator_state_n s
  by equivocator_state_update_simpl.
Qed.

Lemma new_machine_label_equivocator_state_project_last
  {sn s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (Spawn sn) (s, oin) = (s', oout))
  : equivocator_state_descriptor_project s' (Existing (equivocator_state_n s)) =
    equivocator_state_descriptor_project s (NewMachine sn).message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (Spawn sn) (s, oin) = (s', oout)
equivocator_state_descriptor_project s'
  (Existing (equivocator_state_n s)) =
equivocator_state_descriptor_project s (NewMachine sn)
Proof.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (Spawn sn) (s, oin) = (s', oout)
equivocator_state_descriptor_project s'
  (Existing (equivocator_state_n s)) =
equivocator_state_descriptor_project s (NewMachine sn)
  inversion_clear Ht.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
equivocator_state_descriptor_project
  (equivocator_state_extend s sn)
  (Existing (equivocator_state_n s)) =
equivocator_state_descriptor_project s (NewMachine sn) simpl.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
default (equivocator_state_s s 0)
  (equivocator_state_project
     (equivocator_state_extend s sn)
     (equivocator_state_n s)) = sn
  by destruct_equivocator_state_extend_project s sn (equivocator_state_n s) Hi;
    [lia | | lia].
Qed.

Lemma new_machine_label_equivocator_state_project_not_last
  {sn s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (Spawn sn) (s, oin) = (s', oout))
  ni
  (Hni : ni < equivocator_state_n s)
  : equivocator_state_descriptor_project s' (Existing ni) =
    equivocator_state_descriptor_project s (Existing ni).message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (Spawn sn) (s, oin) = (s', oout)
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
Proof.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (Spawn sn) (s, oin) = (s', oout)
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  subst.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (Spawn sn) (s, oin) = (s', oout)
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni) inversion_clear Ht.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project
  (equivocator_state_extend s sn) (Existing ni) =
equivocator_state_descriptor_project s (Existing ni) simpl.message: Type
X: VLSM message
sn: state X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
ni: nat
Hni: ni < equivocator_state_n s
default (equivocator_state_s s 0)
  (equivocator_state_project
     (equivocator_state_extend s sn) ni) =
default (equivocator_state_zero s)
  (equivocator_state_project s ni)
  by destruct_equivocator_state_extend_project s sn ni Hi; [| lia..].
Qed.

Lemma existing_true_label_equivocator_state_project_not_last
  {ieqvi li s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (ForkWith ieqvi li) (s, oin) = (s', oout))
  si
  (Hsi : equivocator_state_project s ieqvi = Some si)
  ni
  (Hni : ni < equivocator_state_n s)
  : equivocator_state_descriptor_project s' (Existing ni)
  = equivocator_state_descriptor_project s (Existing ni).message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ForkWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
Proof.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ForkWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  cbn in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: match equivocator_state_project s ieqvi with
| Some si =>
    let (si', om') := transition li (si, oin) in
    (equivocator_state_extend s si', om')
| None => (s, oin)
end = (s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  rewrite Hsi in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_extend s si', om')) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  destruct (transition _ _ _) as (si', _om') eqn: Hti.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, si': state X
_om': option message
Hti: transition li (si, oin) = (si', _om')
Ht: (equivocator_state_extend s si', _om') =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  inversion Ht; subst s' _om'.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Ht: (equivocator_state_extend s si', oout) =
(equivocator_state_extend s si', oout)
Hti: transition li (si, oin) = (si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project
  (equivocator_state_extend s si') (Existing ni) =
equivocator_state_descriptor_project s (Existing ni) clear Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hti: transition li (si, oin) = (si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
equivocator_state_descriptor_project
  (equivocator_state_extend s si') (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  simpl.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hti: transition li (si, oin) = (si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
default (equivocator_state_s s 0)
  (equivocator_state_project
     (equivocator_state_extend s si') ni) =
default (equivocator_state_zero s)
  (equivocator_state_project s ni)
  by destruct_equivocator_state_extend_project s si' ni Hni'; [| lia..].
Qed.

Lemma existing_true_label_equivocator_state_project_last
  {ieqvi li s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (ForkWith ieqvi li) (s, oin) = (s', oout))
  si
  (Hsi : equivocator_state_project s ieqvi = Some si)
  si' _oout
  (Hti : transition X li (si, oin) = (si', _oout))
  : _oout = oout /\
    equivocator_state_descriptor_project s' (Existing (equivocator_state_n s)) = si'.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ForkWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing (equivocator_state_n s)) = si'
Proof.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ForkWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing (equivocator_state_n s)) = si'
  cbn in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: match equivocator_state_project s ieqvi with
| Some si =>
    let (si', om') := transition li (si, oin) in
    (equivocator_state_extend s si', om')
| None => (s, oin)
end = (s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing (equivocator_state_n s)) = si'
  rewrite Hsi in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_extend s si', om')) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing (equivocator_state_n s)) = si'
  simpl in Hti.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_extend s si', om')) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing (equivocator_state_n s)) = si' rewrite Hti in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, si': state X
_oout: option message
Ht: (equivocator_state_extend s si', _oout) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing (equivocator_state_n s)) = si'
  inversion Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, si': state X
_oout: option message
Ht: (equivocator_state_extend s si', _oout) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', _oout)
H0: equivocator_state_extend s si' = s'
H1: _oout = oout
oout = oout
∧ equivocator_state_descriptor_project
    (equivocator_state_extend s si')
    (Existing (equivocator_state_n s)) = si' subst.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Ht: (equivocator_state_extend s si', oout) =
(equivocator_state_extend s si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', oout)
oout = oout
∧ equivocator_state_descriptor_project
    (equivocator_state_extend s si')
    (Existing (equivocator_state_n s)) = si' clear Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', oout)
oout = oout
∧ equivocator_state_descriptor_project
    (equivocator_state_extend s si')
    (Existing (equivocator_state_n s)) = si'
  by cbn; rewrite equivocator_state_extend_project_2.
Qed.

Lemma existing_false_label_equivocator_state_project_not_same
  {ieqvi li s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (ContinueWith ieqvi li) (s, oin) = (s', oout))
  si
  (Hsi : equivocator_state_project s ieqvi = Some si)
  ni
  (Hni : ni < equivocator_state_n s)
  (Hnieqvi : ieqvi <> ni)
  : equivocator_state_descriptor_project s' (Existing ni)
  = equivocator_state_descriptor_project s (Existing ni).message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ContinueWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
Proof.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ContinueWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  cbn in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: match equivocator_state_project s ieqvi with
| Some si =>
    let (si', om') := transition li (si, oin) in
    (equivocator_state_update s ieqvi si', om')
| None => (s, oin)
end = (s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni) rewrite Hsi in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_update s ieqvi si', om')) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  destruct (transition _ _ _) as (si', _om') eqn: Hti.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, si': state X
_om': option message
Hti: transition li (si, oin) = (si', _om')
Ht: (equivocator_state_update s ieqvi si', _om') =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
equivocator_state_descriptor_project s' (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  inversion Ht; subst s' _om'.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Ht: (equivocator_state_update s ieqvi si', oout) =
(equivocator_state_update s ieqvi si', oout)
Hti: transition li (si, oin) = (si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
equivocator_state_descriptor_project
  (equivocator_state_update s ieqvi si') (Existing ni) =
equivocator_state_descriptor_project s (Existing ni) clear Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hti: transition li (si, oin) = (si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
equivocator_state_descriptor_project
  (equivocator_state_update s ieqvi si') (Existing ni) =
equivocator_state_descriptor_project s (Existing ni)
  simpl.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hti: transition li (si, oin) = (si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
default
  (if decide (ieqvi = 0)
   then si'
   else equivocator_state_s s 0)
  (equivocator_state_project
     (equivocator_state_update s ieqvi si') ni) =
default (equivocator_state_zero s)
  (equivocator_state_project s ni)
  destruct_equivocator_state_update_project s ieqvi si' ni Hni' Hini; [lia.. |].message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hti: transition li (si, oin) = (si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
ni: nat
Hni: ni < equivocator_state_n s
Hnieqvi: ieqvi ≠ ni
Hni': ni < equivocator_state_n s
Hini: ieqvi ≠ ni
default
  (if decide (ieqvi = 0)
   then si'
   else equivocator_state_s s 0)
  (equivocator_state_project s ni) =
default (equivocator_state_zero s)
  (equivocator_state_project s ni)
  by destruct_equivocator_state_project s ni sni Hni''; [| lia].
Qed.

Lemma existing_false_label_equivocator_state_project_same
  {ieqvi li s oin s' oout}
  (Ht : transition (equivocator_vlsm X) (ContinueWith ieqvi li) (s, oin) = (s', oout))
  si
  (Hsi : equivocator_state_project s ieqvi = Some si)
  si' _oout
  (Hti : transition X li (si, oin) = (si', _oout))
  : _oout = oout /\
    equivocator_state_descriptor_project s' (Existing ieqvi) = si'.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ContinueWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing ieqvi) = si'
Proof.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: transition (ContinueWith ieqvi li) (s, oin) =
(s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing ieqvi) = si'
  cbn in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
Ht: match equivocator_state_project s ieqvi with
| Some si =>
    let (si', om') := transition li (si, oin) in
    (equivocator_state_update s ieqvi si', om')
| None => (s, oin)
end = (s', oout)
si: state X
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing ieqvi) = si' rewrite Hsi in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_update s ieqvi si', om')) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing ieqvi) = si'
  simpl in Hti.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si: state X
Ht: (let (si', om') := transition li (si, oin) in
 (equivocator_state_update s ieqvi si', om')) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
si': state X
_oout: option message
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing ieqvi) = si' rewrite Hti in Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin: option message
s': state (equivocator_vlsm X)
oout: option message
si, si': state X
_oout: option message
Ht: (equivocator_state_update s ieqvi si', _oout) =
(s', oout)
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', _oout)
_oout = oout
∧ equivocator_state_descriptor_project s'
    (Existing ieqvi) = si'
  inversion Ht; subst s' _oout.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Ht: (equivocator_state_update s ieqvi si', oout) =
(equivocator_state_update s ieqvi si', oout)
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', oout)
oout = oout
∧ equivocator_state_descriptor_project
    (equivocator_state_update s ieqvi si')
    (Existing ieqvi) = si' clear Ht.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', oout)
oout = oout
∧ equivocator_state_descriptor_project
    (equivocator_state_update s ieqvi si')
    (Existing ieqvi) = si'
  split; [done |].message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', oout)
equivocator_state_descriptor_project
  (equivocator_state_update s ieqvi si')
  (Existing ieqvi) = si'
  simpl.message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', oout)
default
  (if decide (ieqvi = 0)
   then si'
   else equivocator_state_s s 0)
  (equivocator_state_project
     (equivocator_state_update s ieqvi si') ieqvi) =
si'
  rewrite equivocator_state_update_project_eq; [done | | done].message: Type
X: VLSM message
ieqvi: nat
li: label X
s: state (equivocator_vlsm X)
oin, oout: option message
si, si': state X
Hsi: equivocator_state_project s ieqvi = Some si
Hti: transition li (si, oin) = (si', oout)
ieqvi < equivocator_state_n s
  by apply equivocator_state_project_Some_rev in Hsi.
Qed.

End sec_equivocator_vlsm_valid_state_projections.

Arguments NewMachine {_ _} _ : assert.
Arguments Existing {_ _} _ : assert.
Arguments equivocator_label_descriptor {_ _} _ : assert.
Arguments equivocator_state_descriptor_project {_ _} _ _ : assert.