From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From Coq Require Import FunctionalExtensionality.
From Coq Require Import ZArith.Znumtheory.
From stdpp Require Import prelude.
From VLSM.Lib Require Import Preamble StdppExtras FinSuppFn NatExtras ListExtras.[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
[Loading ML file equations_plugin.cmxs (using legacy method) ... done]
From VLSM.Core Require Import VLSM PreloadedVLSM ConstrainedVLSM Composition.
From VLSM.Core Require Import VLSMProjections ProjectionTraces.
From VLSM.Examples Require Import Multiply.

Tutorial: Primes Composition of VLSMs

This module demonstrates some advanced concepts in the VLSM framework.

We generalize the VLSMs defined in the module Multiply as a radix VLSM parameterized on a multiplier and study the composition of a family of such VLSMs.

We then construct the VLSM composition consisting of a component for each prime number, characterize valid messages, and show that any component in the composition is a validator.

#[local] Open Scope Z_scope.

Section sec_radix_vlsm.

We parameterize a radix VLSM on an integer multiplier greater than one.

Context
 (multiplier : Z)
 (multiplier_gt_1 : multiplier > 1)
 .

Definition of the Radix VLSM

The Radix VLSM will share the type and transition validity predicate of the multiplying VLSM and differ only by the fact that the only initial message is the multiplier parameter, and that it outputs its input multiplied by the multiplier.

Definition radix_transition
  (l : multiplying_label) (st : multiplying_state) (om : option multiplying_message)
  : multiplying_state * option multiplying_message :=
  match om with
  | Some j  => (st - j, Some (multiplier * j))
  | None    => (st, None)
  end.

We must also provide a proof that the intial state type is inhabited as the set of initial states is non-empty.

An intermediate representation for the VLSM is required. It uses the previously defined specifications.

Definition radix_machine : VLSMMachine multiplying_type :=
{|
  initial_state_prop := multiplying_initial_state_prop;
  initial_message_prop := fun (ms : multiplying_message) => ms = multiplier;
  s0 := multiplying_initial_state_type_inhabited;
  transition := fun l '(st, om) => radix_transition l st om;
  valid := fun l '(st, om) => multiplying_valid l st om;
|}.

The definition of the Radix VLSM.

Definition radix_vlsm : VLSM multiplying_message :=
{|
  vlsm_type := multiplying_type;
  vlsm_machine := radix_machine;
|}.

To improve readability, we explicitly define radix_label as the value of the unit type.

Definition radix_label : label multiplying_type := ().

Radix VLSM properties

Constrained messages are positives divisible by the multiplier

Lemma radix_constrained_messages_left :
  forall (m : multiplying_message),
    constrained_message_prop radix_vlsm m ->
    exists (j : Z), m = multiplier * j /\ j > 1.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  constrained_message_prop radix_vlsm m
  → ∃ j : Z, m = multiplier * j ∧ j > 1
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  constrained_message_prop radix_vlsm m
  → ∃ j : Z, m = multiplier * j ∧ j > 1
  intros m ([s []] & [] & s' & (_ & _ & []) & Ht).multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
s: state
  (preloaded_with_all_messages_vlsm radix_vlsm)
m0: multiplying_message
s': state
  (preloaded_with_all_messages_vlsm radix_vlsm)
H: 2 ≤ m0
H0: m0 ≤ s
Ht: transition () (s, Some m0) = (s', Some m)
∃ j : Z, m = multiplier * j ∧ j > 1
  inversion Ht; subst.multiplier: Z
multiplier_gt_1: multiplier > 1
s: state
  (preloaded_with_all_messages_vlsm radix_vlsm)
m0: multiplying_message
H: 2 ≤ m0
H0: m0 ≤ s
Ht: transition () (s, Some m0) =
(s - m0, Some (multiplier * m0))
∃ j : Z, multiplier * m0 = multiplier * j ∧ j > 1
  by eexists; split; [done | lia].
Qed.

Lemma radix_constrained_messages_right :
  forall (m : multiplying_message),
    (exists (j : Z), m = multiplier * j) -> m > multiplier ->
    constrained_message_prop radix_vlsm m.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  (∃ j : Z, m = multiplier * j)
  → m > multiplier
    → constrained_message_prop radix_vlsm m
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  (∃ j : Z, m = multiplier * j)
  → m > multiplier
    → constrained_message_prop radix_vlsm m
  intros m (j & Hj) Hmgt0.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
constrained_message_prop radix_vlsm m
  unfold constrained_message_prop_direct, can_emit.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
constrained_message_prop radix_vlsm m
  exists (j, Some j), radix_label, 0.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
input_valid_transition
  (preloaded_with_all_messages_vlsm radix_vlsm)
  radix_label (j, Some j) (0, Some m)
  repeat split.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
valid_state_prop
  (preloaded_with_all_messages_vlsm radix_vlsm) j
multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
option_valid_message_prop
  (preloaded_with_all_messages_vlsm radix_vlsm)
  (Some j)
multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
2 ≤ j
multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
j ≤ j
multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
transition radix_label (j, Some j) = (0, Some m)
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
valid_state_prop
  (preloaded_with_all_messages_vlsm radix_vlsm) j by apply initial_state_is_valid; cbn; red; nia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
option_valid_message_prop
  (preloaded_with_all_messages_vlsm radix_vlsm)
  (Some j) by apply any_message_is_valid_in_preloaded.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
2 ≤ j by nia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
j ≤ j by lia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
j: Z
Hj: m = multiplier * j
Hmgt0: m > multiplier
transition radix_label (j, Some j) = (0, Some m) by cbn; do 2 f_equal; lia.
Qed.

Lemma radix_constrained_messages :
  forall (m : multiplying_message),
    constrained_message_prop radix_vlsm m <-> (exists (j : Z), m = multiplier * j /\ j > 1).multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  constrained_message_prop radix_vlsm m
  ↔ (∃ j : Z, m = multiplier * j ∧ j > 1)
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  constrained_message_prop radix_vlsm m
  ↔ (∃ j : Z, m = multiplier * j ∧ j > 1)
  split.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
constrained_message_prop radix_vlsm m
→ ∃ j : Z, m = multiplier * j ∧ j > 1
multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
(∃ j : Z, m = multiplier * j ∧ j > 1)
→ constrained_message_prop radix_vlsm m
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
constrained_message_prop radix_vlsm m
→ ∃ j : Z, m = multiplier * j ∧ j > 1 by apply radix_constrained_messages_left.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
(∃ j : Z, m = multiplier * j ∧ j > 1)
→ constrained_message_prop radix_vlsm m by intros [? []]; apply radix_constrained_messages_right; [exists x | nia].
Qed.

Constrained states property

Lemma radix_constrained_states_right :
  forall (st : multiplying_state),
    constrained_state_prop radix_vlsm st -> st >= 0.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ st : multiplying_state,
  constrained_state_prop radix_vlsm st → st >= 0
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ st : multiplying_state,
  constrained_state_prop radix_vlsm st → st >= 0
  induction 1 using valid_state_prop_ind.multiplier: Z
multiplier_gt_1: multiplier > 1
s: state
  (preloaded_with_all_messages_vlsm radix_vlsm)
Hs: initial_state_prop s
s >= 0
multiplier: Z
multiplier_gt_1: multiplier > 1
s': state
  (preloaded_with_all_messages_vlsm radix_vlsm)
l: label
  (preloaded_with_all_messages_vlsm radix_vlsm)
om, om': option multiplying_message
s: state
  (preloaded_with_all_messages_vlsm radix_vlsm)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm radix_vlsm) l
  (s, om) (s', om')
IHvalid_state_prop: s >= 0
s' >= 0
  -multiplier: Z
multiplier_gt_1: multiplier > 1
s: state
  (preloaded_with_all_messages_vlsm radix_vlsm)
Hs: initial_state_prop s
s >= 0 by cbn in Hs; red in Hs; lia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
s': state
  (preloaded_with_all_messages_vlsm radix_vlsm)
l: label
  (preloaded_with_all_messages_vlsm radix_vlsm)
om, om': option multiplying_message
s: state
  (preloaded_with_all_messages_vlsm radix_vlsm)
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm radix_vlsm) l
  (s, om) (s', om')
IHvalid_state_prop: s >= 0
s' >= 0 destruct l, om, Ht as [(Hs & _ & []) Ht].multiplier: Z
multiplier_gt_1: multiplier > 1
s': state
  (preloaded_with_all_messages_vlsm radix_vlsm)
m: multiplying_message
om': option multiplying_message
s: state
  (preloaded_with_all_messages_vlsm radix_vlsm)
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm radix_vlsm) s
H: 2 ≤ m
H0: m ≤ s
Ht: transition () (s, Some m) = (s', om')
IHvalid_state_prop: s >= 0
s' >= 0
    by inversion Ht; subst; cbn in *; lia.
Qed.

Lemma radix_constrained_states_left :
  forall (st : multiplying_state),
    st >= 0 -> constrained_state_prop radix_vlsm st.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ st : multiplying_state,
  st >= 0 → constrained_state_prop radix_vlsm st
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ st : multiplying_state,
  st >= 0 → constrained_state_prop radix_vlsm st
  intros st Hst.multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
Hst: st >= 0
constrained_state_prop radix_vlsm st
  apply input_valid_transition_destination
    with (l := radix_label) (s := st + 2) (om := Some 2) (om' := Some (2 * multiplier)).multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
Hst: st >= 0
input_valid_transition
  (preloaded_with_all_messages_vlsm radix_vlsm)
  radix_label (st + 2, Some 2)
  (st, Some (2 * multiplier))
  repeat split; [| | by lia.. | by cbn; do 2 f_equal; lia].multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
Hst: st >= 0
valid_state_prop
  (preloaded_with_all_messages_vlsm radix_vlsm)
  (st + 2)
multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
Hst: st >= 0
option_valid_message_prop
  (preloaded_with_all_messages_vlsm radix_vlsm)
  (Some 2)
  -multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
Hst: st >= 0
valid_state_prop
  (preloaded_with_all_messages_vlsm radix_vlsm)
  (st + 2) by apply initial_state_is_valid; cbn; red; lia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
Hst: st >= 0
option_valid_message_prop
  (preloaded_with_all_messages_vlsm radix_vlsm)
  (Some 2) by apply any_message_is_valid_in_preloaded.
Qed.

Lemma radix_constrained_states :
  forall (st : multiplying_state),
    constrained_state_prop radix_vlsm st <-> st >= 0.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ st : multiplying_state,
  constrained_state_prop radix_vlsm st ↔ st >= 0
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ st : multiplying_state,
  constrained_state_prop radix_vlsm st ↔ st >= 0
  split.multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
constrained_state_prop radix_vlsm st → st >= 0
multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
st >= 0 → constrained_state_prop radix_vlsm st
  -multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
constrained_state_prop radix_vlsm st → st >= 0 by apply radix_constrained_states_right.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
st: multiplying_state
st >= 0 → constrained_state_prop radix_vlsm st by apply radix_constrained_states_left.
Qed.

Positive powers of the multiplier are valid messages

Lemma radix_valid_messages_powers_of_mult_right :
  forall (m : multiplying_message),
    valid_message_prop radix_vlsm m ->
    exists p : Z, p >= 1 /\ m = multiplier ^ p.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  valid_message_prop radix_vlsm m
  → ∃ p : Z, p >= 1 ∧ m = multiplier ^ p
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  valid_message_prop radix_vlsm m
  → ∃ p : Z, p >= 1 ∧ m = multiplier ^ p
  intros m [s Hvsm].multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
s: state radix_vlsm
Hvsm: valid_state_message_prop radix_vlsm s (Some m)
∃ p : Z, p >= 1 ∧ m = multiplier ^ p
  assert (Hom : is_Some (Some m)) by (eexists; done).multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
s: state radix_vlsm
Hvsm: valid_state_message_prop radix_vlsm s (Some m)
Hom: is_Some (Some m)
∃ p : Z, p >= 1 ∧ m = multiplier ^ p
  replace m with (is_Some_proj Hom) by done.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
s: state radix_vlsm
Hvsm: valid_state_message_prop radix_vlsm s (Some m)
Hom: is_Some (Some m)
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
  revert Hvsm Hom; generalize (Some m) as om; intros.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
s: state radix_vlsm
om: option multiplying_message
Hvsm: valid_state_message_prop radix_vlsm s om
Hom: is_Some om
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
  clear m; induction Hvsm using valid_state_message_prop_ind.multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop radix_vlsm om
Hom: is_Some om
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
om: option multiplying_message
Hvsm2: valid_state_message_prop radix_vlsm _s om
l: label radix_vlsm
Hv: valid l (s, om)
s': state radix_vlsm
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
  -multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop radix_vlsm om
Hom: is_Some om
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p unfold option_initial_message_prop, from_option in Hom; cbn in Hom.multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop radix_vlsm om
Hom: is_Some om
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
    destruct Hom as [m ->]; cbn in *.multiplier: Z
multiplier_gt_1: multiplier > 1
s: multiplying_state
Hs: multiplying_initial_state_prop s
m: multiplying_message
Hom0: m = multiplier
∃ p : Z, p >= 1 ∧ m = multiplier ^ p
    by exists 1; split; [lia | f_equal; lia].
  -multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
om: option multiplying_message
Hvsm2: valid_state_message_prop radix_vlsm _s om
l: label radix_vlsm
Hv: valid l (s, om)
s': state radix_vlsm
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p destruct om as [m |]; [| done].multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
m: multiplying_message
Hvsm2: valid_state_message_prop radix_vlsm _s
  (Some m)
l: label radix_vlsm
Hv: valid l (s, Some m)
s': state radix_vlsm
om': option multiplying_message
Ht: transition l (s, Some m) = (s', om')
Hom: is_Some om'
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some (Some m),
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
    unshelve edestruct IHHvsm2 as [x Hx]; [done |].multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
m: multiplying_message
Hvsm2: valid_state_message_prop radix_vlsm _s
  (Some m)
l: label radix_vlsm
Hv: valid l (s, Some m)
s': state radix_vlsm
om': option multiplying_message
Ht: transition l (s, Some m) = (s', om')
Hom: is_Some om'
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some (Some m),
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
x: Z
Hx: x >= 1
∧ is_Some_proj
    (ex_intro
       (λ x : multiplying_message,
          Some m = Some x) m eq_refl) =
  multiplier ^ x
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
    inversion Ht; subst; clear Ht.multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
m: multiplying_message
Hvsm2: valid_state_message_prop radix_vlsm _s
  (Some m)
l: label radix_vlsm
Hv: valid l (s, Some m)
Hom: is_Some (Some (multiplier * m))
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some (Some m),
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
x: Z
Hx: x >= 1
∧ is_Some_proj
    (ex_intro
       (λ x : multiplying_message,
          Some m = Some x) m eq_refl) =
  multiplier ^ x
∃ p : Z, p >= 1 ∧ is_Some_proj Hom = multiplier ^ p
    cbn in Hx |- *; destruct Hx as [Hgeq1 ->].multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
x: Z
Hvsm2: valid_state_message_prop radix_vlsm _s
  (Some (multiplier ^ x))
l: label radix_vlsm
Hom: is_Some (Some (multiplier * multiplier ^ x))
Hv: valid l (s, Some (multiplier ^ x))
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some (Some (multiplier ^ x)),
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
Hgeq1: x >= 1
∃ p : Z,
  p >= 1
  ∧ multiplier * multiplier ^ x = multiplier ^ p
    exists (x + 1).multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
x: Z
Hvsm2: valid_state_message_prop radix_vlsm _s
  (Some (multiplier ^ x))
l: label radix_vlsm
Hom: is_Some (Some (multiplier * multiplier ^ x))
Hv: valid l (s, Some (multiplier ^ x))
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some (Some (multiplier ^ x)),
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
Hgeq1: x >= 1
x + 1 >= 1
∧ multiplier * multiplier ^ x = multiplier ^ (x + 1)
    split; [by lia |].multiplier: Z
multiplier_gt_1: multiplier > 1
s: state radix_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_vlsm s _om
_s: state radix_vlsm
x: Z
Hvsm2: valid_state_message_prop radix_vlsm _s
  (Some (multiplier ^ x))
l: label radix_vlsm
Hom: is_Some (Some (multiplier * multiplier ^ x))
Hv: valid l (s, Some (multiplier ^ x))
IHHvsm1: ∀ Hom : is_Some _om,
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
IHHvsm2: ∀ Hom : is_Some (Some (multiplier ^ x)),
  ∃ p : Z,
    p >= 1
    ∧ is_Some_proj Hom = multiplier ^ p
Hgeq1: x >= 1
multiplier * multiplier ^ x = multiplier ^ (x + 1)
    by rewrite <- Z.pow_succ_r; [| lia].
Qed.

Lemma radix_valid_messages_powers_of_mult_left :
  forall (p : Z),
    p >= 1 -> valid_message_prop radix_vlsm (multiplier ^ p).multiplier: Z
multiplier_gt_1: multiplier > 1
∀ p : Z,
  p >= 1
  → valid_message_prop radix_vlsm (multiplier ^ p)
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ p : Z,
  p >= 1
  → valid_message_prop radix_vlsm (multiplier ^ p)
  intros p Hp.multiplier: Z
multiplier_gt_1: multiplier > 1
p: Z
Hp: p >= 1
valid_message_prop radix_vlsm (multiplier ^ p)
  assert (Hle : 0 <= p - 1) by lia.multiplier: Z
multiplier_gt_1: multiplier > 1
p: Z
Hp: p >= 1
Hle: 0 ≤ p - 1
valid_message_prop radix_vlsm (multiplier ^ p)
  replace p with (p - 1 + 1) by lia.multiplier: Z
multiplier_gt_1: multiplier > 1
p: Z
Hp: p >= 1
Hle: 0 ≤ p - 1
valid_message_prop radix_vlsm
  (multiplier ^ (p - 1 + 1))
  remember (p - 1) as x.multiplier: Z
multiplier_gt_1: multiplier > 1
p: Z
Hp: p >= 1
x: Z
Heqx: x = p - 1
Hle: 0 ≤ x
valid_message_prop radix_vlsm (multiplier ^ (x + 1))
  clear p Hp Heqx.multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hle: 0 ≤ x
valid_message_prop radix_vlsm (multiplier ^ (x + 1))
  revert x Hle.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ x : Z,
  0 ≤ x
  → valid_message_prop radix_vlsm
      (multiplier ^ (x + 1))
  apply natlike_ind; [by apply initial_message_is_valid; cbn; lia |].multiplier: Z
multiplier_gt_1: multiplier > 1
∀ x : Z,
  0 ≤ x
  → valid_message_prop radix_vlsm
      (multiplier ^ (x + 1))
    → valid_message_prop radix_vlsm
        (multiplier ^ (Z.succ x + 1))
  intros x Hxgt0 Hindh.multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
valid_message_prop radix_vlsm
  (multiplier ^ (Z.succ x + 1))
  pose (msgin := multiplier ^ (x + 1)).multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
valid_message_prop radix_vlsm
  (multiplier ^ (Z.succ x + 1))
  apply emitted_messages_are_valid.multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
can_emit radix_vlsm (multiplier ^ (Z.succ x + 1))
  exists (msgin, Some (multiplier ^ (x + 1))), radix_label, 0.multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
input_valid_transition radix_vlsm radix_label
  (msgin, Some (multiplier ^ (x + 1)))
  (0, Some (multiplier ^ (Z.succ x + 1)))
  repeat split.multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
valid_state_prop radix_vlsm msgin
multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
option_valid_message_prop radix_vlsm
  (Some (multiplier ^ (x + 1)))
multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
2 ≤ multiplier ^ (x + 1)
multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
multiplier ^ (x + 1) ≤ msgin
multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
transition radix_label
  (msgin, Some (multiplier ^ (x + 1))) =
(0, Some (multiplier ^ (Z.succ x + 1)))
  -multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
valid_state_prop radix_vlsm msgin by apply initial_state_is_valid; cbn; red; lia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
option_valid_message_prop radix_vlsm
  (Some (multiplier ^ (x + 1))) by apply Hindh.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
2 ≤ multiplier ^ (x + 1) replace (x + 1) with (Z.succ x) by lia.multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
2 ≤ multiplier ^ Z.succ x
    by rewrite Z.pow_succ_r; lia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
multiplier ^ (x + 1) ≤ msgin by lia.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop radix_vlsm
  (multiplier ^ (x + 1))
msgin:= multiplier ^ (x + 1): Z
transition radix_label
  (msgin, Some (multiplier ^ (x + 1))) =
(0, Some (multiplier ^ (Z.succ x + 1))) by cbn; rewrite <- Z.pow_succ_r, Z.add_succ_l; [do 2 f_equal; lia | lia].
Qed.

Lemma radix_valid_messages_powers_of_mult :
  forall (m : multiplying_message),
    valid_message_prop radix_vlsm m
      <->
    exists p : Z, p >= 1 /\ m = multiplier ^ p.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  valid_message_prop radix_vlsm m
  ↔ (∃ p : Z, p >= 1 ∧ m = multiplier ^ p)
Proof.multiplier: Z
multiplier_gt_1: multiplier > 1
∀ m : multiplying_message,
  valid_message_prop radix_vlsm m
  ↔ (∃ p : Z, p >= 1 ∧ m = multiplier ^ p)
  split.multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
valid_message_prop radix_vlsm m
→ ∃ p : Z, p >= 1 ∧ m = multiplier ^ p
multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
(∃ p : Z, p >= 1 ∧ m = multiplier ^ p)
→ valid_message_prop radix_vlsm m
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
valid_message_prop radix_vlsm m
→ ∃ p : Z, p >= 1 ∧ m = multiplier ^ p by intros; apply radix_valid_messages_powers_of_mult_right.
  -multiplier: Z
multiplier_gt_1: multiplier > 1
m: multiplying_message
(∃ p : Z, p >= 1 ∧ m = multiplier ^ p)
→ valid_message_prop radix_vlsm m by intros (p & Hpgt0 & [= ->]); apply radix_valid_messages_powers_of_mult_left.
Qed.

End sec_radix_vlsm.

Section sec_composition.

Context
  {index : Type}
  (multipliers : index -> Z)
  (Hmultipliers : forall (i : index), multipliers i <> 0)
  `{FinSet index indexSet}
  .

Definition indexed_radix_vlsms (i : index) : VLSM multiplying_message :=
  radix_vlsm (multipliers i).

Context
  (radix_constraint : composite_label indexed_radix_vlsms ->
    composite_state indexed_radix_vlsms * option multiplying_message -> Prop)
  .

Definition radix_composite_vlsm : VLSM multiplying_message :=
  composite_vlsm indexed_radix_vlsms radix_constraint.

Lemma composite_state_pos
  (s : composite_state indexed_radix_vlsms)
  (Hs : valid_state_prop radix_composite_vlsm s) :
    forall (i : index), s i >= 0.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: composite_state indexed_radix_vlsms
Hs: valid_state_prop radix_composite_vlsm s
∀ i : index, s i >= 0
Proof.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: composite_state indexed_radix_vlsms
Hs: valid_state_prop radix_composite_vlsm s
∀ i : index, s i >= 0
  intros i.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: composite_state indexed_radix_vlsms
Hs: valid_state_prop radix_composite_vlsm s
i: index
s i >= 0
  apply radix_constrained_states_right with (multipliers i).index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: composite_state indexed_radix_vlsms
Hs: valid_state_prop radix_composite_vlsm s
i: index
constrained_state_prop (radix_vlsm (multipliers i))
  (s i)
  by apply (valid_state_project_preloaded multiplying_message indexed_radix_vlsms radix_constraint).
Qed.

Any valid message can be expressed as a non-empty product of powers of the multipliers associated to the components.

Lemma composition_valid_messages_powers_of_mults_right (m : multiplying_message) :
  valid_message_prop radix_composite_vlsm m ->
  exists (f : fsfun index 0%nat),
    fin_supp f <> [] /\ m = fsfun_prod multipliers f.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
m: multiplying_message
valid_message_prop radix_composite_vlsm m
→ ∃ f : fsfun index 0%nat,
    fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
Proof.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
m: multiplying_message
valid_message_prop radix_composite_vlsm m
→ ∃ f : fsfun index 0%nat,
    fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
  intros [s Hvsm].index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
m: multiplying_message
s: state radix_composite_vlsm
Hvsm: valid_state_message_prop radix_composite_vlsm s
  (Some m)
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
  remember (Some m) as om.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
m: multiplying_message
s: state radix_composite_vlsm
om: option multiplying_message
Heqom: om = Some m
Hvsm: valid_state_message_prop radix_composite_vlsm s
  om
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
  revert m Heqom.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
om: option multiplying_message
Hvsm: valid_state_message_prop radix_composite_vlsm s
  om
∀ m : multiplying_message,
  om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
  induction Hvsm using valid_state_message_prop_ind; intros; subst.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
Hs: initial_state_prop s
m: multiplying_message
Hom: option_initial_message_prop radix_composite_vlsm
  (Some m)
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
om: option multiplying_message
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s om
l: label radix_composite_vlsm
Hv: valid l (s, om)
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition l (s, om) = (s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
  -index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
Hs: initial_state_prop s
m: multiplying_message
Hom: option_initial_message_prop radix_composite_vlsm
  (Some m)
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f destruct Hom as (n & (mielem & mi) & Hmi); cbn in mi, Hmi.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
Hs: initial_state_prop s
m: multiplying_message
n: index
mielem: multiplying_message
mi: mielem = multipliers n
Hmi: mielem = m
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
    exists (delta_nat_fsfun n).index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
Hs: initial_state_prop s
m: multiplying_message
n: index
mielem: multiplying_message
mi: mielem = multipliers n
Hmi: mielem = m
fin_supp (delta_nat_fsfun n) ≠ []
∧ m = fsfun_prod multipliers (delta_nat_fsfun n)
    split; [by eapply elem_of_not_nil, elem_of_delta_nat_fsfun |].index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
Hs: initial_state_prop s
m: multiplying_message
n: index
mielem: multiplying_message
mi: mielem = multipliers n
Hmi: mielem = m
m = fsfun_prod multipliers (delta_nat_fsfun n)
    by rewrite <- Hmi, mi, prod_powers_delta.
  -index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
om: option multiplying_message
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s om
l: label radix_composite_vlsm
Hv: valid l (s, om)
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition l (s, om) = (s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f destruct l as (k & lk).index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
om: option multiplying_message
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s om
k: index
lk: label (indexed_radix_vlsms k)
Hv: valid (existT k lk) (s, om)
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition (existT k lk) (s, om) = (s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
    destruct om; [| done].index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
m0: multiplying_message
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s (Some m0)
k: index
lk: label (indexed_radix_vlsms k)
Hv: valid (existT k lk) (s, Some m0)
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition (existT k lk) (s, Some m0) =
(s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  Some m0 = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
    destruct (IHHvsm2 _ eq_refl) as (f & Hdomf & ->).index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
f: fsfun index 0%nat
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s (Some (fsfun_prod multipliers f))
k: index
lk: label (indexed_radix_vlsms k)
Hv: valid (existT k lk)
  (s, Some (fsfun_prod multipliers f))
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition (existT k lk)
  (s, Some (fsfun_prod multipliers f)) =
(s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  Some (fsfun_prod multipliers f) = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
Hdomf: fin_supp f ≠ []
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
    inversion Ht.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
f: fsfun index 0%nat
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s (Some (fsfun_prod multipliers f))
k: index
lk: label (indexed_radix_vlsms k)
Hv: valid (existT k lk)
  (s, Some (fsfun_prod multipliers f))
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition (existT k lk)
  (s, Some (fsfun_prod multipliers f)) =
(s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  Some (fsfun_prod multipliers f) = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
Hdomf: fin_supp f ≠ []
H8: state_update indexed_radix_vlsms s k
  (s k - fsfun_prod multipliers f) = s'
H9: multipliers k * fsfun_prod multipliers f = m
∃ f0 : fsfun index 0%nat,
  fin_supp f0 ≠ []
  ∧ multipliers k * fsfun_prod multipliers f =
    fsfun_prod multipliers f0
    exists (succ_fsfun f k).index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
f: fsfun index 0%nat
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s (Some (fsfun_prod multipliers f))
k: index
lk: label (indexed_radix_vlsms k)
Hv: valid (existT k lk)
  (s, Some (fsfun_prod multipliers f))
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition (existT k lk)
  (s, Some (fsfun_prod multipliers f)) =
(s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  Some (fsfun_prod multipliers f) = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
Hdomf: fin_supp f ≠ []
H8: state_update indexed_radix_vlsms s k
  (s k - fsfun_prod multipliers f) = s'
H9: multipliers k * fsfun_prod multipliers f = m
fin_supp (succ_fsfun f k) ≠ []
∧ multipliers k * fsfun_prod multipliers f =
  fsfun_prod multipliers (succ_fsfun f k)
    split; [| by rewrite fsfun_prod_succ].index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
f: fsfun index 0%nat
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s (Some (fsfun_prod multipliers f))
k: index
lk: label (indexed_radix_vlsms k)
Hv: valid (existT k lk)
  (s, Some (fsfun_prod multipliers f))
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition (existT k lk)
  (s, Some (fsfun_prod multipliers f)) =
(s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  Some (fsfun_prod multipliers f) = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
Hdomf: fin_supp f ≠ []
H8: state_update indexed_radix_vlsms s k
  (s k - fsfun_prod multipliers f) = s'
H9: multipliers k * fsfun_prod multipliers f = m
fin_supp (succ_fsfun f k) ≠ []
    apply not_null_element in Hdomf; destruct_dec_sig Hdomf i Hi Heq.index: Type
multipliers: index → Z
Hmultipliers: ∀ i : index, multipliers i ≠ 0
indexSet: Type
H: ElemOf index indexSet
H0: Empty indexSet
H1: Singleton index indexSet
H2: Union indexSet
H3: Intersection indexSet
H4: Difference indexSet
H5: Elements index indexSet
EqDecision0: EqDecision index
H6: FinSet index indexSet
radix_constraint: composite_label indexed_radix_vlsms
→ composite_state
    indexed_radix_vlsms *
  option multiplying_message → Prop
s: state radix_composite_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop radix_composite_vlsm
  s _om
_s: state radix_composite_vlsm
f: fsfun index 0%nat
Hvsm2: valid_state_message_prop radix_composite_vlsm
  _s (Some (fsfun_prod multipliers f))
k: index
lk: label (indexed_radix_vlsms k)
Hv: valid (existT k lk)
  (s, Some (fsfun_prod multipliers f))
s': state radix_composite_vlsm
m: multiplying_message
Ht: transition (existT k lk)
  (s, Some (fsfun_prod multipliers f)) =
(s', Some m)
IHHvsm1: ∀ m : multiplying_message,
  _om = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
IHHvsm2: ∀ m : multiplying_message,
  Some (fsfun_prod multipliers f) = Some m
  → ∃ f : fsfun index 0%nat,
      fin_supp f ≠ []
      ∧ m = fsfun_prod multipliers f
Hdomf: dsig (λ i : index, i ∈ fin_supp f)
H8: state_update indexed_radix_vlsms s k
  (s k - fsfun_prod multipliers f) = s'
H9: multipliers k * fsfun_prod multipliers f = m
i: index
Hi: i ∈ fin_supp f
Heq: Hdomf = dexist i Hi
fin_supp (succ_fsfun f k) ≠ []
    by eapply elem_of_not_nil, elem_of_succ_fsfun; right.
Qed.

End sec_composition.

Section sec_free_composition.

Context
  `{EqDecision index}
  (multipliers : index -> Z)
  `{Inhabited index}
  .

Definition free_radix_composite_vlsm : VLSM multiplying_message :=
  free_composite_vlsm (indexed_radix_vlsms multipliers).

#[local] Lemma free_radix_composite_vlsm_emits_multiplier :
  forall (m : multiplying_message),
    valid_message_prop free_radix_composite_vlsm m ->
    m >= 2 ->
  forall (n : index),
  input_valid_transition free_radix_composite_vlsm (existT n radix_label)
(update (const 1) n (m + 1), Some m)
(const 1, Some (multipliers n * m)).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
∀ m : multiplying_message,
  valid_message_prop free_radix_composite_vlsm m
  → m >= 2
    → ∀ n : index,
        input_valid_transition
          free_radix_composite_vlsm
          (existT n radix_label)
          (update (const 1) n (m + 1), Some m)
          (const 1, Some (multipliers n * m))
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
∀ m : multiplying_message,
  valid_message_prop free_radix_composite_vlsm m
  → m >= 2
    → ∀ n : index,
        input_valid_transition
          free_radix_composite_vlsm
          (existT n radix_label)
          (update (const 1) n (m + 1), Some m)
          (const 1, Some (multipliers n * m))
  repeat split.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
valid_state_prop free_radix_composite_vlsm
  (update (const 1) n (m + 1))
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
option_valid_message_prop free_radix_composite_vlsm
  (Some m)
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
2 ≤ m
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
m ≤ update (const 1) n (m + 1) n
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
transition (existT n radix_label)
  (update (const 1) n (m + 1), Some m) =
(const 1, Some (multipliers n * m))
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
valid_state_prop free_radix_composite_vlsm
  (update (const 1) n (m + 1)) apply initial_state_is_valid.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
initial_state_prop (update (const 1) n (m + 1))
    intros j; cbn; red.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n, j: index
update (const 1) n (m + 1) j >= 1
    by destruct (decide (n = j)) as [-> |];
      [rewrite update_eq; lia | rewrite update_neq].
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
option_valid_message_prop free_radix_composite_vlsm
  (Some m) done.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
2 ≤ m by lia.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
m ≤ update (const 1) n (m + 1) n by rewrite update_eq; lia.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
transition (existT n radix_label)
  (update (const 1) n (m + 1), Some m) =
(const 1, Some (multipliers n * m)) cbn; f_equal; rewrite update_eq.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n: index
state_update (indexed_radix_vlsms multipliers)
  (update (const 1) n (m + 1)) n (m + 1 - m) = const 1
    extensionality j; cbn.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n, j: index
state_update (indexed_radix_vlsms multipliers)
  (update (const 1) n (m + 1)) n (m + 1 - m) j = 1
    destruct (decide (n =j)) as [-> |]; state_update_simpl; [by lia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
m: multiplying_message
H0: valid_message_prop free_radix_composite_vlsm m
H1: m >= 2
n, j: index
n0: n ≠ j
update (const 1) n (m + 1) j = 1
    by rewrite update_neq.
Qed.

Lemma composition_valid_messages_powers_of_mults_left
  (Hmpos : forall (i : index), multipliers i > 1) (m : multiplying_message)
  (f : fsfun index 0%nat) :
    fin_supp f <> [] /\ m = fsfun_prod multipliers f ->
    valid_message_prop free_radix_composite_vlsm m.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
f: fsfun index 0%nat
fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
→ valid_message_prop free_radix_composite_vlsm m
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
f: fsfun index 0%nat
fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
→ valid_message_prop free_radix_composite_vlsm m
  intros [Hpowgeq1 Hm]; revert f Hpowgeq1 m Hm.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
∀ f : fsfun index 0%nat,
  fin_supp f ≠ []
  → ∀ m : multiplying_message,
      m = fsfun_prod multipliers f
      → valid_message_prop free_radix_composite_vlsm m
  apply (nat_fsfun_ind (fun (f : fsfun index 0%nat) => fin_supp f <> [] ->
    forall m : multiplying_message, m = fsfun_prod multipliers f ->
    valid_message_prop free_radix_composite_vlsm m)); [| done |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
Proper (equiv ==> impl)
  (λ f : fsfun index 0%nat,
     fin_supp f ≠ []
     → ∀ m : multiplying_message,
         m = fsfun_prod multipliers f
         → valid_message_prop
             free_radix_composite_vlsm m)
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
∀ (i : index) (f : fsfun index 0%nat),
  (fin_supp f ≠ []
   → ∀ m : multiplying_message,
       m = fsfun_prod multipliers f
       → valid_message_prop free_radix_composite_vlsm
           m)
  → fin_supp (succ_fsfun f i) ≠ []
    → ∀ m : multiplying_message,
        m = fsfun_prod multipliers (succ_fsfun f i)
        → valid_message_prop free_radix_composite_vlsm
            m
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
Proper (equiv ==> impl)
  (λ f : fsfun index 0%nat,
     fin_supp f ≠ []
     → ∀ m : multiplying_message,
         m = fsfun_prod multipliers f
         → valid_message_prop
             free_radix_composite_vlsm m) intros f1 f2 Heq Hall Hi m Hm.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
f1, f2: fsfun index 0%nat
Heq: f1 ≡ f2
Hall: fin_supp f1 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f1
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp f2 ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers f2
valid_message_prop free_radix_composite_vlsm m
    eapply Hall; [| by rewrite Heq].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
f1, f2: fsfun index 0%nat
Heq: f1 ≡ f2
Hall: fin_supp f1 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f1
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp f2 ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers f2
fin_supp f1 ≠ []
    contradict Hi.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
f1, f2: fsfun index 0%nat
Heq: f1 ≡ f2
Hall: fin_supp f1 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f1
    → valid_message_prop
        free_radix_composite_vlsm m
m: multiplying_message
Hm: m = fsfun_prod multipliers f2
Hi: fin_supp f1 = []
fin_supp f2 = []
    apply Permutation_nil.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
f1, f2: fsfun index 0%nat
Heq: f1 ≡ f2
Hall: fin_supp f1 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f1
    → valid_message_prop
        free_radix_composite_vlsm m
m: multiplying_message
Hm: m = fsfun_prod multipliers f2
Hi: fin_supp f1 = []
[] ≡ₚ fin_supp f2
    by rewrite <- Hi, Heq.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
∀ (i : index) (f : fsfun index 0%nat),
  (fin_supp f ≠ []
   → ∀ m : multiplying_message,
       m = fsfun_prod multipliers f
       → valid_message_prop free_radix_composite_vlsm
           m)
  → fin_supp (succ_fsfun f i) ≠ []
    → ∀ m : multiplying_message,
        m = fsfun_prod multipliers (succ_fsfun f i)
        → valid_message_prop free_radix_composite_vlsm
            m intros n f0 IHf0 Hi m Hm.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
valid_message_prop free_radix_composite_vlsm m
    destruct (nat_fsfun_inv f0) as [Heq | (n' & f0' & Heq)].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
Heq: f0 ≡ zero_fsfun
valid_message_prop free_radix_composite_vlsm m
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
valid_message_prop free_radix_composite_vlsm m
    +index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
Heq: f0 ≡ zero_fsfun
valid_message_prop free_radix_composite_vlsm m rewrite fsfun_prod_succ, Heq, fsfun_prod_zero in Hm.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = multipliers n * 1
Heq: f0 ≡ zero_fsfun
valid_message_prop free_radix_composite_vlsm m
      apply initial_message_is_valid.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = multipliers n * 1
Heq: f0 ≡ zero_fsfun
initial_message_prop m exists n.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = multipliers n * 1
Heq: f0 ≡ zero_fsfun
∃ mi : initial_message
         (indexed_radix_vlsms multipliers n), `mi = m
      by unshelve eexists (exist _ m _); cbn; lia.
    +index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
valid_message_prop free_radix_composite_vlsm m assert (Hmvalid : valid_message_prop free_radix_composite_vlsm (fsfun_prod multipliers f0)).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
valid_message_prop free_radix_composite_vlsm m
      {index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
        apply IHf0; [| done].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
fin_supp f0 ≠ []
        assert (Hinh : fin_supp (succ_fsfun f0' n') <> []).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
fin_supp (succ_fsfun f0' n') ≠ []
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hinh: fin_supp (succ_fsfun f0' n') ≠ []
fin_supp f0 ≠ []
        {index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
fin_supp (succ_fsfun f0' n') ≠ []
          by eapply elem_of_not_nil, elem_of_succ_fsfun; left.
        }index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hinh: fin_supp (succ_fsfun f0' n') ≠ []
fin_supp f0 ≠ []
        contradict Hinh; apply Permutation_nil.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hinh: fin_supp f0 = []
[] ≡ₚ fin_supp (succ_fsfun f0' n')
        by rewrite <- Hinh, Heq.
      }index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
m: multiplying_message
Hm: m = fsfun_prod multipliers (succ_fsfun f0 n)
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
valid_message_prop free_radix_composite_vlsm m
      subst m; rewrite fsfun_prod_succ.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
valid_message_prop free_radix_composite_vlsm
  (multipliers n * fsfun_prod multipliers f0)
      assert (Hpos : fsfun_prod multipliers f0 >= multipliers n').index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
fsfun_prod multipliers f0 >= multipliers n'
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
Hpos: fsfun_prod multipliers f0 >= multipliers n'
valid_message_prop free_radix_composite_vlsm
  (multipliers n * fsfun_prod multipliers f0)
      {index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
fsfun_prod multipliers f0 >= multipliers n'
        rewrite Heq, fsfun_prod_succ.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
multipliers n' * fsfun_prod multipliers f0' >=
multipliers n'
        cut (fsfun_prod multipliers f0' > 0); [by specialize (Hmpos n'); nia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
fsfun_prod multipliers f0' > 0
        destruct (decide (fin_supp f0' = [])) as [Hz |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
Hz: fin_supp f0' = []
fsfun_prod multipliers f0' > 0
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
n0: fin_supp f0' ≠ []
fsfun_prod multipliers f0' > 0
        -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
Hz: fin_supp f0' = []
fsfun_prod multipliers f0' > 0 eapply empty_fsfun_supp_inv in Hz as ->.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
fsfun_prod multipliers empty_fsfun > 0
          by setoid_rewrite fsfun_prod_zero; lia.
        -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
n0: fin_supp f0' ≠ []
fsfun_prod multipliers f0' > 0 apply prod_powers_gt; [by lia | | done].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
n0: fin_supp f0' ≠ []
∀ i : index, multipliers i > 0
          by intro i; specialize (Hmpos i); lia.
      }index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
n': index
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
Hpos: fsfun_prod multipliers f0 >= multipliers n'
valid_message_prop free_radix_composite_vlsm
  (multipliers n * fsfun_prod multipliers f0)
      specialize (Hmpos n').index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
n': index
Hmpos: multipliers n' > 1
n: index
f0: fsfun index 0%nat
IHf0: fin_supp f0 ≠ []
→ ∀ m : multiplying_message,
    m = fsfun_prod multipliers f0
    → valid_message_prop
        free_radix_composite_vlsm m
Hi: fin_supp (succ_fsfun f0 n) ≠ []
f0': fsfun index 0%nat
Heq: f0 ≡ succ_fsfun f0' n'
Hmvalid: valid_message_prop free_radix_composite_vlsm
  (fsfun_prod multipliers f0)
Hpos: fsfun_prod multipliers f0 >= multipliers n'
valid_message_prop free_radix_composite_vlsm
  (multipliers n * fsfun_prod multipliers f0)
      by eapply input_valid_transition_out,
        free_radix_composite_vlsm_emits_multiplier; [| lia].
Qed.

Lemma composition_valid_messages_powers_of_mults
  (Hmpos : forall (i : index), multipliers i > 1) (m : multiplying_message) :
    valid_message_prop free_radix_composite_vlsm m <->
  exists (f : fsfun index 0%nat),
    fin_supp f <> [] /\ m = fsfun_prod multipliers f.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
valid_message_prop free_radix_composite_vlsm m
↔ (∃ f : fsfun index 0%nat,
     fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f)
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
valid_message_prop free_radix_composite_vlsm m
↔ (∃ f : fsfun index 0%nat,
     fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f)
  split.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
valid_message_prop free_radix_composite_vlsm m
→ ∃ f : fsfun index 0%nat,
    fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
(∃ f : fsfun index 0%nat,
   fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f)
→ valid_message_prop free_radix_composite_vlsm m
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
valid_message_prop free_radix_composite_vlsm m
→ ∃ f : fsfun index 0%nat,
    fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f intros Hvm.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hvm: valid_message_prop free_radix_composite_vlsm m
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
    eapply VLSM_incl_valid_message in Hvm; cycle 1.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hvm: valid_message_prop free_radix_composite_vlsm m
VLSM_incl_part
  (free_composite_vlsm_machine
     (indexed_radix_vlsms multipliers)) ?MY
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hvm: valid_message_prop free_radix_composite_vlsm m
strong_incl_initial_message_preservation
  (free_composite_vlsm_machine
     (indexed_radix_vlsms multipliers)) 
  ?MY
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hvm: valid_message_prop
  {|
    vlsm_type :=
      composite_type
        (indexed_radix_vlsms multipliers);
    vlsm_machine := ?MY
  |} m
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f
    +index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hvm: valid_message_prop free_radix_composite_vlsm m
VLSM_incl_part
  (free_composite_vlsm_machine
     (indexed_radix_vlsms multipliers)) ?MY by apply free_composite_vlsm_spec.
    +index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hvm: valid_message_prop free_radix_composite_vlsm m
strong_incl_initial_message_preservation
  (free_composite_vlsm_machine
     (indexed_radix_vlsms multipliers))
  {|
    vlsm_type :=
      free_composite_vlsm
        (indexed_radix_vlsms multipliers);
    vlsm_machine :=
      composite_vlsm (indexed_radix_vlsms multipliers)
        (free_constraint
           (indexed_radix_vlsms multipliers))
  |} by do 2 red.
    +index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hvm: valid_message_prop
  {|
    vlsm_type :=
      composite_type
        (indexed_radix_vlsms multipliers);
    vlsm_machine :=
      {|
        vlsm_type :=
          free_composite_vlsm
            (indexed_radix_vlsms multipliers);
        vlsm_machine :=
          composite_vlsm
            (indexed_radix_vlsms multipliers)
            (free_constraint
               (indexed_radix_vlsms multipliers))
      |}
  |} m
∃ f : fsfun index 0%nat,
  fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f by cbn in Hvm; eapply composition_valid_messages_powers_of_mults_right.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
(∃ f : fsfun index 0%nat,
   fin_supp f ≠ [] ∧ m = fsfun_prod multipliers f)
→ valid_message_prop free_radix_composite_vlsm m by intros [? []]; eapply composition_valid_messages_powers_of_mults_left.
Qed.

Lemma composition_valid_message_ge_2
  (Hmpos : forall (i : index), multipliers i > 1) (m : multiplying_message) :
  valid_message_prop free_radix_composite_vlsm m -> m >= 2.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
valid_message_prop free_radix_composite_vlsm m
→ m >= 2
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
valid_message_prop free_radix_composite_vlsm m
→ m >= 2
  intro Hv.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
m: multiplying_message
Hv: valid_message_prop free_radix_composite_vlsm m
m >= 2
  apply composition_valid_messages_powers_of_mults in Hv
    as (i & Hsupp & ->); [| done].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
i: fsfun index 0%nat
Hsupp: fin_supp i ≠ []
fsfun_prod multipliers i >= 2
  cut (fsfun_prod multipliers i > 1); [by lia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
H: Inhabited index
Hmpos: ∀ i : index, multipliers i > 1
i: fsfun index 0%nat
Hsupp: fin_supp i ≠ []
fsfun_prod multipliers i > 1
  by apply prod_powers_gt; [lia | ..].
Qed.

End sec_free_composition.

A VLSM composition for all primes

In the following section we give an example of a composition with an infinite number of radix_vlsm components, one for each prime number.

Then we characterize the valid messages for this composition to be precisely all natural numbers larger than 1.

Finally, we show that in this composition any component is a validator.

Section sec_primes_vlsm_composition.

Definition primes_vlsm_composition : VLSM Z :=
  free_radix_composite_vlsm (fun p : primes => `p).

Lemma primes_vlsm_composition_valid_message_char :
  forall (m : Z),
    valid_message_prop primes_vlsm_composition m <-> m > 1.∀ m : Z,
  valid_message_prop primes_vlsm_composition m ↔ m > 1
Proof.∀ m : Z,
  valid_message_prop primes_vlsm_composition m ↔ m > 1
  assert (Hprime_pos : forall i : primes, `i > 1).∀ i : primes, `i > 1
Hprime_pos: ∀ i : primes, `i > 1
∀ m : Z,
  valid_message_prop primes_vlsm_composition m ↔ m > 1
  {∀ i : primes, `i > 1
    intro i.i: primes
`i > 1
    destruct_dec_sig i n Hn Heq; subst; cbn.n: Z
Hn: prime n
n > 1
    by destruct Hn; lia.
  }Hprime_pos: ∀ i : primes, `i > 1
∀ m : Z,
  valid_message_prop primes_vlsm_composition m ↔ m > 1
  intros m; unfold primes_vlsm_composition.Hprime_pos: ∀ i : primes, `i > 1
m: Z
valid_message_prop
  (free_radix_composite_vlsm (λ p : primes, `p)) m
↔ m > 1
  rewrite composition_valid_messages_powers_of_mults;
    [| by intro i; specialize (Hprime_pos i); lia..].Hprime_pos: ∀ i : primes, `i > 1
m: Z
(∃ f : fsfun primes 0%nat,
   fin_supp f ≠ []
   ∧ m = fsfun_prod (λ p : primes, `p) f) ↔ m > 1
  split.Hprime_pos: ∀ i : primes, `i > 1
m: Z
(∃ f : fsfun primes 0%nat,
   fin_supp f ≠ []
   ∧ m = fsfun_prod (λ p : primes, `p) f) → m > 1
Hprime_pos: ∀ i : primes, `i > 1
m: Z
m > 1
→ ∃ f : fsfun primes 0%nat,
    fin_supp f ≠ []
    ∧ m = fsfun_prod (λ p : primes, `p) f
  -Hprime_pos: ∀ i : primes, `i > 1
m: Z
(∃ f : fsfun primes 0%nat,
   fin_supp f ≠ []
   ∧ m = fsfun_prod (λ p : primes, `p) f) → m > 1 intros (fp & Hdom_fp & ->).Hprime_pos: ∀ i : primes, `i > 1
fp: fsfun primes 0%nat
Hdom_fp: fin_supp fp ≠ []
fsfun_prod (λ p : primes, `p) fp > 1
    by apply prod_powers_gt.
  -Hprime_pos: ∀ i : primes, `i > 1
m: Z
m > 1
→ ∃ f : fsfun primes 0%nat,
    fin_supp f ≠ []
    ∧ m = fsfun_prod (λ p : primes, `p) f by apply primes_factorization.
Qed.

For any prime number, its corresponding component in the primes_vlsm_composition is a validator for that composition, i.e., all of its constrained transitions can be lifted to valid transitions for the composition.

Theorem component_projection_validator_prop_primes :
  forall (p : primes),
    component_projection_validator_prop
      (indexed_radix_vlsms (fun p : primes => ` p))
      (fun _ _ => True) p.∀ p : primes,
  component_projection_validator_prop
    (indexed_radix_vlsms (λ p0 : primes, `p0))
    (λ (_ : composite_label
              (indexed_radix_vlsms
                 (λ p0 : primes, `p0))) (_ : composite_state
                                               (indexed_radix_vlsms
                                                 (λ p0 : primes,
                                                 `p0)) *
                                             option
                                               multiplying_message),
       True) p
Proof.∀ p : primes,
  component_projection_validator_prop
    (indexed_radix_vlsms (λ p0 : primes, `p0))
    (λ (_ : composite_label
              (indexed_radix_vlsms
                 (λ p0 : primes, `p0))) (_ : composite_state
                                               (indexed_radix_vlsms
                                                 (λ p0 : primes,
                                                 `p0)) *
                                             option
                                               multiplying_message),
       True) p
  intros p lp sp [m|] (Hsp & _ & []).p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
valid lp (sp, Some m)
  exists (lift_to_composite_state' (indexed_radix_vlsms (fun p : primes => `p)) p sp).p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
lift_to_composite_state'
  (indexed_radix_vlsms (λ p : primes, `p)) p sp p = sp
∧ input_valid
    (composite_vlsm
       (indexed_radix_vlsms (λ p : primes, `p))
       (λ (_ : composite_label
                 (indexed_radix_vlsms
                    (λ p : primes, `p))) (_ : composite_state
                                                (indexed_radix_vlsms
                                                 (λ p : primes,
                                                 `p)) *
                                              option
                                                multiplying_message),
          True)) (existT p lp)
    (lift_to_composite_state'
       (indexed_radix_vlsms (λ p : primes, `p)) p sp,
     Some m)
  repeat split; cycle 1; [| | by state_update_simpl..].p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
valid_state_prop
  (composite_vlsm
     (indexed_radix_vlsms (λ p : primes, `p))
     (λ (_ : composite_label
               (indexed_radix_vlsms (λ p : primes, `p))) 
        (_ : composite_state
               (indexed_radix_vlsms (λ p : primes, `p)) *
             option multiplying_message), True))
  (lift_to_composite_state'
     (indexed_radix_vlsms (λ p : primes, `p)) p sp)
p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
option_valid_message_prop
  (composite_vlsm
     (indexed_radix_vlsms (λ p : primes, `p))
     (λ (_ : composite_label
               (indexed_radix_vlsms (λ p : primes, `p))) 
        (_ : composite_state
               (indexed_radix_vlsms (λ p : primes, `p)) *
             option multiplying_message), True))
  (Some m)
  -p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
valid_state_prop
  (composite_vlsm
     (indexed_radix_vlsms (λ p : primes, `p))
     (λ (_ : composite_label
               (indexed_radix_vlsms (λ p : primes, `p))) 
        (_ : composite_state
               (indexed_radix_vlsms (λ p : primes, `p)) *
             option multiplying_message), True))
  (lift_to_composite_state'
     (indexed_radix_vlsms (λ p : primes, `p)) p sp) apply initial_state_is_valid.p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
initial_state_prop
  (lift_to_composite_state'
     (indexed_radix_vlsms (λ p : primes, `p)) p sp)
    intros p'; cbn; red.p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
p': primes
lift_to_composite_state'
  (indexed_radix_vlsms (λ p : primes, `p)) p sp p' >=
1
    by destruct (decide (p = p')); subst; state_update_simpl; cbn; [lia |].
  -p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
option_valid_message_prop
  (composite_vlsm
     (indexed_radix_vlsms (λ p : primes, `p))
     (λ (_ : composite_label
               (indexed_radix_vlsms (λ p : primes, `p))) 
        (_ : composite_state
               (indexed_radix_vlsms (λ p : primes, `p)) *
             option multiplying_message), True))
  (Some m) eapply VLSM_incl_valid_message; [by apply free_composite_vlsm_spec | ..].p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
strong_incl_initial_message_preservation
  {|
    vlsm_type :=
      free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p));
    vlsm_machine :=
      free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p))
  |}
  (constrained_vlsm_machine
     (free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p)))
     (λ (_ : composite_label
               (indexed_radix_vlsms (λ p : primes, `p))) 
        (_ : composite_state
               (indexed_radix_vlsms (λ p : primes, `p)) *
             option multiplying_message), True))
p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
valid_message_prop
  {|
    vlsm_type :=
      free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p));
    vlsm_machine :=
      {|
        vlsm_type :=
          free_composite_vlsm
            (indexed_radix_vlsms (λ p : primes, `p));
        vlsm_machine :=
          free_composite_vlsm
            (indexed_radix_vlsms (λ p : primes, `p))
      |}
  |} m
    +p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
strong_incl_initial_message_preservation
  {|
    vlsm_type :=
      free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p));
    vlsm_machine :=
      free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p))
  |}
  (constrained_vlsm_machine
     (free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p)))
     (λ (_ : composite_label
               (indexed_radix_vlsms (λ p : primes, `p))) 
        (_ : composite_state
               (indexed_radix_vlsms (λ p : primes, `p)) *
             option multiplying_message), True)) by do 2 red.
    +p: primes
lp: label (indexed_radix_vlsms (λ p : primes, `p) p)
sp: state (indexed_radix_vlsms (λ p : primes, `p) p)
m: multiplying_message
Hsp: valid_state_prop
(preloaded_with_all_messages_vlsm
(indexed_radix_vlsms (λ p : primes, `p) p)) sp
H: 2 ≤ m
H0: m ≤ sp
valid_message_prop
  {|
    vlsm_type :=
      free_composite_vlsm
        (indexed_radix_vlsms (λ p : primes, `p));
    vlsm_machine :=
      {|
        vlsm_type :=
          free_composite_vlsm
            (indexed_radix_vlsms (λ p : primes, `p));
        vlsm_machine :=
          free_composite_vlsm
            (indexed_radix_vlsms (λ p : primes, `p))
      |}
  |} m by apply primes_vlsm_composition_valid_message_char; lia.
Qed.

A (slightly) constrained composition of primes

To show how a composition constraint affects validation, we here add a very simple constraint, that the received message must be even, to the composition.

Inductive EvenConstraint :
  label primes_vlsm_composition -> state primes_vlsm_composition * option Z -> Prop :=
| even_constraint : forall l s m, Z.Even m -> EvenConstraint l (s, Some m).

Definition even_constrained_primes_composition : VLSM Z :=
  constrained_vlsm primes_vlsm_composition EvenConstraint.

#[local] Lemma even_constrained_primes_composition_emits_multiplier :
  forall (m : multiplying_message),
    valid_message_prop even_constrained_primes_composition m ->
    m >= 2 ->
    Z.Even m ->
  forall (n : primes),
  input_valid_transition even_constrained_primes_composition (existT n radix_label)
  (update (const 1) n (m + 1), Some m)
  (const 1, Some (` n * m)).∀ m : multiplying_message,
  valid_message_prop
    even_constrained_primes_composition m
  → m >= 2
    → Z.Even m
      → ∀ n : primes,
          input_valid_transition
            even_constrained_primes_composition
            (existT n radix_label)
            (update (const 1) n (m + 1), Some m)
            (const 1, Some (`n * m))
Proof.∀ m : multiplying_message,
  valid_message_prop
    even_constrained_primes_composition m
  → m >= 2
    → Z.Even m
      → ∀ n : primes,
          input_valid_transition
            even_constrained_primes_composition
            (existT n radix_label)
            (update (const 1) n (m + 1), Some m)
            (const 1, Some (`n * m))
  repeat split.m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
valid_state_prop even_constrained_primes_composition
  (update (const 1) n (m + 1))
m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
option_valid_message_prop
  even_constrained_primes_composition (Some m)
m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
2 ≤ m
m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
m ≤ update (const 1) n (m + 1) n
m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
Z.Even m
m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
transition (existT n radix_label)
  (update (const 1) n (m + 1), Some m) =
(const 1, Some (`n * m))
  -m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
valid_state_prop even_constrained_primes_composition
  (update (const 1) n (m + 1)) apply initial_state_is_valid.m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
initial_state_prop (update (const 1) n (m + 1))
    intros j; cbn; red.m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n, j: primes
update (const 1) n (m + 1) j >= 1
    by destruct (decide (n = j)) as [-> |];
      [rewrite update_eq; lia | rewrite update_neq].
  -m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
option_valid_message_prop
  even_constrained_primes_composition (Some m) done.
  -m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
2 ≤ m by lia.
  -m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
m ≤ update (const 1) n (m + 1) n by rewrite update_eq; lia.
  -m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
Z.Even m done.
  -m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n: primes
transition (existT n radix_label)
  (update (const 1) n (m + 1), Some m) =
(const 1, Some (`n * m)) cbn; f_equal; extensionality j; cbn.m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n, j: primes
state_update (indexed_radix_vlsms (λ p : primes, `p))
  (update (const 1) n (m + 1)) n
  (update (const 1) n (m + 1) n - m) j = 1
    destruct (decide (n = j)); subst; state_update_simpl.m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
j: primes
update (const 1) j (m + 1) j - m = 1
m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n, j: primes
n0: n ≠ j
update (const 1) n (m + 1) j = 1
    +m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
j: primes
update (const 1) j (m + 1) j - m = 1 by rewrite update_eq; lia.
    +m: multiplying_message
H: valid_message_prop
  even_constrained_primes_composition m
H0: m >= 2
H1: Z.Even m
n, j: primes
n0: n ≠ j
update (const 1) n (m + 1) j = 1 by rewrite update_neq.
Qed.

Lemma even_constrained_primes_composition_valid_messages_left (m : Z) :
  m > 1 -> Z.Even m -> valid_message_prop even_constrained_primes_composition m.m: Z
m > 1
→ Z.Even m
  → valid_message_prop
      even_constrained_primes_composition m
Proof.m: Z
m > 1
→ Z.Even m
  → valid_message_prop
      even_constrained_primes_composition m
  intros Hm1 Hmeven.m: Z
Hm1: m > 1
Hmeven: Z.Even m
valid_message_prop even_constrained_primes_composition
  m
  assert (Hinit : composite_initial_message_prop (indexed_radix_vlsms (fun p : primes => `p)) 2)
    by (unshelve eexists (dexist 2 prime_2), (exist _ 2 _); done).m: Z
Hm1: m > 1
Hmeven: Z.Even m
Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
valid_message_prop even_constrained_primes_composition
  m
  destruct (decide (m = 2)) as [-> | Hm2]; [by apply initial_message_is_valid |].m: Z
Hm1: m > 1
Hmeven: Z.Even m
Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
Hm2: m ≠ 2
valid_message_prop even_constrained_primes_composition
  m
  destruct Hmeven as [n ->].n: Z
Hm1: 2 * n > 1
Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
Hm2: 2 * n ≠ 2
valid_message_prop even_constrained_primes_composition
  (2 * n)
  assert (Hn : 2 <= n) by lia.n: Z
Hm1: 2 * n > 1
Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
Hm2: 2 * n ≠ 2
Hn: 2 ≤ n
valid_message_prop even_constrained_primes_composition
  (2 * n)
  pose (P := fun n => valid_message_prop even_constrained_primes_composition (2 * n)).n: Z
Hm1: 2 * n > 1
Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
Hm2: 2 * n ≠ 2
Hn: 2 ≤ n
P:= λ n : Z,
  valid_message_prop
    even_constrained_primes_composition 
    (2 * n): Z → Prop
valid_message_prop even_constrained_primes_composition
  (2 * n)
  cut (P n); [done |].n: Z
Hm1: 2 * n > 1
Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
Hm2: 2 * n ≠ 2
Hn: 2 ≤ n
P:= λ n : Z,
  valid_message_prop
    even_constrained_primes_composition 
    (2 * n): Z → Prop
P n
  clear -Hn Hinit; revert n Hn; apply Zlt_lower_bound_ind; subst P; cbn; intros n Hind Hn.Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
n: Z
Hind: ∀ y : Z,
  2 ≤ y < n
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hn: 2 ≤ n
valid_message_prop even_constrained_primes_composition
  (2 * n)
  destruct (decide (prime n)) as [Hp | Hnp].Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
n: Z
Hind: ∀ y : Z,
  2 ≤ y < n
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hn: 2 ≤ n
Hp: prime n
valid_message_prop even_constrained_primes_composition
  (2 * n)
Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
n: Z
Hind: ∀ y : Z,
  2 ≤ y < n
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hn: 2 ≤ n
Hnp: ¬ prime n
valid_message_prop even_constrained_primes_composition
  (2 * n)
  -Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
n: Z
Hind: ∀ y : Z,
  2 ≤ y < n
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hn: 2 ≤ n
Hp: prime n
valid_message_prop even_constrained_primes_composition
  (2 * n) replace (2 * n) with (` (dexist n Hp) * 2) by (cbn; lia).Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
n: Z
Hind: ∀ y : Z,
  2 ≤ y < n
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hn: 2 ≤ n
Hp: prime n
valid_message_prop even_constrained_primes_composition
  (`(dexist n Hp) * 2)
    eapply input_valid_transition_out,
      even_constrained_primes_composition_emits_multiplier;
        [| done | by exists 1].Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
n: Z
Hind: ∀ y : Z,
  2 ≤ y < n
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hn: 2 ≤ n
Hp: prime n
valid_message_prop even_constrained_primes_composition
  2
    by apply initial_message_is_valid.
  -Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
n: Z
Hind: ∀ y : Z,
  2 ≤ y < n
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hn: 2 ≤ n
Hnp: ¬ prime n
valid_message_prop even_constrained_primes_composition
  (2 * n) apply not_prime_divide_prime in Hnp as (m & Hp & q & Hq & ->); [| by lia].Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
m, q: Z
Hq: 2 ≤ q < q * m
Hn: 2 ≤ q * m
Hind: ∀ y : Z,
  2 ≤ y < q * m
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hp: prime m
valid_message_prop even_constrained_primes_composition
  (2 * (q * m))
    replace (2 * (q * m)) with (` (dexist m Hp) * (2 * q)) by (cbn; lia).Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
m, q: Z
Hq: 2 ≤ q < q * m
Hn: 2 ≤ q * m
Hind: ∀ y : Z,
  2 ≤ y < q * m
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hp: prime m
valid_message_prop even_constrained_primes_composition
  (`(dexist m Hp) * (2 * q))
    eapply input_valid_transition_out,
      even_constrained_primes_composition_emits_multiplier;
      [| by lia | by eexists].Hinit: composite_initial_message_prop
  (indexed_radix_vlsms (λ p : primes, `p)) 2
m, q: Z
Hq: 2 ≤ q < q * m
Hn: 2 ≤ q * m
Hind: ∀ y : Z,
  2 ≤ y < q * m
  → valid_message_prop
      even_constrained_primes_composition
      (2 * y)
Hp: prime m
valid_message_prop even_constrained_primes_composition
  (2 * q)
    by apply Hind.
Qed.

The valid messages of the even_constrained_primes_composition are precisely all positive even numbers.

Lemma even_constrained_primes_composition_valid_message_char (m : Z) :
  valid_message_prop even_constrained_primes_composition m
    <->
  ((m > 1 /\ Z.Even m) \/ prime m).m: Z
valid_message_prop even_constrained_primes_composition
  m ↔ m > 1 ∧ Z.Even m ∨ prime m
Proof.m: Z
valid_message_prop even_constrained_primes_composition
  m ↔ m > 1 ∧ Z.Even m ∨ prime m
  split.m: Z
valid_message_prop even_constrained_primes_composition
  m → m > 1 ∧ Z.Even m ∨ prime m
m: Z
m > 1 ∧ Z.Even m ∨ prime m
→ valid_message_prop
    even_constrained_primes_composition m
  -m: Z
valid_message_prop even_constrained_primes_composition
  m → m > 1 ∧ Z.Even m ∨ prime m intros Hm.m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
m > 1 ∧ Z.Even m ∨ prime m
    cut (m > 1 /\ (Z.Even m \/ prime m)).m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
m > 1 ∧ (Z.Even m ∨ prime m)
→ m > 1 ∧ Z.Even m ∨ prime m
m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
m > 1 ∧ (Z.Even m ∨ prime m)
    {m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
m > 1 ∧ (Z.Even m ∨ prime m)
→ m > 1 ∧ Z.Even m ∨ prime m
      by destruct (decide (prime m)); [right | left; itauto].
    }m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
m > 1 ∧ (Z.Even m ∨ prime m)
    split.m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
m > 1
m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
Z.Even m ∨ prime m
    +m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
m > 1 apply primes_vlsm_composition_valid_message_char.m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
valid_message_prop primes_vlsm_composition m
      eapply VLSM_incl_valid_message; [..| done].m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
VLSM_incl_part
  (constrained_vlsm_machine primes_vlsm_composition
     EvenConstraint)
  (free_composite_vlsm_machine
     (indexed_radix_vlsms (λ p : primes, `p)))
m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
strong_incl_initial_message_preservation
  (constrained_vlsm_machine primes_vlsm_composition
     EvenConstraint)
  (free_composite_vlsm_machine
     (indexed_radix_vlsms (λ p : primes, `p)))
      *m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
VLSM_incl_part
  (constrained_vlsm_machine primes_vlsm_composition
     EvenConstraint)
  (free_composite_vlsm_machine
     (indexed_radix_vlsms (λ p : primes, `p))) by apply (VLSM_incl_constrained_vlsm primes_vlsm_composition).
      *m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
strong_incl_initial_message_preservation
  (constrained_vlsm_machine primes_vlsm_composition
     EvenConstraint)
  (free_composite_vlsm_machine
     (indexed_radix_vlsms (λ p : primes, `p))) by do 2 red.
    +m: Z
Hm: valid_message_prop
  even_constrained_primes_composition m
Z.Even m ∨ prime m apply emitted_messages_are_valid_iff in Hm
        as [([p Hp] & [i Hi] & <-) | ([s [im |]] & [i li] & s' & (_ & _ & _ & Hc) & Ht)];
        cbn in *; [by subst; right; apply bool_decide_spec in Hp | | done].m: Z
s: composite_state
  (indexed_radix_vlsms (λ p : primes, `p))
im: Z
i: primes
li: multiplying_label
s': composite_state
  (indexed_radix_vlsms (λ p : primes, `p))
Hc: EvenConstraint (existT i li) (s, Some im)
Ht: (state_update
   (indexed_radix_vlsms (λ p : primes, `p)) s i
   (s i - im), Some (`i * im)) = (s', Some m)
Z.Even m ∨ prime m
      inversion Hc; subst; clear Hc.m: Z
s: composite_state
  (indexed_radix_vlsms (λ p : primes, `p))
im: Z
i: primes
li: multiplying_label
s': composite_state
  (indexed_radix_vlsms (λ p : primes, `p))
Ht: (state_update
   (indexed_radix_vlsms (λ p : primes, `p)) s i
   (s i - im), Some (`i * im)) = (s', Some m)
H1: Z.Even im
Z.Even m ∨ prime m
      inversion Ht; subst; clear Ht.s: composite_state
  (indexed_radix_vlsms (λ p : primes, `p))
im: Z
i: primes
li: multiplying_label
H1: Z.Even im
Z.Even (`i * im) ∨ prime (`i * im)
      by left; apply Zeven_equiv, Zeven_mult_Zeven_r, Zeven_equiv.
  -m: Z
m > 1 ∧ Z.Even m ∨ prime m
→ valid_message_prop
    even_constrained_primes_composition m intros [[] | Hprime].m: Z
H: m > 1
H0: Z.Even m
valid_message_prop even_constrained_primes_composition
  m
m: Z
Hprime: prime m
valid_message_prop even_constrained_primes_composition
  m
    +m: Z
H: m > 1
H0: Z.Even m
valid_message_prop even_constrained_primes_composition
  m by apply even_constrained_primes_composition_valid_messages_left.
    +m: Z
Hprime: prime m
valid_message_prop even_constrained_primes_composition
  m apply initial_message_is_valid.m: Z
Hprime: prime m
initial_message_prop m
      by unshelve eexists (dexist m Hprime), (exist _ m _).
Qed.

No component is validating for the even_constrained_primes_composition.

Lemma even_constrained_primes_composition_no_validator :
  forall (p : primes),
    ~ component_projection_validator_prop
        (indexed_radix_vlsms (fun p : primes => ` p))
        EvenConstraint p.∀ p : primes,
  ¬ component_projection_validator_prop
      (indexed_radix_vlsms (λ p0 : primes, `p0))
      EvenConstraint p
Proof.∀ p : primes,
  ¬ component_projection_validator_prop
      (indexed_radix_vlsms (λ p0 : primes, `p0))
      EvenConstraint p
  intros p Hnv.p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
False
  cut (input_constrained (indexed_radix_vlsms (λ p0 : primes, `p0) p) () (3, Some 3)).p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
input_constrained
  (indexed_radix_vlsms (λ p0 : primes, `p0) p) ()
  (3, Some 3) → False
p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
input_constrained
  (indexed_radix_vlsms (λ p0 : primes, `p0) p) ()
  (3, Some 3)
  {p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
input_constrained
  (indexed_radix_vlsms (λ p0 : primes, `p0) p) ()
  (3, Some 3) → False
    intro Hiv.p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
Hiv: input_constrained (indexed_radix_vlsms (λ p0 : primes, `p0) p) () (3, Some 3)
False
    apply Hnv in Hiv as (s & _ & _ & _ & _ & Hc).p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
s: state
  (composite_vlsm
     (indexed_radix_vlsms (λ p : primes, `p))
     EvenConstraint)
Hc: EvenConstraint (existT p ()) (s, Some 3)
False
    by inversion Hc as [? ? ? []]; lia.
  }p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
input_constrained
  (indexed_radix_vlsms (λ p0 : primes, `p0) p) ()
  (3, Some 3)
  repeat split; [| by apply any_message_is_valid_in_preloaded | by lia..].p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
valid_state_prop
  (preloaded_with_all_messages_vlsm
     (indexed_radix_vlsms (λ p0 : primes, `p0) p)) 3
  apply initial_state_is_valid; cbn.p: primes
Hnv: component_projection_validator_prop (indexed_radix_vlsms (λ p : primes, `p))
EvenConstraint p
multiplying_initial_state_prop 3
  by red; lia.
Qed.

Now we show that if we constrain each component with a local condition equivalent to the global constraint we can recover validation.

Inductive LocalEvenConstraint (mult : Z) :
  label (radix_vlsm mult) -> state (radix_vlsm mult) * option Z -> Prop :=
| local_even_constraint : forall l s m, Z.Even m ->
    LocalEvenConstraint mult l (s, Some m).

Definition even_prime_vlsms (p : primes) : VLSM multiplying_message :=
  constrained_vlsm (radix_vlsm (`p)) (LocalEvenConstraint (`p)).

Adding the local constraint to each component does not change the behavior of the composition.

Lemma even_constrained_primes_composition_incl_left :
  VLSM_incl
    even_constrained_primes_composition
    (composite_vlsm even_prime_vlsms EvenConstraint).VLSM_incl even_constrained_primes_composition
  (composite_vlsm even_prime_vlsms EvenConstraint)
Proof.VLSM_incl even_constrained_primes_composition
  (composite_vlsm even_prime_vlsms EvenConstraint)
  apply basic_VLSM_strong_incl; cycle 3; [by intros ? **.. |].strong_incl_valid_preservation
  (constrained_vlsm_machine primes_vlsm_composition
     EvenConstraint)
  (constrained_vlsm_machine
     (free_composite_vlsm even_prime_vlsms)
     EvenConstraint)
  intros [p []] s [m |] [Hv Hc]; [| by inversion Hc]; cbn.p: primes
s: state
  {|
    vlsm_type := primes_vlsm_composition;
    vlsm_machine :=
      constrained_vlsm_machine
        primes_vlsm_composition EvenConstraint
  |}
m: Z
Hv: valid (existT p ()) (s, Some m)
Hc: EvenConstraint (existT p ()) (s, Some m)
(2 ≤ m ≤ s p
 ∧ LocalEvenConstraint (`p) () (s p, Some m))
∧ EvenConstraint (existT p ()) (s, Some m)
  split; [| done].p: primes
s: state
  {|
    vlsm_type := primes_vlsm_composition;
    vlsm_machine :=
      constrained_vlsm_machine
        primes_vlsm_composition EvenConstraint
  |}
m: Z
Hv: valid (existT p ()) (s, Some m)
Hc: EvenConstraint (existT p ()) (s, Some m)
2 ≤ m ≤ s p
∧ LocalEvenConstraint (`p) () (s p, Some m)
  split; [| by inversion Hc].p: primes
s: state
  {|
    vlsm_type := primes_vlsm_composition;
    vlsm_machine :=
      constrained_vlsm_machine
        primes_vlsm_composition EvenConstraint
  |}
m: Z
Hv: valid (existT p ()) (s, Some m)
Hc: EvenConstraint (existT p ()) (s, Some m)
2 ≤ m ≤ s p
  by destruct Hv.
Qed.

The validation result is recovered for the new constrained components and composition.

Theorem even_constrained_primes_composition_all_validators :
  forall (p : primes),
    component_projection_validator_prop even_prime_vlsms EvenConstraint p.∀ p : primes,
  component_projection_validator_prop even_prime_vlsms
    EvenConstraint p
Proof.∀ p : primes,
  component_projection_validator_prop even_prime_vlsms
    EvenConstraint p
  intros p lp sp [m |] (Hsp & _ & [[] Hc]).p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
valid lp (sp, Some m)
  inversion Hc as [? ? ? Heven]; subst.p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
valid lp (sp, Some m)
  exists (lift_to_composite_state' (indexed_radix_vlsms (fun p : primes => `p)) p sp).p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
lift_to_composite_state'
  (indexed_radix_vlsms (λ p : primes, `p)) p sp p = sp
∧ input_valid
    (composite_vlsm even_prime_vlsms EvenConstraint)
    (existT p lp)
    (lift_to_composite_state'
       (indexed_radix_vlsms (λ p : primes, `p)) p sp,
     Some m)
  repeat split; cycle 1; [| | by state_update_simpl..].p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
valid_state_prop
  (composite_vlsm even_prime_vlsms EvenConstraint)
  (lift_to_composite_state'
     (indexed_radix_vlsms (λ p : primes, `p)) p sp)
p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
option_valid_message_prop
  (composite_vlsm even_prime_vlsms EvenConstraint)
  (Some m)
  -p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
valid_state_prop
  (composite_vlsm even_prime_vlsms EvenConstraint)
  (lift_to_composite_state'
     (indexed_radix_vlsms (λ p : primes, `p)) p sp) apply initial_state_is_valid.p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
initial_state_prop
  (lift_to_composite_state'
     (indexed_radix_vlsms (λ p : primes, `p)) p sp)
    intro p'; cbn; red.p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
p': primes
lift_to_composite_state'
  (indexed_radix_vlsms (λ p : primes, `p)) p sp p' >=
1
    by destruct (decide (p = p')); subst; state_update_simpl; cbn; [lia |].
  -p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
option_valid_message_prop
  (composite_vlsm even_prime_vlsms EvenConstraint)
  (Some m) apply option_valid_message_Some.p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
valid_message_prop
  (composite_vlsm even_prime_vlsms EvenConstraint) m
    eapply VLSM_incl_valid_message;
      [by apply even_constrained_primes_composition_incl_left | ..].p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
strong_incl_initial_message_preservation
  even_constrained_primes_composition
  (constrained_vlsm_machine
     (free_composite_vlsm even_prime_vlsms)
     EvenConstraint)
p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
valid_message_prop
  {|
    vlsm_type := free_composite_vlsm even_prime_vlsms;
    vlsm_machine :=
      even_constrained_primes_composition
  |} m
    +p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
strong_incl_initial_message_preservation
  even_constrained_primes_composition
  (constrained_vlsm_machine
     (free_composite_vlsm even_prime_vlsms)
     EvenConstraint) by do 2 red.
    +p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
valid_message_prop
  {|
    vlsm_type := free_composite_vlsm even_prime_vlsms;
    vlsm_machine :=
      even_constrained_primes_composition
  |} m apply even_constrained_primes_composition_valid_message_char.p: primes
lp: label (even_prime_vlsms p)
sp: state (even_prime_vlsms p)
m: multiplying_message
Hsp: valid_state_prop (preloaded_with_all_messages_vlsm (even_prime_vlsms p)) sp
H: 2 ≤ m
H0: m ≤ sp
Hc: LocalEvenConstraint (`p) lp (sp, Some m)
Heven: Z.Even m
m > 1 ∧ Z.Even m ∨ prime m
      by left; split; [lia |].
Qed.

End sec_primes_vlsm_composition.