Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[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.

Tutorial: VLSMs that Multiply

This module demonstrates some basic notions of the VLSM framework.
We define a family of VLSMs that store an integer and continually decrement it using input messages (also integers), while a constraint is checked at each step. The definitions and lemmas tap into concepts such as valid and constrained traces, transitions, states, and messages.
The "doubling" VLSM has 2 as its only initial message and as output doubles the messages it receives as input. Therefore, constrained messages are positive even numbers (doubling_constrained_messages) and valid messages are powers of 2 (doubling_valid_messages_powers_of_2). Similarly, the "tripling" VLSM has 3 as its only initial message and as output triples the messages it receives as input.
When composing the doubling and tripling VLSMs, they become more than the sum of their parts: the free composition's valid messages are all integers which can be decomposed as a product of powers of 2 and 3.
#[local] Open Scope Z_scope.

Definition of common features of the multiplying VLSMs

The multiplying VLSMs have only one type of transition, decrementing their state and multiplying their input message as an output. For this reason, the unit type can be used as a label.
Definition multiplying_label : Type := unit.
The state will hold an integer.
Definition multiplying_state : Type := Z.
Messages are integers.
Definition multiplying_message : Type := Z.
A VLSM Type is defined using multiplying_state and multiplying_label.
Definition multiplying_type : VLSMType multiplying_message :=
{|
  state := multiplying_state;
  label := multiplying_label;
|}.
To improve readability, we explicitly define multiply_label as the value of the unit type.
Definition multiply_label : label multiplying_type := ().
The initial states of multiplying VLSMs will be positive integers.
Definition multiplying_initial_state_prop (st : multiplying_state) : Prop :=
  st >= 1.
We must also provide a proof that the intial state type is inhabited as the set of initial states is non-empty.
Definition multiplying_initial_state_type : Type :=
  {st : multiplying_state | multiplying_initial_state_prop st}.

Program Definition multiplying_initial_state :
  multiplying_initial_state_type := exist _ 1 _.

(λ st : multiplying_state, multiplying_initial_state_prop st) 1

(λ st : multiplying_state, multiplying_initial_state_prop st) 1
done. Defined. #[export] Instance multiplying_initial_state_type_inhabited : Inhabited (multiplying_initial_state_type) := populate (multiplying_initial_state).
The transition validity predicate is also common for all multiplying VLSMs: the message must exist, must be larger than 1, and not larger than the current state.
Definition multiplying_valid
  (l : multiplying_label) (st : multiplying_state) (om : option multiplying_message) : Prop :=
  match om with
  | Some msg => 2 <= msg <= st
  | None     => False
  end.

Definition of the doubling VLSM

The doubling VLSM is a multiplying VLSM whose initial message is 2 and which outputs the double of the received input, while using it to decrement the current state; the multiplying_valid constraint ensures that the valid/constraines states don't become negative.
Not that, since the transition function must be total, it must also be defined for the case in which no input is provided, although that case will be filtered out by the transition validity predicate.
Definition doubling_transition
  (l : multiplying_label) (st : multiplying_state) (om : option multiplying_message)
  : multiplying_state * option multiplying_message :=
  match om with
  | Some j  => (st - j, Some (2 * j))
  | None    => (st, None)
  end.
An intermediate representation for the VLSM is required. It uses the previously defined specifications with the addition that it states that 2 is the only initial message.
Definition doubling_machine : VLSMMachine multiplying_type :=
{|
  initial_state_prop := multiplying_initial_state_prop;
  initial_message_prop := fun (ms : multiplying_message) => ms = 2;
  s0 := multiplying_initial_state_type_inhabited;
  transition := fun l '(st, om) => doubling_transition l st om;
  valid := fun l '(st, om) => multiplying_valid l st om;
|}.
The definition of the doubling VLSM
Definition doubling_vlsm : VLSM multiplying_message :=
{|
  vlsm_type := multiplying_type;
  vlsm_machine := doubling_machine;
|}.

Doubling VLSM examples

Example of an arbitrary transition

X: VLSM multiplying_message

transition multiply_label (4, Some 10) = (-6, Some 20)
X: VLSM multiplying_message

transition multiply_label (4, Some 10) = (-6, Some 20)
done. Qed.

Example of a valid trace

The initial state cannot be included to this definition, because, since there is no transition reaching this state, it cannot be expressed in the below manner Regarding the transition which leads to the final state, it technically could be included, but we choose to model this way, in order to be consistent with the subsequent example, where adding the last transition makes a qualitative difference to the trace
Definition doubling_trace1_init : list (transition_item doubling_vlsm) :=
  [ Build_transition_item multiply_label (Some 4)
     4 (Some 8)
  ; Build_transition_item multiply_label (Some 2)
     2 (Some 4) ].

Definition doubling_trace1_last_item : transition_item doubling_vlsm :=
  Build_transition_item multiply_label (Some 2)
    0 (Some 4).

Definition doubling_trace1 : list (transition_item doubling_vlsm) :=
  doubling_trace1_init ++ [doubling_trace1_last_item].

Definition doubling_trace1_first_state : multiplying_state := 8.

Definition doubling_trace1_last_state : multiplying_state :=
  destination doubling_trace1_last_item.
Defined trace is valid:

valid_message_prop doubling_vlsm 2

valid_message_prop doubling_vlsm 2
by apply initial_message_is_valid. Qed.

can_emit doubling_vlsm 4

can_emit doubling_vlsm 4

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)

valid_state_prop doubling_vlsm 2

option_valid_message_prop doubling_vlsm (Some 2)

valid_state_prop doubling_vlsm 2
by apply initial_state_is_valid; cbn; unfold multiplying_initial_state_prop; lia.

option_valid_message_prop doubling_vlsm (Some 2)
by app_valid_tran. Qed.

valid_message_prop doubling_vlsm 4

valid_message_prop doubling_vlsm 4
by apply (emitted_messages_are_valid doubling_vlsm 4 doubling_can_emit_4). Qed.

input_valid_transition doubling_vlsm multiply_label (8, Some 4) (4, Some 8)

input_valid_transition doubling_vlsm multiply_label (8, Some 4) (4, Some 8)

valid_state_prop doubling_vlsm 8

option_valid_message_prop doubling_vlsm (Some 4)

24

valid_state_prop doubling_vlsm 8
by apply initial_state_is_valid; cbn; unfold multiplying_initial_state_prop, doubling_trace1_first_state; lia.

option_valid_message_prop doubling_vlsm (Some 4)
by apply doubling_valid_message_prop_4.

24
by unfold doubling_trace1_first_state; nia. Qed.

input_valid_transition doubling_vlsm multiply_label (4, Some 2) (2, Some 4)

input_valid_transition doubling_vlsm multiply_label (4, Some 2) (2, Some 4)

valid_state_prop doubling_vlsm 4

option_valid_message_prop doubling_vlsm (Some 2)

valid_state_prop doubling_vlsm 4
by app_valid_tran; eapply doubling_valid_transition_1; lia.

option_valid_message_prop doubling_vlsm (Some 2)
by apply doubling_valid_message_prop_2. Qed.

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)

valid_state_prop doubling_vlsm 2

option_valid_message_prop doubling_vlsm (Some 2)

valid_state_prop doubling_vlsm 2
by app_valid_tran; apply doubling_valid_transition_2.

option_valid_message_prop doubling_vlsm (Some 2)
by apply doubling_valid_message_prop_2. Qed.

finite_valid_trace_init_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1

finite_valid_trace_init_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1

finite_valid_trace_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1

finite_valid_trace_from_to doubling_vlsm 0 doubling_trace1_last_state []

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)

input_valid_transition doubling_vlsm multiply_label (4, Some 2) (2, Some 4)

input_valid_transition doubling_vlsm multiply_label (doubling_trace1_first_state, Some 4) (4, Some 8)

finite_valid_trace_from_to doubling_vlsm 0 doubling_trace1_last_state []
by eapply finite_valid_trace_from_to_empty, input_valid_transition_destination, doubling_valid_transition_3.

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)
by apply doubling_valid_transition_3.

input_valid_transition doubling_vlsm multiply_label (4, Some 2) (2, Some 4)
by apply doubling_valid_transition_2.

input_valid_transition doubling_vlsm multiply_label (doubling_trace1_first_state, Some 4) (4, Some 8)
by apply doubling_valid_transition_1. Qed.

finite_valid_trace_init_to_alt doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1

finite_valid_trace_init_to_alt doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1

message_valid_transitions_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1
by repeat apply mvt_extend; [.. | apply mvt_empty]; try done; [apply doubling_valid_message_prop_4 | apply doubling_valid_message_prop_2 ..]. Qed.

Example of a constrained trace

Previously defined trace is obviously constrained, since it's valid

finite_constrained_trace_init_to_direct doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1

finite_constrained_trace_init_to_direct doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1

constrained_transitions_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1
by repeat apply ct_extend; [.. | apply ct_empty]. Qed. Definition doubling_trace2_init : list (transition_item doubling_vlsm) := [ Build_transition_item multiply_label (Some 2) 5 (Some 4) ; Build_transition_item multiply_label (Some 2) 3 (Some 4) ]. Definition doubling_trace2_last_item : transition_item doubling_vlsm := Build_transition_item multiply_label (Some 3) 0 (Some 6). Definition doubling_trace2 : list (transition_item doubling_vlsm) := doubling_trace2_init ++ [doubling_trace2_last_item]. Definition doubling_trace2_init_first_state : multiplying_state := 7. Definition doubling_trace2_init_last_state : multiplying_state := 3. Definition doubling_trace2_last_state : multiplying_state := destination doubling_trace2_last_item.
The given trace is valid without the last transition.

input_valid_transition doubling_vlsm multiply_label (doubling_trace2_init_first_state, Some 2) (5, Some 4)

input_valid_transition doubling_vlsm multiply_label (doubling_trace2_init_first_state, Some 2) (5, Some 4)
by app_valid_tran. Qed.

input_valid_transition doubling_vlsm multiply_label (5, Some 2) (3, Some 4)

input_valid_transition doubling_vlsm multiply_label (5, Some 2) (3, Some 4)
by app_valid_tran; apply doubling_valid_transition_1'. Qed.

finite_valid_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

finite_valid_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

finite_valid_trace_from_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

finite_valid_trace_from_to doubling_vlsm 3 doubling_trace2_init_last_state []

input_valid_transition doubling_vlsm multiply_label (5, Some 2) (3, Some 4)

input_valid_transition doubling_vlsm multiply_label (doubling_trace2_init_first_state, Some 2) (5, Some 4)

finite_valid_trace_from_to doubling_vlsm 3 doubling_trace2_init_last_state []
by eapply finite_valid_trace_from_to_empty, input_valid_transition_destination, doubling_valid_transition_2'.

input_valid_transition doubling_vlsm multiply_label (5, Some 2) (3, Some 4)
by apply doubling_valid_transition_2'.

input_valid_transition doubling_vlsm multiply_label (doubling_trace2_init_first_state, Some 2) (5, Some 4)
by apply doubling_valid_transition_1'. Qed.

finite_valid_trace_init_to_alt doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

finite_valid_trace_init_to_alt doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

message_valid_transitions_from_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
by repeat apply mvt_extend; [..| apply mvt_empty]; try done; apply doubling_valid_message_prop_2. Qed.
From the previous lemmas, it follows that the given trace without its last transition is constrained.

finite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

finite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

VLSM_incl_part doubling_machine (preloaded_vlsm_machine doubling_vlsm (λ _ : multiplying_message, True))

finite_valid_trace_init_to {| vlsm_type := doubling_vlsm; vlsm_machine := doubling_machine |} doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init

VLSM_incl_part doubling_machine (preloaded_vlsm_machine doubling_vlsm (λ _ : multiplying_message, True))
by apply vlsm_incl_preloaded.

finite_valid_trace_init_to {| vlsm_type := doubling_vlsm; vlsm_machine := doubling_machine |} doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
by apply doubling_valid_trace2_init. Qed.
The trace is valid (in the preloaded doubling VLSM) without its last element and appending it to the end also gives a valid trace (in the preloaded doubling VLSM). It follows that the full trace is constrained in the original doubling VLSM.

finite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2

finite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2
H: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
H0: initial_state_prop doubling_trace2_init_first_state

finite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2
H: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
H0: initial_state_prop doubling_trace2_init_first_state

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2
H: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
H0: initial_state_prop doubling_trace2_init_first_state

input_valid_transition (preloaded_with_all_messages_vlsm doubling_vlsm) multiply_label (doubling_trace2_init_last_state, Some 3) (0, Some 6)
H: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
H0: initial_state_prop doubling_trace2_init_first_state

valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_last_state
H: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
H0: initial_state_prop doubling_trace2_init_first_state
option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 3)
H: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
H0: initial_state_prop doubling_trace2_init_first_state

valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_last_state
by eapply finite_valid_trace_from_to_last_pstate.
H: finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
H0: initial_state_prop doubling_trace2_init_first_state

option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 3)
by apply any_message_is_valid_in_preloaded. Qed.

Example of a valid transition

The last transition of a valid trace is valid.

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)

finite_valid_trace_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1
by apply doubling_valid_trace1. Qed.

Example of a constrained transition

The last transition of a constrained trace is constrained.

input_constrained_transition doubling_vlsm multiply_label (3, Some 3) (0, Some 6)

input_constrained_transition doubling_vlsm multiply_label (3, Some 3) (0, Some 6)

finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2
by apply doubling_constrained_trace2. Qed.

Doubling VLSM properties

Inclusion into preloaded with all messages


VLSM_incl doubling_vlsm (preloaded_with_all_messages_vlsm doubling_vlsm)

VLSM_incl doubling_vlsm (preloaded_with_all_messages_vlsm doubling_vlsm)
by apply vlsm_incl_preloaded_with_all_messages_vlsm. Qed.

Constrained messages are positive even integers


m : multiplying_message, constrained_message_prop doubling_vlsm m → Z.Even m ∧ m >= 4

m : multiplying_message, constrained_message_prop doubling_vlsm m → Z.Even m ∧ m >= 4
m: multiplying_message
s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
m0: multiplying_message
s': state (preloaded_with_all_messages_vlsm doubling_vlsm)
H: 2 ≤ m0
H0: m0 ≤ s
Ht: transition () (s, Some m0) = (s', Some m)

Z.Even m ∧ m >= 4
s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
m0: multiplying_message
H: 2 ≤ m0
H0: m0 ≤ s
Ht: transition () (s, Some m0) = (s - m0, Some (2 * m0))

Z.Even (2 * m0) ∧ 2 * m0 >= 4
by split; [eexists | lia]. Qed.

m : multiplying_message, Z.Even m → m >= 4 → constrained_message_prop doubling_vlsm m

m : multiplying_message, Z.Even m → m >= 4 → constrained_message_prop doubling_vlsm m
n: Z
Hmgt0: 2 * n >= 4

constrained_message_prop doubling_vlsm (2 * n)
n: Z
Hmgt0: 2 * n >= 4

input_valid_transition (preloaded_with_all_messages_vlsm doubling_vlsm) multiply_label (n, Some n) (0, Some (2 * n))
n: Z
Hmgt0: 2 * n >= 4

valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) n
n: Z
Hmgt0: 2 * n >= 4
option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some n)
n: Z
Hmgt0: 2 * n >= 4

valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) n
apply initial_state_is_valid; cbn; red; lia.
n: Z
Hmgt0: 2 * n >= 4

option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some n)
by apply any_message_is_valid_in_preloaded. Qed.

m : multiplying_message, constrained_message_prop doubling_vlsm m ↔ Z.Even m ∧ m >= 4

m : multiplying_message, constrained_message_prop doubling_vlsm m ↔ Z.Even m ∧ m >= 4
m: multiplying_message

constrained_message_prop doubling_vlsm m → Z.Even m ∧ m >= 4
m: multiplying_message
Z.Even m ∧ m >= 4 → constrained_message_prop doubling_vlsm m
m: multiplying_message

constrained_message_prop doubling_vlsm m → Z.Even m ∧ m >= 4
by apply doubling_constrained_messages_left.
m: multiplying_message

Z.Even m ∧ m >= 4 → constrained_message_prop doubling_vlsm m
by intros [? ?]; apply doubling_constrained_messages_right. Qed.

Constrained states property


st : multiplying_state, constrained_state_prop doubling_vlsm st → st >= 0

st : multiplying_state, constrained_state_prop doubling_vlsm st → st >= 0
s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
Hs: initial_state_prop s

s >= 0
s': state (preloaded_with_all_messages_vlsm doubling_vlsm)
l: label (preloaded_with_all_messages_vlsm doubling_vlsm)
om, om': option multiplying_message
s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm doubling_vlsm) l (s, om) (s', om')
IHvalid_state_prop: s >= 0
s' >= 0
s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
Hs: initial_state_prop s

s >= 0
cbn in Hs; red in Hs; lia.
s': state (preloaded_with_all_messages_vlsm doubling_vlsm)
l: label (preloaded_with_all_messages_vlsm doubling_vlsm)
om, om': option multiplying_message
s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
Ht: input_valid_transition (preloaded_with_all_messages_vlsm doubling_vlsm) l (s, om) (s', om')
IHvalid_state_prop: s >= 0

s' >= 0
s': state (preloaded_with_all_messages_vlsm doubling_vlsm)
m: multiplying_message
om': option multiplying_message
s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
Hs: valid_state_prop (preloaded_with_all_messages_vlsm doubling_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.

st : multiplying_state, st >= 0 → constrained_state_prop doubling_vlsm st

st : multiplying_state, st >= 0 → constrained_state_prop doubling_vlsm st
st: multiplying_state
Hst: st >= 0

constrained_state_prop doubling_vlsm st
st: multiplying_state
Hst: st >= 0

input_valid_transition (preloaded_with_all_messages_vlsm doubling_vlsm) multiply_label (st + 2, Some 2) (st, Some 4)
st: multiplying_state
Hst: st >= 0

valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (st + 2)
st: multiplying_state
Hst: st >= 0
option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 2)
st: multiplying_state
Hst: st >= 0

valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (st + 2)
apply initial_state_is_valid; cbn; red; lia.
st: multiplying_state
Hst: st >= 0

option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 2)
by apply any_message_is_valid_in_preloaded. Qed.

st : multiplying_state, constrained_state_prop doubling_vlsm st ↔ st >= 0

st : multiplying_state, constrained_state_prop doubling_vlsm st ↔ st >= 0
st: multiplying_state

constrained_state_prop doubling_vlsm st → st >= 0
st: multiplying_state
st >= 0 → constrained_state_prop doubling_vlsm st
st: multiplying_state

constrained_state_prop doubling_vlsm st → st >= 0
by apply doubling_constrained_states_right.
st: multiplying_state

st >= 0 → constrained_state_prop doubling_vlsm st
by apply doubling_constrained_states_left. Qed.

Powers of 2 greater than or equal to 2 are valid messages


m : multiplying_message, valid_message_prop doubling_vlsm m → p : Z, p >= 1 ∧ m = 2 ^ p

m : multiplying_message, valid_message_prop doubling_vlsm m → p : Z, p >= 1 ∧ m = 2 ^ p
m: multiplying_message
s: state doubling_vlsm
Hvsm: valid_state_message_prop doubling_vlsm s (Some m)

p : Z, p >= 1 ∧ m = 2 ^ p
m: multiplying_message
s: state doubling_vlsm
Hvsm: valid_state_message_prop doubling_vlsm s (Some m)
Hom: is_Some (Some m)

p : Z, p >= 1 ∧ m = 2 ^ p
m: multiplying_message
s: state doubling_vlsm
Hvsm: valid_state_message_prop doubling_vlsm s (Some m)
Hom: is_Some (Some m)

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
m: multiplying_message
s: state doubling_vlsm
om: option multiplying_message
Hvsm: valid_state_message_prop doubling_vlsm s om
Hom: is_Some om

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: state doubling_vlsm
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop doubling_vlsm om
Hom: is_Some om

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
om: option multiplying_message
Hvsm2: valid_state_message_prop doubling_vlsm _s om
l: label doubling_vlsm
Hv: valid l (s, om)
s': state doubling_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 = 2 ^ p
IHHvsm2: Hom : is_Some om, p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: state doubling_vlsm
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop doubling_vlsm om
Hom: is_Some om

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: multiplying_state
Hs: multiplying_initial_state_prop s

p : Z, p >= 12 = 2 ^ p
by exists 1; split; lia.
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
om: option multiplying_message
Hvsm2: valid_state_message_prop doubling_vlsm _s om
l: label doubling_vlsm
Hv: valid l (s, om)
s': state doubling_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 = 2 ^ p
IHHvsm2: Hom : is_Some om, p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
m: multiplying_message
Hvsm2: valid_state_message_prop doubling_vlsm _s (Some m)
l: label doubling_vlsm
Hv: valid l (s, Some m)
s': state doubling_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 = 2 ^ p
IHHvsm2: Hom : is_Some (Some m), p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
m: multiplying_message
Hvsm2: valid_state_message_prop doubling_vlsm _s (Some m)
l: label doubling_vlsm
Hv: valid l (s, Some m)
s': state doubling_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 = 2 ^ p
IHHvsm2: Hom : is_Some (Some m), p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
x: Z
Hx: x >= 1 ∧ is_Some_proj (ex_intro (λ x : multiplying_message, Some m = Some x) m eq_refl) = 2 ^ x

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
m: multiplying_message
Hvsm2: valid_state_message_prop doubling_vlsm _s (Some m)
l: label doubling_vlsm
Hv: valid l (s, Some m)
Hom: is_Some (Some (2 * m))
IHHvsm1: Hom : is_Some _om, p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
IHHvsm2: Hom : is_Some (Some m), p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
x: Z
Hx: x >= 1 ∧ is_Some_proj (ex_intro (λ x : multiplying_message, Some m = Some x) m eq_refl) = 2 ^ x

p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
x: Z
Hvsm2: valid_state_message_prop doubling_vlsm _s (Some (2 ^ x))
l: label doubling_vlsm
Hom: is_Some (Some (2 * 2 ^ x))
Hv: valid l (s, Some (2 ^ x))
IHHvsm1: Hom : is_Some _om, p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
IHHvsm2: Hom : is_Some (Some (2 ^ x)), p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
Hgeq1: x >= 1

p : Z, p >= 12 * 2 ^ x = 2 ^ p
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
x: Z
Hvsm2: valid_state_message_prop doubling_vlsm _s (Some (2 ^ x))
l: label doubling_vlsm
Hom: is_Some (Some (2 * 2 ^ x))
Hv: valid l (s, Some (2 ^ x))
IHHvsm1: Hom : is_Some _om, p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
IHHvsm2: Hom : is_Some (Some (2 ^ x)), p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
Hgeq1: x >= 1

x + 1 >= 12 * 2 ^ x = 2 ^ (x + 1)
s: state doubling_vlsm
_om: option multiplying_message
Hvsm1: valid_state_message_prop doubling_vlsm s _om
_s: state doubling_vlsm
x: Z
Hvsm2: valid_state_message_prop doubling_vlsm _s (Some (2 ^ x))
l: label doubling_vlsm
Hom: is_Some (Some (2 * 2 ^ x))
Hv: valid l (s, Some (2 ^ x))
IHHvsm1: Hom : is_Some _om, p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
IHHvsm2: Hom : is_Some (Some (2 ^ x)), p : Z, p >= 1 ∧ is_Some_proj Hom = 2 ^ p
Hgeq1: x >= 1

2 * 2 ^ x = 2 ^ (x + 1)
by rewrite <- Z.pow_succ_r; [| lia]. Qed.

p : Z, p >= 1 → valid_message_prop doubling_vlsm (2 ^ p)

p : Z, p >= 1 → valid_message_prop doubling_vlsm (2 ^ p)
p: Z
Hp: p >= 1

valid_message_prop doubling_vlsm (2 ^ p)
p: Z
Hp: p >= 1
Hle: 0 ≤ p - 1

valid_message_prop doubling_vlsm (2 ^ p)
p: Z
Hp: p >= 1
Hle: 0 ≤ p - 1

valid_message_prop doubling_vlsm (2 ^ (p - 1 + 1))
p: Z
Hp: p >= 1
x: Z
Heqx: x = p - 1
Hle: 0 ≤ x

valid_message_prop doubling_vlsm (2 ^ (x + 1))
x: Z
Hle: 0 ≤ x

valid_message_prop doubling_vlsm (2 ^ (x + 1))

x : Z, 0 ≤ x → valid_message_prop doubling_vlsm (2 ^ (x + 1))

x : Z, 0 ≤ x → valid_message_prop doubling_vlsm (2 ^ (x + 1)) → valid_message_prop doubling_vlsm (2 ^ (Z.succ x + 1))
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

valid_message_prop doubling_vlsm (2 ^ (Z.succ x + 1))
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

can_emit doubling_vlsm (2 ^ (Z.succ x + 1))
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

input_valid_transition doubling_vlsm multiply_label (2 ^ (x + 1), Some (2 ^ (x + 1))) (0, Some (2 ^ (Z.succ x + 1)))
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

valid_state_prop doubling_vlsm (2 ^ (x + 1))
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))
option_valid_message_prop doubling_vlsm (Some (2 ^ (x + 1)))
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))
22 ^ (x + 1)
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))
2 ^ (x + 1) ≤ 2 ^ (x + 1)
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))
transition multiply_label (2 ^ (x + 1), Some (2 ^ (x + 1))) = (0, Some (2 ^ (Z.succ x + 1)))
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

valid_state_prop doubling_vlsm (2 ^ (x + 1))
by apply initial_state_is_valid; cbn; red; lia.
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

option_valid_message_prop doubling_vlsm (Some (2 ^ (x + 1)))
by apply Hindh.
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

22 ^ (x + 1)
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

22 ^ Z.succ x
by rewrite Z.pow_succ_r; lia.
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

2 ^ (x + 1) ≤ 2 ^ (x + 1)
by lia.
x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))

transition multiply_label (2 ^ (x + 1), Some (2 ^ (x + 1))) = (0, Some (2 ^ (Z.succ x + 1)))
by cbn; rewrite <- Z.pow_succ_r, Z.add_succ_l; [do 2 f_equal; lia | lia]. Qed.

m : multiplying_message, valid_message_prop doubling_vlsm m ↔ ( p : Z, p >= 1 ∧ m = 2 ^ p)

m : multiplying_message, valid_message_prop doubling_vlsm m ↔ ( p : Z, p >= 1 ∧ m = 2 ^ p)
m: multiplying_message

valid_message_prop doubling_vlsm m → p : Z, p >= 1 ∧ m = 2 ^ p
m: multiplying_message
( p : Z, p >= 1 ∧ m = 2 ^ p) → valid_message_prop doubling_vlsm m
m: multiplying_message

valid_message_prop doubling_vlsm m → p : Z, p >= 1 ∧ m = 2 ^ p
by intros; apply doubling_valid_messages_powers_of_2_right.
m: multiplying_message

( p : Z, p >= 1 ∧ m = 2 ^ p) → valid_message_prop doubling_vlsm m
by intros (p & Hpgt0 & [= ->]); apply doubling_valid_messages_powers_of_2_left. Qed.
The constrained transition from doubling_example_constrained_transition is not also valid.

¬ input_valid_transition doubling_vlsm multiply_label (3, Some 3) (0, Some 6)

¬ input_valid_transition doubling_vlsm multiply_label (3, Some 3) (0, Some 6)
Hm: option_valid_message_prop doubling_vlsm (Some 3)

False
p: Z
Hp: p >= 1
Heq: 3 = 2 ^ p

False
p: Z
Hp: p >= 1
Heq: 3 = 2 ^ Z.succ (Z.pred p)

False
by rewrite Z.pow_succ_r in Heq; lia. Qed.

Valid states hold non-negative integers

s: multiplying_state

valid_state_prop doubling_vlsm s → s >= 0
s: multiplying_state

valid_state_prop doubling_vlsm s → s >= 0
s': state doubling_vlsm
l: label doubling_vlsm
om, om': option multiplying_message
s: state doubling_vlsm
Ht: input_valid_transition doubling_vlsm l (s, om) (s', om')
IHvalid_state_prop: s >= 0

s' >= 0
s': state doubling_vlsm
m: multiplying_message
om': option multiplying_message
s: state doubling_vlsm
Hs: valid_state_prop doubling_vlsm s
Hm: option_valid_message_prop doubling_vlsm (Some m)
Hv: valid () (s, Some m)
Ht: transition () (s, Some m) = (s', om')
IHvalid_state_prop: s >= 0

s' >= 0
m: multiplying_message
s: state doubling_vlsm
Hs: valid_state_prop doubling_vlsm s
Hm: option_valid_message_prop doubling_vlsm (Some m)
Hv: valid () (s, Some m)
Ht: transition () (s, Some m) = (s - m, Some (2 * m))
IHvalid_state_prop: s >= 0

s - m >= 0
by destruct Hv; lia. Qed.
s: multiplying_state

s >= 0 → valid_state_prop doubling_vlsm s
s: multiplying_state

s >= 0 → valid_state_prop doubling_vlsm s
s: multiplying_state
H: s >= 0

valid_state_prop doubling_vlsm s
H: 0 >= 0

valid_state_prop doubling_vlsm 0
H: 0 >= 0

input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)
H: 0 >= 0

valid_state_prop doubling_vlsm 2
H: 0 >= 0
option_valid_message_prop doubling_vlsm (Some 2)
H: 0 >= 0

valid_state_prop doubling_vlsm 2
by apply initial_state_is_valid; cbn; red; lia.
H: 0 >= 0

option_valid_message_prop doubling_vlsm (Some 2)
by apply initial_message_is_valid. Qed.

s : multiplying_state, valid_state_prop doubling_vlsm s ↔ s >= 0

s : multiplying_state, valid_state_prop doubling_vlsm s ↔ s >= 0
s: multiplying_state

valid_state_prop doubling_vlsm s → s >= 0
s: multiplying_state
s >= 0 → valid_state_prop doubling_vlsm s
s: multiplying_state

valid_state_prop doubling_vlsm s → s >= 0
by apply doubling_valid_states_right.
s: multiplying_state

s >= 0 → valid_state_prop doubling_vlsm s
by apply doubling_valid_states_left. Qed.

Definition of the tripling VLSM

Similarly to the doubling VLSM, the tripling VLSM is a multiplying VLSM, differing only by the fact that its initial message is 3 and that it outputs the triple of the received input.
It can be shown that its constrained messages are multiples of three and that its valid messages are powers of three, but the proofs will be similar to those for the doubling VLSM so we will omit them. The development in module PrimesComposition will make the results for the doubling and tripling VLSM be particular instances of more general results.
Definition tripling_transition
  (l : multiplying_label) (st : multiplying_state) (om : option multiplying_message)
  : multiplying_state * option multiplying_message :=
  match om with
  | Some j  => (st - j, Some (3 * j))
  | None    => (st, None)
  end.

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

Definition tripling_vlsm : VLSM multiplying_message := mk_vlsm tripling_machine.

Composition of doubling and tripling VLSMs

Section sec_23_composition.
Since our notion of composite_vlsm is based on an indexed set of components, we need to define a base index type
Inductive index23 := two | three.


EqDecision index23

EqDecision index23
by intros x y; unfold Decision; decide equality. Qed. Definition components_23 (i : index23) : VLSM multiplying_message := match i with | two => doubling_vlsm | three => tripling_vlsm end.
We define a helper function to make composite state easier to write.
Definition state_23 (n m : Z) : composite_state components_23 :=
  fun (i : index23) => match i with two => n | three => m end.

Definition state00 := state_23 0 0.

Definition state01 := state_23 0 1.

Definition state10 := state_23 1 0.

Definition state11 := state_23 1 1.

Definition state12 := state_23 1 2.

Definition state21 := state_23 2 1.

Definition state22 := state_23 2 2.

Definition state02 := state_23 0 2.

Definition zproj (s : composite_state components_23) (i : index23) : Z :=
  match i with
  | two => s two
  | three => s three
  end.

Definition free_composition_23 : VLSM multiplying_message :=
  free_composite_vlsm components_23.


composite_initial_message_prop components_23 2

composite_initial_message_prop components_23 2
by exists two; unshelve eexists (exist _ 2 _); cbn; lia. Qed.

composite_initial_message_prop components_23 3

composite_initial_message_prop components_23 3
by exists three; unshelve eexists (exist _ 3 _); cbn; lia. Qed.

m : multiplying_message, valid_message_prop free_composition_23 m → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

m : multiplying_message, valid_message_prop free_composition_23 m → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
m: multiplying_message
s: state free_composition_23
Hvsm: valid_state_message_prop free_composition_23 s (Some m)

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
m: multiplying_message
s: state free_composition_23
Hvsm: valid_state_message_prop free_composition_23 s (Some m)
Hom: is_Some (Some m)

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
m: multiplying_message
s: state free_composition_23
Hvsm: valid_state_message_prop free_composition_23 s (Some m)
Hom: is_Some (Some m)

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
m: multiplying_message
s: state free_composition_23
om: option multiplying_message
Hvsm: valid_state_message_prop free_composition_23 s om
Hom: is_Some om

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: state free_composition_23
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop free_composition_23 om
Hom: is_Some om

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: state free_composition_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: state free_composition_23
om: option multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s om
l: label free_composition_23
Hv: valid l (s, om)
s': state free_composition_23
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: Hom : is_Some om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: state free_composition_23
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop free_composition_23 om
Hom: is_Some om

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
m: multiplying_message
Hom0: composite_initial_message_prop components_23 m

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
x: multiplying_message
i: x = 2

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ x = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
x: multiplying_message
i: x = 3
p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ x = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
x: multiplying_message
i: x = 2

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ x = 2 ^ p2 * 3 ^ p3
by exists 1, 0; split; lia.
s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
x: multiplying_message
i: x = 3

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ x = 2 ^ p2 * 3 ^ p3
by exists 0, 1; split; lia.
s: state free_composition_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: state free_composition_23
om: option multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s om
l: label free_composition_23
Hv: valid l (s, om)
s': state free_composition_23
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: Hom : is_Some om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s two
Hom: is_Some (Some (2 * m))
Ht: (state_update components_23 s two (s two - m), Some (2 * m)) = (state_update components_23 s two (s two - m), Some (2 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 12 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 13 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s two
Hom: is_Some (Some (2 * m))
Ht: (state_update components_23 s two (s two - m), Some (2 * m)) = (state_update components_23 s two (s two - m), Some (2 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 12 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s two
Hom: is_Some (Some (2 * m))
Ht: (state_update components_23 s two (s two - m), Some (2 * m)) = (state_update components_23 s two (s two - m), Some (2 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

Z.succ p2 >= 0 ∧ p3 >= 0 ∧ Z.succ p2 + p3 >= 12 * m = 2 ^ Z.succ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s two
Hom: is_Some (Some (2 * m))
Ht: (state_update components_23 s two (s two - m), Some (2 * m)) = (state_update components_23 s two (s two - m), Some (2 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

p3 >= 0 ∧ Z.succ p2 + p3 >= 12 * m = 2 ^ Z.succ p2 * 3 ^ p3
by rewrite Z.pow_succ_r; lia.
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 13 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

p2 >= 0 ∧ Z.succ p3 >= 0 ∧ p2 + Z.succ p3 >= 13 * m = 2 ^ p2 * 3 ^ Z.succ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop free_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop free_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
IHHvsm2: is_Some (Some m) → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
p2, p3: Z
Hgt1: p2 >= 0
Heq: p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3

Z.succ p3 >= 0 ∧ p2 + Z.succ p3 >= 13 * m = 2 ^ p2 * 3 ^ Z.succ p3
by rewrite Z.pow_succ_r; lia. Qed.

p2 p3 : Z, p2 >= 0 → p3 >= 01 ≤ p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)

p2 p3 : Z, p2 >= 0 → p3 >= 01 ≤ p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p2, p3: Z
Hp2: p2 >= 0
Hp3: p3 >= 0
Hp: 1 ≤ p2 + p3

valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p2, p3: Z
Hp2: p2 >= 0
Hp3: p3 >= 0
p: Z
Heqp: p = p2 + p3
Hp: 1 ≤ p

valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p: Z
Hp: 1 ≤ p

p2 p3 : Z, p2 >= 0 → p3 >= 0 → p = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p: Z
Hp: 1 ≤ p
P:= λ p : Z, p2 p3 : Z, p2 >= 0 → p3 >= 0 → p = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3): Z → Prop

p2 p3 : Z, p2 >= 0 → p3 >= 0 → p = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p: Z
Hp: 1 ≤ p
P:= λ p : Z, p2 p3 : Z, p2 >= 0 → p3 >= 0 → p = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3): Z → Prop

P p

x : Z, ( y : Z, 1 ≤ y < x → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)) → 1 ≤ x → p2 p3 : Z, p2 >= 0 → p3 >= 0 → x = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0

valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0

valid_message_prop free_composition_23 (2 ^ 0 * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ 0)
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0
valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0

valid_message_prop free_composition_23 (2 ^ 0 * 3 ^ p3)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

valid_message_prop free_composition_23 (2 ^ 0 * 3 ^ p3)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

can_emit free_composition_23 (2 ^ 0 * 3 ^ p3)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

input_valid_transition free_composition_23 (existT three multiply_label) (state_23 1 (3 ^ (p3 - 1)), Some (3 ^ (p3 - 1))) (state10, Some (2 ^ 0 * 3 ^ p3))
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

valid_state_prop free_composition_23 (state_23 1 (3 ^ (p3 - 1)))
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1
option_valid_message_prop free_composition_23 (Some (3 ^ (p3 - 1)))
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1
23 ^ (p3 - 1)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1
3 ^ (p3 - 1) ≤ state_23 1 (3 ^ (p3 - 1)) three
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1
transition (existT three multiply_label) (state_23 1 (3 ^ (p3 - 1)), Some (3 ^ (p3 - 1))) = (state10, Some (2 ^ 0 * 3 ^ p3))
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

valid_state_prop free_composition_23 (state_23 1 (3 ^ (p3 - 1)))
by apply initial_state_is_valid; intros []; cbn; red; lia.
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

option_valid_message_prop free_composition_23 (Some (3 ^ (p3 - 1)))
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

option_valid_message_prop free_composition_23 (Some (2 ^ 0 * 3 ^ (p3 - 1)))
by eapply Hind; cycle 3; [done | lia..].
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

23 ^ (p3 - 1)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

23 ^ Z.succ (p3 - 2)
by rewrite Z.pow_succ_r; lia.
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

3 ^ (p3 - 1) ≤ state_23 1 (3 ^ (p3 - 1)) three
by cbn; lia.
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

transition (existT three multiply_label) (state_23 1 (3 ^ (p3 - 1)), Some (3 ^ (p3 - 1))) = (state10, Some (2 ^ 0 * 3 ^ p3))
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

state_update components_23 (state_23 1 (3 ^ (p3 - 1))) three (3 ^ (p3 - 1) - 3 ^ (p3 - 1)) = state10
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1
Some (3 * 3 ^ (p3 - 1)) = Some (2 ^ 0 * 3 ^ p3)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

state_update components_23 (state_23 1 (3 ^ (p3 - 1))) three (3 ^ (p3 - 1) - 3 ^ (p3 - 1)) = state10
by extensionality i; destruct i; state_update_simpl; cbn; lia.
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

Some (3 * 3 ^ (p3 - 1)) = Some (2 ^ 0 * 3 ^ p3)
p3: Z
Hp2: 0 >= 0
Hind: y : Z, 1 ≤ y < 0 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 10 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1

Some (3 * 3 ^ (p3 - 1)) = Some (2 ^ 0 * 3 ^ Z.succ (p3 - 1))
by f_equal; rewrite Z.pow_succ_r; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0

valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ 0)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ 0)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

can_emit free_composition_23 (2 ^ p2 * 3 ^ 0)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

input_valid_transition free_composition_23 (existT two multiply_label) (state_23 (2 ^ (p2 - 1)) 1, Some (2 ^ (p2 - 1))) (state01, Some (2 ^ p2 * 3 ^ 0))
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

valid_state_prop free_composition_23 (state_23 (2 ^ (p2 - 1)) 1)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1
option_valid_message_prop free_composition_23 (Some (2 ^ (p2 - 1)))
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1
22 ^ (p2 - 1)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1
2 ^ (p2 - 1) ≤ state_23 (2 ^ (p2 - 1)) 1 two
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1
transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1)) 1, Some (2 ^ (p2 - 1))) = (state01, Some (2 ^ p2 * 3 ^ 0))
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

valid_state_prop free_composition_23 (state_23 (2 ^ (p2 - 1)) 1)
by apply initial_state_is_valid; intros []; cbn; red; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

option_valid_message_prop free_composition_23 (Some (2 ^ (p2 - 1)))
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

option_valid_message_prop free_composition_23 (Some (2 ^ (p2 - 1) * 3 ^ 0))
by eapply Hind; cycle 3; [done | lia..].
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

22 ^ (p2 - 1)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

22 ^ Z.succ (p2 - 2)
by rewrite Z.pow_succ_r; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

2 ^ (p2 - 1) ≤ state_23 (2 ^ (p2 - 1)) 1 two
by cbn; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1)) 1, Some (2 ^ (p2 - 1))) = (state01, Some (2 ^ p2 * 3 ^ 0))
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

state_update components_23 (state_23 (2 ^ (p2 - 1)) 1) two (2 ^ (p2 - 1) - 2 ^ (p2 - 1)) = state01
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1
Some (2 * 2 ^ (p2 - 1)) = Some (2 ^ p2 * 3 ^ 0)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

state_update components_23 (state_23 (2 ^ (p2 - 1)) 1) two (2 ^ (p2 - 1) - 2 ^ (p2 - 1)) = state01
by extensionality i; destruct i; state_update_simpl; cbn; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

Some (2 * 2 ^ (p2 - 1)) = Some (2 ^ p2 * 3 ^ 0)
p2: Z
Hind: y : Z, 1 ≤ y < p2 + 0 p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp: 1 ≤ p2 + 0
Hp2: p2 >= 0
Hp3: 0 >= 0
n: p2 ≠ 0
n0: p2 ≠ 1

Some (2 * 2 ^ (p2 - 1)) = Some (2 ^ Z.succ (p2 - 1) * 3 ^ 0)
by f_equal; rewrite Z.pow_succ_r; lia.
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

can_emit free_composition_23 (2 ^ p2 * 3 ^ p3)
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

input_valid_transition free_composition_23 (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) (state01, Some (2 ^ p2 * 3 ^ p3))
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

valid_state_prop free_composition_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1)
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0
option_valid_message_prop free_composition_23 (Some (2 ^ (p2 - 1) * 3 ^ p3))
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0
22 ^ (p2 - 1) * 3 ^ p3
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0
2 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 two
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0
transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) = (state01, Some (2 ^ p2 * 3 ^ p3))
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

valid_state_prop free_composition_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1)
by apply initial_state_is_valid; intros []; cbn; red; lia.
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

option_valid_message_prop free_composition_23 (Some (2 ^ (p2 - 1) * 3 ^ p3))
by eapply Hind; cycle 3; [done | lia..].
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

22 ^ (p2 - 1) * 3 ^ p3
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

22 ^ (p2 - 1) * 3 ^ Z.succ (p3 - 1)
by rewrite Z.pow_succ_r; lia.
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

2 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 two
by cbn; lia.
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) = (state01, Some (2 ^ p2 * 3 ^ p3))
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0
Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01
by extensionality i; destruct i; state_update_simpl; cbn; lia.
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)
p2, p3: Z
Hp: 1 ≤ p2 + p3
Hind: y : Z, 1 ≤ y < p2 + p3 → p2 p3 : Z, p2 >= 0 → p3 >= 0 → y = p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: p2 >= 0
Hp3: p3 >= 0
n: p2 ≠ 0
n0: p3 ≠ 0

Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ Z.succ (p2 - 1) * 3 ^ p3)
by f_equal; rewrite Z.pow_succ_r; lia. Qed.
The valid messages of the free_composition_23 VLSM consist of all integers larger than 1 which can be decomposed as a product of powers of 2 and 3.

m : multiplying_message, valid_message_prop free_composition_23 m ↔ ( p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3)

m : multiplying_message, valid_message_prop free_composition_23 m ↔ ( p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3)
m: multiplying_message

valid_message_prop free_composition_23 m → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
m: multiplying_message
( p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop free_composition_23 m
m: multiplying_message

valid_message_prop free_composition_23 m → p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3
by apply free_composition_23_valid_messages_powers_of_23_right.
m: multiplying_message

( p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop free_composition_23 m
x, x0: Z
H: x >= 0
H0: x0 >= 0
H1: x + x0 >= 1

valid_message_prop free_composition_23 (2 ^ x * 3 ^ x0)
by eapply free_composition_23_valid_messages_powers_of_23_left; lia. Qed. Section sec_state_update_23_def. Context (s : composite_state components_23) (i : index23) (z : Z) . Definition state_update_23 (j : index23) : state (components_23 j) := if (decide (i = j)) then match j with | two => z | three => z end else s j.
s: composite_state components_23
i: index23
z: Z

zproj state_update_23 i = z
s: composite_state components_23
i: index23
z: Z

zproj state_update_23 i = z
by unfold state_update_23; destruct i; cbn; rewrite decide_True. Qed.
s: composite_state components_23
i: index23
z: Z

j : index23, j ≠ i → state_update_23 j = s j
s: composite_state components_23
i: index23
z: Z

j : index23, j ≠ i → state_update_23 j = s j
by intros; unfold state_update_23; rewrite decide_False. Qed. End sec_state_update_23_def.

(s : composite_state components_23) (i : index23) (z z' : Z), state_update_23 (state_update_23 s i z) i z' = state_update_23 s i z'

(s : composite_state components_23) (i : index23) (z z' : Z), state_update_23 (state_update_23 s i z) i z' = state_update_23 s i z'
by intros; extensionality j; unfold state_update_23; case_decide; subst. Qed.
s: composite_state components_23
z: Z

state_update_23 s two z = state_update components_23 s two z
s: composite_state components_23
z: Z

state_update_23 s two z = state_update components_23 s two z
s: composite_state components_23
z: Z

(if decide (two = two) then z else s two) = z
s: composite_state components_23
z: Z
(if decide (two = three) then z else s three) = s three
s: composite_state components_23
z: Z

(if decide (two = two) then z else s two) = z
by rewrite decide_True.
s: composite_state components_23
z: Z

(if decide (two = three) then z else s three) = s three
by rewrite decide_False. Qed.
s: composite_state components_23
z: Z

state_update_23 s three z = state_update components_23 s three z
s: composite_state components_23
z: Z

state_update_23 s three z = state_update components_23 s three z
s: composite_state components_23
z: Z

(if decide (three = two) then z else s two) = s two
s: composite_state components_23
z: Z
(if decide (three = three) then z else s three) = z
s: composite_state components_23
z: Z

(if decide (three = two) then z else s two) = s two
by rewrite decide_False.
s: composite_state components_23
z: Z

(if decide (three = three) then z else s three) = z
by rewrite decide_True. Qed.
i: index23

composite_label components_23
i: index23

composite_label components_23
i: index23

label (components_23 i)
by destruct i; exact (). Defined. Definition multiplier_23 (i : index23) : Z := match i with | two => 2 | three => 3 end.

s : composite_state components_23, valid_state_prop free_composition_23 s → i : index23, 2 ≤ zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)

s : composite_state components_23, valid_state_prop free_composition_23 s → i : index23, 2 ≤ zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
i: index23
Hi: 2 ≤ zproj s i

in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hi: 2 ≤ si

s : composite_state components_23, valid_state_prop free_composition_23 s → si = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hi: 2 ≤ si
P:= λ si : Z, s : composite_state components_23, valid_state_prop free_composition_23 s → si = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0): Z → Prop

s : composite_state components_23, valid_state_prop free_composition_23 s → si = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hi: 2 ≤ si
P:= λ si : Z, s : composite_state components_23, valid_state_prop free_composition_23 s → si = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0): Z → Prop

P si
i: index23

x : Z, ( y : Z, 2 ≤ y < x → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)) → 2 ≤ x → s : composite_state components_23, valid_state_prop free_composition_23 s → x = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i

in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si

in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3
in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3
in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si

in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i)) → in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i)) → in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
H: input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

in_futures free_composition_23 s' (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
H: input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

in_futures free_composition_23 s' (state_update_23 s' i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
H: input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

valid_state_prop free_composition_23 s'
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
H: input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))
si - 2 = zproj s' i
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
H: input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

valid_state_prop free_composition_23 s'
by eapply input_valid_transition_destination.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
H: input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

si - 2 = zproj s' i
by symmetry; apply state_update_23_eq.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

option_valid_message_prop free_composition_23 (Some 2)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
valid (label_23 i) (s, Some 2)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)
transition (label_23 i) (s, Some 2) = (s', Some (2 * multiplier_23 i))
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

option_valid_message_prop free_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

valid (label_23 i) (s, Some 2)
by destruct i; cbn in Heqsi |- *; lia.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
l: 4 ≤ si
s':= state_update_23 s i (si - 2): j : index23, state (components_23 j)

transition (label_23 i) (s, Some 2) = (s', Some (2 * multiplier_23 i))
s: composite_state components_23
Hlt: 2 ≤ zproj s two
Hind: y : Z, 2 ≤ y < zproj s two → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s two → in_futures free_composition_23 s (state_update_23 s two 0)
Hs: valid_state_prop free_composition_23 s
l: 4 ≤ zproj s two

state_update_23 s two (s two - 2) = state_update components_23 s two (s two - 2)
s: composite_state components_23
Hlt: 2 ≤ zproj s three
Hind: y : Z, 2 ≤ y < zproj s three → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s three → in_futures free_composition_23 s (state_update_23 s three 0)
Hs: valid_state_prop free_composition_23 s
l: 4 ≤ zproj s three
state_update_23 s three (s three - 2) = state_update components_23 s three (s three - 2)
s: composite_state components_23
Hlt: 2 ≤ zproj s two
Hind: y : Z, 2 ≤ y < zproj s two → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s two → in_futures free_composition_23 s (state_update_23 s two 0)
Hs: valid_state_prop free_composition_23 s
l: 4 ≤ zproj s two

state_update_23 s two (s two - 2) = state_update components_23 s two (s two - 2)
by apply state_update_23_two.
s: composite_state components_23
Hlt: 2 ≤ zproj s three
Hind: y : Z, 2 ≤ y < zproj s three → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s three → in_futures free_composition_23 s (state_update_23 s three 0)
Hs: valid_state_prop free_composition_23 s
l: 4 ≤ zproj s three

state_update_23 s three (s three - 2) = state_update components_23 s three (s three - 2)
by apply state_update_23_three.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3

in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3

input_valid_transition free_composition_23 (label_23 i) (s, Some 3) (state_update_23 s i 0, Some (3 * multiplier_23 i))
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3

option_valid_message_prop free_composition_23 (Some 3)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3
valid (label_23 i) (s, Some 3)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3
transition (label_23 i) (s, Some 3) = (state_update_23 s i 0, Some (3 * multiplier_23 i))
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3

option_valid_message_prop free_composition_23 (Some 3)
by apply initial_message_is_valid, composition_23_3_initial.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3

valid (label_23 i) (s, Some 3)
by destruct i; cbn in Heqsi |- *; lia.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
e: si = 3

transition (label_23 i) (s, Some 3) = (state_update_23 s i 0, Some (3 * multiplier_23 i))
s: composite_state components_23
Hlt: 2 ≤ s two
Hind: y : Z, 2 ≤ y < s two → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s two → in_futures free_composition_23 s (state_update_23 s two 0)
Hs: valid_state_prop free_composition_23 s
e: s two = 3
n: ¬ 4 ≤ s two

state_update_23 s two 0 = state_update components_23 s two (s two - 3)
s: composite_state components_23
Hlt: 2 ≤ s three
Hind: y : Z, 2 ≤ y < s three → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s three → in_futures free_composition_23 s (state_update_23 s three 0)
Hs: valid_state_prop free_composition_23 s
e: s three = 3
n: ¬ 4 ≤ s three
state_update_23 s three 0 = state_update components_23 s three (s three - 3)
s: composite_state components_23
Hlt: 2 ≤ s two
Hind: y : Z, 2 ≤ y < s two → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s two → in_futures free_composition_23 s (state_update_23 s two 0)
Hs: valid_state_prop free_composition_23 s
e: s two = 3
n: ¬ 4 ≤ s two

state_update_23 s two 0 = state_update components_23 s two (s two - 3)
by rewrite state_update_23_two; f_equal; lia.
s: composite_state components_23
Hlt: 2 ≤ s three
Hind: y : Z, 2 ≤ y < s three → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s three → in_futures free_composition_23 s (state_update_23 s three 0)
Hs: valid_state_prop free_composition_23 s
e: s three = 3
n: ¬ 4 ≤ s three

state_update_23 s three 0 = state_update components_23 s three (s three - 3)
by rewrite state_update_23_three; f_equal; lia.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3

in_futures free_composition_23 s (state_update_23 s i 0)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3

input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (state_update_23 s i 0, Some (2 * multiplier_23 i))
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3

option_valid_message_prop free_composition_23 (Some 2)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3
valid (label_23 i) (s, Some 2)
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3
transition (label_23 i) (s, Some 2) = (state_update_23 s i 0, Some (2 * multiplier_23 i))
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3

option_valid_message_prop free_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3

valid (label_23 i) (s, Some 2)
by destruct i; cbn in Heqsi |- *; lia.
i: index23
si: Z
Hind: y : Z, 2 ≤ y < si → s : composite_state components_23, valid_state_prop free_composition_23 s → y = zproj s i → in_futures free_composition_23 s (state_update_23 s i 0)
Hlt: 2 ≤ si
s: composite_state components_23
Hs: valid_state_prop free_composition_23 s
Heqsi: si = zproj s i
n: ¬ 4 ≤ si
n0: si ≠ 3

transition (label_23 i) (s, Some 2) = (state_update_23 s i 0, Some (2 * multiplier_23 i))
s: composite_state components_23
Hlt: 2 ≤ s two
Hind: y : Z, 2 ≤ y < s two → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s two → in_futures free_composition_23 s (state_update_23 s two 0)
Hs: valid_state_prop free_composition_23 s
n0: s two ≠ 3
n: ¬ 4 ≤ s two

state_update_23 s two 0 = state_update components_23 s two (s two - 2)
s: composite_state components_23
Hlt: 2 ≤ s three
Hind: y : Z, 2 ≤ y < s three → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s three → in_futures free_composition_23 s (state_update_23 s three 0)
Hs: valid_state_prop free_composition_23 s
n0: s three ≠ 3
n: ¬ 4 ≤ s three
state_update_23 s three 0 = state_update components_23 s three (s three - 2)
s: composite_state components_23
Hlt: 2 ≤ s two
Hind: y : Z, 2 ≤ y < s two → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s two → in_futures free_composition_23 s (state_update_23 s two 0)
Hs: valid_state_prop free_composition_23 s
n0: s two ≠ 3
n: ¬ 4 ≤ s two

state_update_23 s two 0 = state_update components_23 s two (s two - 2)
by rewrite state_update_23_two; f_equal; lia.
s: composite_state components_23
Hlt: 2 ≤ s three
Hind: y : Z, 2 ≤ y < s three → s : composite_state components_23, valid_state_prop free_composition_23 s → y = s three → in_futures free_composition_23 s (state_update_23 s three 0)
Hs: valid_state_prop free_composition_23 s
n0: s three ≠ 3
n: ¬ 4 ≤ s three

state_update_23 s three 0 = state_update components_23 s three (s three - 2)
by rewrite state_update_23_three; f_equal; lia. Qed.
From any composite state whose components are larger than 1 there is a valid trace reaching state00.

s2 s3 : Z, 2 ≤ s2 → 2 ≤ s3 → in_futures free_composition_23 (state_23 s2 s3) state00

s2 s3 : Z, 2 ≤ s2 → 2 ≤ s3 → in_futures free_composition_23 (state_23 s2 s3) state00
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

in_futures free_composition_23 (state_23 s2 s3) state00
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3) → in_futures free_composition_23 (state_23 s2 s3) state00
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3) → in_futures free_composition_23 (state_23 s2 s3) state00
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

in_futures free_composition_23 (state_23 0 s3) state00
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

in_futures free_composition_23 (state_23 0 s3) (state_update_23 (state_23 0 s3) three 0)
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)
state_update_23 (state_23 0 s3) three 0 = state00
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

in_futures free_composition_23 (state_23 0 s3) (state_update_23 (state_23 0 s3) three 0)
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

valid_state_prop free_composition_23 (state_23 0 s3)
by eapply in_futures_valid_snd.
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

state_update_23 (state_23 0 s3) three 0 = state00
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

state_update_23 (state_23 0 s3) three 0 two = 0
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)
state_update_23 (state_23 0 s3) three 0 three = 0
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

state_update_23 (state_23 0 s3) three 0 two = 0
by rewrite state_update_23_neq.
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
H1: in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)

state_update_23 (state_23 0 s3) three 0 three = 0
by rewrite state_update_23_three; state_update_simpl.
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

in_futures free_composition_23 (state_23 s2 s3) (state_update_23 (state_23 s2 s3) two 0)
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
state_update_23 (state_23 s2 s3) two 0 = state_23 0 s3
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

in_futures free_composition_23 (state_23 s2 s3) (state_update_23 (state_23 s2 s3) two 0)
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

valid_state_prop free_composition_23 (state_23 s2 s3)
by apply initial_state_is_valid; intros []; cbn; red; lia.
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

state_update_23 (state_23 s2 s3) two 0 = state_23 0 s3
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

state_update_23 (state_23 s2 s3) two 0 two = 0
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3
state_update_23 (state_23 s2 s3) two 0 three = s3
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

state_update_23 (state_23 s2 s3) two 0 two = 0
by rewrite state_update_23_two; state_update_simpl.
s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3

state_update_23 (state_23 s2 s3) two 0 three = s3
by rewrite state_update_23_neq. Qed. Definition composite_state_23_sum (s : composite_state components_23) : Z := s two + s three. Definition parity_constraint_23 (l : composite_label components_23) (sm : composite_state components_23 * option multiplying_message) : Prop := let sm' := composite_transition components_23 l sm in Z.Even (composite_state_23_sum sm.1 + composite_state_23_sum sm'.1). Definition parity_composition_23 : VLSM multiplying_message := composite_vlsm components_23 parity_constraint_23.
l: composite_label components_23
s: composite_state components_23
m: multiplying_message

parity_constraint_23 l (s, Some m) ↔ Z.Even m
l: composite_label components_23
s: composite_state components_23
m: multiplying_message

parity_constraint_23 l (s, Some m) ↔ Z.Even m
l: composite_label components_23
s: composite_state components_23
m: multiplying_message

Z.Even ((s, Some m).1 two + (s, Some m).1 three + ((composite_transition components_23 l (s, Some m)).1 two + (composite_transition components_23 l (s, Some m)).1 three)) ↔ Z.Even m
by split; intros [n Hn]; destruct l as [[] li]; cbn in *; state_update_simpl; exists (s two + s three - n); lia. Qed.

m : multiplying_message, valid_message_prop parity_composition_23 m → m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)

m : multiplying_message, valid_message_prop parity_composition_23 m → m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)
m: multiplying_message
s: state parity_composition_23
Hvsm: valid_state_message_prop parity_composition_23 s (Some m)

m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)
m: multiplying_message
s: state parity_composition_23
Hvsm: valid_state_message_prop parity_composition_23 s (Some m)
Hom: is_Some (Some m)

m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)
m: multiplying_message
s: state parity_composition_23
Hvsm: valid_state_message_prop parity_composition_23 s (Some m)
Hom: is_Some (Some m)

is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
m: multiplying_message
s: state parity_composition_23
om: option multiplying_message
Hvsm: valid_state_message_prop parity_composition_23 s om
Hom: is_Some om

is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
s: state parity_composition_23
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop parity_composition_23 om
Hom: is_Some om

is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
s: state parity_composition_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: state parity_composition_23
om: option multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s om
l: label parity_composition_23
Hv: valid l (s, om)
s': state parity_composition_23
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
IHHvsm2: Hom : is_Some om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
s: state parity_composition_23
Hs: initial_state_prop s
om: option multiplying_message
Hom0: option_initial_message_prop parity_composition_23 om
Hom: is_Some om

is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
m: multiplying_message
Hom0: composite_initial_message_prop components_23 m

m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)
s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
x: multiplying_message
i: x = 2

x = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ x = 2 ^ p2 * 3 ^ p3)
by right; exists 1, 0; split; lia.
s: state parity_composition_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: state parity_composition_23
om: option multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s om
l: label parity_composition_23
Hv: valid l (s, om)
s': state parity_composition_23
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
IHHvsm2: Hom : is_Some om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)

is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
s: state parity_composition_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: state parity_composition_23
om: option multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s om
l: label parity_composition_23
Hv: valid l (s, om)
Hc: Z.Even (composite_state_23_sum (s, om).1 + composite_state_23_sum (composite_transition components_23 l (s, om)).1)
s': state parity_composition_23
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
IHHvsm2: Hom : is_Some om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)

p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: state parity_composition_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: state parity_composition_23
om: option multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s om
l: label parity_composition_23
Hv: valid l (s, om)
Hc: Z.Even (composite_state_23_sum (s, om).1 + composite_state_23_sum (composite_transition components_23 l (s, om)).1)
s': state parity_composition_23
om': option multiplying_message
Ht: transition l (s, om) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
IHHvsm2: Hom : is_Some om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some om

p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: state parity_composition_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: state parity_composition_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
l: label parity_composition_23
Hv: valid l (s, Some m)
Hc: Z.Even (composite_state_23_sum (s, Some m).1 + composite_state_23_sum (composite_transition components_23 l (s, Some m)).1)
s': state parity_composition_23
om': option multiplying_message
Ht: transition l (s, Some m) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
IHHvsm2: Hom : is_Some (Some m), is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)

p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
l: composite_label components_23
Hv: let (i, li) := l in valid li (s i, Some m)
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (let (i, li) := l in let (si', om') := transition li (s i, Some m) in (state_update components_23 s i si', om')).1)
s': composite_state components_23
om': option multiplying_message
Ht: (let (i, li) := l in let (si', om') := transition li (s i, Some m) in (state_update components_23 s i si', om')) = (s', om')
Hom: is_Some om'
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
IHHvsm2: m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)

p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s two (s two - 3)))
Hv: 23 ≤ s two
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some 3)
Hom: is_Some (Some (2 * 3))
Ht: (state_update components_23 s two (s two - 3), Some (2 * 3)) = (state_update components_23 s two (s two - 3), Some (2 * 3))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some 3)

p2 p3 : Z, p2 >= 1 ∧ p3 >= 02 * 3 = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s two
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s two (s two - m)))
Hom: is_Some (Some (2 * m))
Ht: (state_update components_23 s two (s two - m), Some (2 * m)) = (state_update components_23 s two (s two - m), Some (2 * m))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
p2, p3: Z
Hgt1: p2 >= 1
Heq: p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3
p2 p3 : Z, p2 >= 1 ∧ p3 >= 02 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s three (s three - 3)))
Hv: 23 ≤ s three
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some 3)
Hom: is_Some (Some (3 * 3))
Ht: (state_update components_23 s three (s three - 3), Some (3 * 3)) = (state_update components_23 s three (s three - 3), Some (3 * 3))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some 3)
p2 p3 : Z, p2 >= 1 ∧ p3 >= 03 * 3 = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s three (s three - m)))
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
p2, p3: Z
Hgt1: p2 >= 1
Heq: p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3
p2 p3 : Z, p2 >= 1 ∧ p3 >= 03 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s two (s two - 3)))
Hv: 23 ≤ s two
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some 3)
Hom: is_Some (Some (2 * 3))
Ht: (state_update components_23 s two (s two - 3), Some (2 * 3)) = (state_update components_23 s two (s two - 3), Some (2 * 3))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some 3)

p2 p3 : Z, p2 >= 1 ∧ p3 >= 02 * 3 = 2 ^ p2 * 3 ^ p3
by exists 1, 1; lia.
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s two
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s two (s two - m)))
Hom: is_Some (Some (2 * m))
Ht: (state_update components_23 s two (s two - m), Some (2 * m)) = (state_update components_23 s two (s two - m), Some (2 * m))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
p2, p3: Z
Hgt1: p2 >= 1
Heq: p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3

p2 p3 : Z, p2 >= 1 ∧ p3 >= 02 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s two
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s two (s two - m)))
Hom: is_Some (Some (2 * m))
Ht: (state_update components_23 s two (s two - m), Some (2 * m)) = (state_update components_23 s two (s two - m), Some (2 * m))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
p2, p3: Z
Hgt1: p2 >= 1
Heq: p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3

p3 >= 02 * m = 2 ^ Z.succ p2 * 3 ^ p3
by rewrite Z.pow_succ_r; lia.
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s three (s three - 3)))
Hv: 23 ≤ s three
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some 3)
Hom: is_Some (Some (3 * 3))
Ht: (state_update components_23 s three (s three - 3), Some (3 * 3)) = (state_update components_23 s three (s three - 3), Some (3 * 3))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some 3)

p2 p3 : Z, p2 >= 1 ∧ p3 >= 03 * 3 = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s three (s three - 3)))

False
s: composite_state components_23
n: Z
Hn: s two + s three + (state_update components_23 s three (s three - 3) two + state_update components_23 s three (s three - 3) three) = 2 * n

False
by state_update_simpl; lia.
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s three (s three - m)))
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
p2, p3: Z
Hgt1: p2 >= 1
Heq: p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3

p2 p3 : Z, p2 >= 1 ∧ p3 >= 03 * m = 2 ^ p2 * 3 ^ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s three (s three - m)))
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
p2, p3: Z
Hgt1: p2 >= 1
Heq: p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3

p2 >= 1 ∧ Z.succ p3 >= 03 * m = 2 ^ p2 * 3 ^ Z.succ p3
s: composite_state components_23
_om: option multiplying_message
Hvsm1: valid_state_message_prop parity_composition_23 s _om
_s: composite_state components_23
m: multiplying_message
Hvsm2: valid_state_message_prop parity_composition_23 _s (Some m)
Hv: 2 ≤ m ≤ s three
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s three (s three - m)))
Hom: is_Some (Some (3 * m))
Ht: (state_update components_23 s three (s three - m), Some (3 * m)) = (state_update components_23 s three (s three - m), Some (3 * m))
IHHvsm1: Hom : is_Some _om, is_Some_proj Hom = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ is_Some_proj Hom = 2 ^ p2 * 3 ^ p3)
H_om: is_Some (Some m)
p2, p3: Z
Hgt1: p2 >= 1
Heq: p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3

Z.succ p3 >= 03 * m = 2 ^ p2 * 3 ^ Z.succ p3
by rewrite Z.pow_succ_r; lia. Qed.

p2 p3 : Z, 1 ≤ p2 → 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)

p2 p3 : Z, 1 ≤ p2 → 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)
p2: Z
Hp2: 1 ≤ p2

p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)
p2: Z
Hp2: 1 ≤ p2
P:= λ p2 : Z, p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3): Z → Prop

p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)
p2: Z
Hp2: 1 ≤ p2
P:= λ p2 : Z, p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3): Z → Prop

P p2

x : Z, ( y : Z, 1 ≤ y < x → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)) → 1 ≤ x → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ x * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2

p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: 11
Hind: y : Z, 1 ≤ y < 1 p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)

p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)
Hp2: 11
Hind: y : Z, 1 ≤ y < 1 p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)

p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
Hp2: 11

x : Z, 0 ≤ x → valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ x) → valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ Z.succ x)
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ Z.succ p3)
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

can_emit parity_composition_23 (2 ^ 1 * 3 ^ Z.succ p3)
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

input_valid_transition parity_composition_23 (existT three multiply_label) (state_23 1 (2 * 3 ^ p3), Some (2 ^ 1 * 3 ^ p3)) (state10, Some (2 ^ 1 * 3 ^ Z.succ p3))
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

valid_state_prop parity_composition_23 (state_23 1 (2 * 3 ^ p3))
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
option_valid_message_prop parity_composition_23 (Some (2 ^ 1 * 3 ^ p3))
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
22 ^ 1 * 3 ^ p3
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
2 ^ 1 * 3 ^ p3 ≤ state_23 1 (2 * 3 ^ p3) three
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
parity_constraint_23 (existT three multiply_label) (state_23 1 (2 * 3 ^ p3), Some (2 ^ 1 * 3 ^ p3))
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
transition (existT three multiply_label) (state_23 1 (2 * 3 ^ p3), Some (2 ^ 1 * 3 ^ p3)) = (state10, Some (2 ^ 1 * 3 ^ Z.succ p3))
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

valid_state_prop parity_composition_23 (state_23 1 (2 * 3 ^ p3))
by apply initial_state_is_valid; intros []; cbn; red; lia.
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

option_valid_message_prop parity_composition_23 (Some (2 ^ 1 * 3 ^ p3))
done.
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

22 ^ 1 * 3 ^ p3
by lia.
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

2 ^ 1 * 3 ^ p3 ≤ state_23 1 (2 * 3 ^ p3) three
by cbn; lia.
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

parity_constraint_23 (existT three multiply_label) (state_23 1 (2 * 3 ^ p3), Some (2 ^ 1 * 3 ^ p3))
by apply parity_constraint_23_even; exists (3 ^ p3); lia.
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

transition (existT three multiply_label) (state_23 1 (2 * 3 ^ p3), Some (2 ^ 1 * 3 ^ p3)) = (state10, Some (2 ^ 1 * 3 ^ Z.succ p3))
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

state_update components_23 (state_23 1 (2 * 3 ^ p3)) three (2 * 3 ^ p3 - 2 ^ 1 * 3 ^ p3) = state10
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)
Some (3 * (2 ^ 1 * 3 ^ p3)) = Some (2 ^ 1 * 3 ^ Z.succ p3)
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

state_update components_23 (state_23 1 (2 * 3 ^ p3)) three (2 * 3 ^ p3 - 2 ^ 1 * 3 ^ p3) = state10
by extensionality i; destruct i; state_update_simpl; cbn; lia.
Hp2: 11
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)

Some (3 * (2 ^ 1 * 3 ^ p3)) = Some (2 ^ 1 * 3 ^ Z.succ p3)
by f_equal; rewrite Z.pow_succ_r; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1

p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

valid_message_prop parity_composition_23 (2 ^ p2 * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

can_emit parity_composition_23 (2 ^ p2 * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

input_valid_transition parity_composition_23 (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) (state01, Some (2 ^ p2 * 3 ^ p3))
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

valid_state_prop parity_composition_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3
option_valid_message_prop parity_composition_23 (Some (2 ^ (p2 - 1) * 3 ^ p3))
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3
22 ^ (p2 - 1) * 3 ^ p3
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3
2 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 two
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3
parity_constraint_23 (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3))
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3
transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) = (state01, Some (2 ^ p2 * 3 ^ p3))
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

valid_state_prop parity_composition_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1)
by apply initial_state_is_valid; intros []; cbn; red; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

option_valid_message_prop parity_composition_23 (Some (2 ^ (p2 - 1) * 3 ^ p3))
by apply Hind; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

22 ^ (p2 - 1) * 3 ^ p3
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

22 ^ Z.succ (p2 - 2) * 3 ^ p3
by rewrite Z.pow_succ_r; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

2 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 two
by cbn; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

parity_constraint_23 (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3))
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

2 ^ (p2 - 1) * 3 ^ p3 = 2 * (2 ^ (p2 - 2) * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

2 ^ Z.succ (p2 - 2) * 3 ^ p3 = 2 * (2 ^ (p2 - 2) * 3 ^ p3)
by rewrite Z.pow_succ_r; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) = (state01, Some (2 ^ p2 * 3 ^ p3))
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3
Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01
by extensionality i; destruct i; state_update_simpl; cbn; lia.
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)
p2: Z
Hind: y : Z, 1 ≤ y < p2 → p3 : Z, 0 ≤ p3 → valid_message_prop parity_composition_23 (2 ^ y * 3 ^ p3)
Hp2: 1 ≤ p2
n: p2 ≠ 1
p3: Z
Hp3: 0 ≤ p3

Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ Z.succ (p2 - 1) * 3 ^ p3)
by f_equal; rewrite !Z.pow_succ_r; lia. Qed.
The valid messages of the parity_composition_23 VLSM consist of the initial message 3 together with all even integers larger than 1 which can be decomposed as a product of powers of 2 and 3.

m : multiplying_message, valid_message_prop parity_composition_23 m ↔ m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)

m : multiplying_message, valid_message_prop parity_composition_23 m ↔ m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)
m: multiplying_message

valid_message_prop parity_composition_23 m → m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)
m: multiplying_message
m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop parity_composition_23 m
m: multiplying_message

valid_message_prop parity_composition_23 m → m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)
by apply parity_composition_23_valid_messages_powers_of_23_right.
m: multiplying_message

m = 3 ∨ ( p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop parity_composition_23 m

valid_message_prop parity_composition_23 3
x, x0: Z
H: x >= 1
H0: x0 >= 0
valid_message_prop parity_composition_23 (2 ^ x * 3 ^ x0)

valid_message_prop parity_composition_23 3
by apply initial_message_is_valid, composition_23_3_initial.
x, x0: Z
H: x >= 1
H0: x0 >= 0

valid_message_prop parity_composition_23 (2 ^ x * 3 ^ x0)
by apply parity_composition_23_valid_messages_powers_of_23_left; lia. Qed.
Final states are valid states from which no further valid transition can be taken.
Definition parity_23_final_state (s : composite_state components_23) : Prop :=
  valid_state_prop parity_composition_23 s /\
  ~ exists
      (l : composite_label components_23)
      (om : option multiplying_message)
      (som' : composite_state components_23 * option multiplying_message),
        input_valid_transition parity_composition_23 l (s, om) som'.

n, m: Z
Hn: n >= 1
Hm: m >= 1

valid_state_prop parity_composition_23 (state_23 n m)
n, m: Z
Hn: n >= 1
Hm: m >= 1

valid_state_prop parity_composition_23 (state_23 n m)
by apply initial_state_is_valid; intros []; cbn; red. Qed.

valid_state_prop parity_composition_23 state11

valid_state_prop parity_composition_23 state11
by apply (valid_state_23_geq1 1 1); lia. Qed.

valid_state_prop parity_composition_23 state22

valid_state_prop parity_composition_23 state22
by apply valid_state_23_geq1. Qed.
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 0 n)
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 0 n)
n: Z
Hn: n >= 1

input_valid_transition parity_composition_23 (existT two multiply_label) (state_23 2 n, Some 2) (state_23 0 n, Some 4)
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 2 n)
n: Z
Hn: n >= 1
option_valid_message_prop parity_composition_23 (Some 2)
n: Z
Hn: n >= 1
22
n: Z
Hn: n >= 1
2 ≤ state_23 2 n two
n: Z
Hn: n >= 1
parity_constraint_23 (existT two multiply_label) (state_23 2 n, Some 2)
n: Z
Hn: n >= 1
transition (existT two multiply_label) (state_23 2 n, Some 2) = (state_23 0 n, Some 4)
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 2 n)
by apply valid_state_23_geq1.
n: Z
Hn: n >= 1

option_valid_message_prop parity_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.
n: Z
Hn: n >= 1

22
by lia.
n: Z
Hn: n >= 1

2 ≤ state_23 2 n two
by cbn; lia.
n: Z
Hn: n >= 1

parity_constraint_23 (existT two multiply_label) (state_23 2 n, Some 2)
by apply parity_constraint_23_even; exists 1; lia.
n: Z
Hn: n >= 1

transition (existT two multiply_label) (state_23 2 n, Some 2) = (state_23 0 n, Some 4)
by cbn; f_equal; extensionality i; destruct i; cbn; state_update_simpl; cbn. Qed.
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 n 0)
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 n 0)
n: Z
Hn: n >= 1

input_valid_transition parity_composition_23 (existT three multiply_label) (state_23 n 2, Some 2) (state_23 n 0, Some 6)
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 n 2)
n: Z
Hn: n >= 1
option_valid_message_prop parity_composition_23 (Some 2)
n: Z
Hn: n >= 1
22
n: Z
Hn: n >= 1
2 ≤ state_23 n 2 three
n: Z
Hn: n >= 1
parity_constraint_23 (existT three multiply_label) (state_23 n 2, Some 2)
n: Z
Hn: n >= 1
transition (existT three multiply_label) (state_23 n 2, Some 2) = (state_23 n 0, Some 6)
n: Z
Hn: n >= 1

valid_state_prop parity_composition_23 (state_23 n 2)
by apply valid_state_23_geq1.
n: Z
Hn: n >= 1

option_valid_message_prop parity_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.
n: Z
Hn: n >= 1

22
by lia.
n: Z
Hn: n >= 1

2 ≤ state_23 n 2 three
by cbn; lia.
n: Z
Hn: n >= 1

parity_constraint_23 (existT three multiply_label) (state_23 n 2, Some 2)
by apply parity_constraint_23_even; exists 1; lia.
n: Z
Hn: n >= 1

transition (existT three multiply_label) (state_23 n 2, Some 2) = (state_23 n 0, Some 6)
cbn; f_equal; extensionality i; destruct i; cbn; state_update_simpl; cbn; lia. Qed.

valid_state_prop parity_composition_23 state00

valid_state_prop parity_composition_23 state00

input_valid_transition parity_composition_23 (existT three multiply_label) (state02, Some 2) (state00, Some 6)

valid_state_prop parity_composition_23 state02

option_valid_message_prop parity_composition_23 (Some 2)

22

2 ≤ state02 three

parity_constraint_23 (existT three multiply_label) (state02, Some 2)

transition (existT three multiply_label) (state02, Some 2) = (state00, Some 6)

valid_state_prop parity_composition_23 state02
by apply valid_state0n.

option_valid_message_prop parity_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.

22
by lia.

2 ≤ state02 three
by unfold state02; cbn; lia.

parity_constraint_23 (existT three multiply_label) (state02, Some 2)
by red; cbn; unfold composite_state_23_sum; state_update_simpl; cbn; exists 1.

transition (existT three multiply_label) (state02, Some 2) = (state00, Some 6)
by cbn; f_equal; extensionality i; destruct i; cbn; state_update_simpl; cbn. Qed.

valid_state_prop parity_composition_23 state01

valid_state_prop parity_composition_23 state01
by apply valid_state0n. Qed.

valid_state_prop parity_composition_23 state10

valid_state_prop parity_composition_23 state10
by apply valid_staten0. Qed.
s: composite_state components_23

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state s
s: composite_state components_23

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state s
s: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11

parity_23_final_state s
s: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11

valid_state_prop parity_composition_23 s
s: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som')
s: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11

valid_state_prop parity_composition_23 s

valid_state_prop parity_composition_23 state00

valid_state_prop parity_composition_23 state01

valid_state_prop parity_composition_23 state10

valid_state_prop parity_composition_23 state11

valid_state_prop parity_composition_23 state00
by apply valid_state00.

valid_state_prop parity_composition_23 state01
by apply valid_state01.

valid_state_prop parity_composition_23 state10
by apply valid_state10.

valid_state_prop parity_composition_23 state11
by apply valid_state11.
s: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11

¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som')
s: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
i: index23
li: label (components_23 i)
om: option multiplying_message
som': (composite_state components_23 * option multiplying_message)%type
Hs: valid_state_prop parity_composition_23 s
Hom: option_valid_message_prop parity_composition_23 om
Hv: valid (existT i li) (s, om)
Hc: parity_constraint_23 (existT i li) (s, om)

False
s: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
i: index23
li: label (components_23 i)
om: option multiplying_message
som': (composite_state components_23 * option multiplying_message)%type
Hs: valid_state_prop parity_composition_23 s
Hom: option_valid_message_prop parity_composition_23 om
Hv: valid (existT i li) (s, om)
n: Z
Hc: composite_state_23_sum (s, om).1 + composite_state_23_sum (composite_transition components_23 (existT i li) (s, om)).1 = 2 * n

False
by destruct i; (destruct om ; [| done]); unfold composite_state_23_sum in Hc; cbn in *; state_update_simpl; destruct Hcases as [| [| []]]; subst; cbn in *; lia. Qed.

s : composite_state components_23, valid_state_prop parity_composition_23 s → i : index23, zproj s i >= 0

s : composite_state components_23, valid_state_prop parity_composition_23 s → i : index23, zproj s i >= 0
s': state parity_composition_23
l: label parity_composition_23
om, om': option multiplying_message
s: state parity_composition_23
Ht: input_valid_transition parity_composition_23 l (s, om) (s', om')
IHHs: i : index23, zproj s i >= 0

i : index23, zproj s' i >= 0
s': state parity_composition_23
j: index23
lj: label (components_23 j)
om, om': option multiplying_message
s: state parity_composition_23
Hv: valid (existT j lj) (s, om)
Hc: parity_constraint_23 (existT j lj) (s, om)
Ht: transition (existT j lj) (s, om) = (s', om')
IHHs: i : index23, zproj s i >= 0

i : index23, zproj s' i >= 0
s': state parity_composition_23
j: index23
lj: label (components_23 j)
om, om': option multiplying_message
s: state parity_composition_23
Hv: valid (existT j lj) (s, om)
Hc: parity_constraint_23 (existT j lj) (s, om)
Ht: transition (existT j lj) (s, om) = (s', om')
i: index23
IHHs: zproj s i >= 0

zproj s' i >= 0
by destruct j; (destruct om ; [| done]); inversion Ht; subst; clear Ht; cbn in *; destruct i; cbn in *; state_update_simpl; lia. Qed.
s: composite_state components_23

parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23

parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')

s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1 → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')

s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1 → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 0
H0: s three = 0

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 0
H0: s three = 1
s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 1
H0: s three = 0
s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 1
H0: s three = 1
s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 0
H0: s three = 0

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
by left; extensionality x; destruct x.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 0
H0: s three = 1

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
by right; left; extensionality x; destruct x.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 1
H0: s three = 0

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
by right; right; left; extensionality x; destruct x.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
H: s two = 1
H0: s three = 1

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
by right; right; right; extensionality x; destruct x.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')

s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hfinal: ¬ ( (l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l ( s, om) som')
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)

s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)

(l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som'
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)

s two > 1 ∨ s three > 1
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1
(l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som'
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1
(l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som'
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)

s two > 1 ∨ s three > 1
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
H: zproj s two >= 0

s two > 1 ∨ s three > 1
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
H: zproj s two >= 0
H0: zproj s three >= 0

s two > 1 ∨ s three > 1
by cbn in *; lia.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

(l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som'
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1
(l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som'
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

(l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som'
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

input_valid_transition parity_composition_23 (existT two ()) (s, Some 2) (state_update components_23 s two (s two - 2), Some 4)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

option_valid_message_prop parity_composition_23 (Some 2)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1
22
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1
2 ≤ s two
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1
parity_constraint_23 (existT two ()) (s, Some 2)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

option_valid_message_prop parity_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

22
by lia.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

2 ≤ s two
by lia.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s two > 1

parity_constraint_23 (existT two ()) (s, Some 2)
by apply parity_constraint_23_even; exists 1; lia.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1

(l : composite_label components_23) (om : option multiplying_message) (som' : composite_state components_23 * option multiplying_message), input_valid_transition parity_composition_23 l (s, om) som'
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1

input_valid_transition parity_composition_23 (existT three ()) (s, Some 2) (state_update components_23 s three (s three - 2), Some 6)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1

option_valid_message_prop parity_composition_23 (Some 2)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1
22
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1
2 ≤ s three
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1
parity_constraint_23 (existT three ()) (s, Some 2)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1

option_valid_message_prop parity_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1

22
by lia.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1

2 ≤ s three
by lia.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
n: ¬ (s two = 0 ∧ s three = 0 ∨ s two = 0 ∧ s three = 1 ∨ s two = 1 ∧ s three = 0 ∨ s two = 1 ∧ s three = 1)
Hs1: s three > 1

parity_constraint_23 (existT three ()) (s, Some 2)
by apply parity_constraint_23_even; exists 1; lia. Qed.
The final states of the parity_composition_23 VLSM consist of state00, state01, state10, and state11.
s: composite_state components_23

parity_23_final_state s ↔ s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23

parity_23_final_state s ↔ s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23

parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
s: composite_state components_23
s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state s
s: composite_state components_23

parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11
by apply parity_23_final_state_prop23_right.
s: composite_state components_23

s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state s
by apply parity_23_final_state_prop23_left. Qed.

s : composite_state components_23, valid_state_prop parity_composition_23 s → (i : index23) (n : Z), 0 ≤ n → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)

s : composite_state components_23, valid_state_prop parity_composition_23 s → (i : index23) (n : Z), 0 ≤ n → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
i: index23
n: Z
Hn: 0 ≤ n

zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n

s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
P:= λ n : Z, s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0): Z → Prop

s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
P:= λ n : Z, s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0): Z → Prop

P n
i: index23
P:= λ n : Z, s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0): Z → Prop

n : Z, 0 ≤ n → P n
i: index23

s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * 0 → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
x : Z, 0 ≤ x → ( s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * x → in_futures parity_composition_23 s (state_update_23 s i 0)) → s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * Z.succ x → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23

s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * 0 → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * 0

in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * 0

state_update_23 s i 0 = s
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s two = 2 * 0

state_update_23 s two 0 = s
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s three = 2 * 0
state_update_23 s three 0 = s
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s two = 2 * 0

state_update_23 s two 0 = s
by rewrite state_update_23_two, state_update_id.
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s three = 2 * 0

state_update_23 s three 0 = s
by rewrite state_update_23_three, state_update_id.
i: index23

x : Z, 0 ≤ x → ( s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * x → in_futures parity_composition_23 s (state_update_23 s i 0)) → s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * Z.succ x → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n

in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i)) → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i)) → in_futures parity_composition_23 s (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
H: input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

in_futures parity_composition_23 s' (state_update_23 s i 0)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
H: input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

in_futures parity_composition_23 s' (state_update_23 s' i 0)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
H: input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

valid_state_prop parity_composition_23 s'
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
H: input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))
zproj s' i = 2 * n
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
H: input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

valid_state_prop parity_composition_23 s'
by eapply input_valid_transition_destination.
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
H: input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))

zproj s' i = 2 * n
by subst s'; rewrite state_update_23_eq, Hsi; lia.
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

option_valid_message_prop parity_composition_23 (Some 2)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
valid (label_23 i) (s, Some 2)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
parity_constraint_23 (label_23 i) (s, Some 2)
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)
transition (label_23 i) (s, Some 2) = (s', Some (2 * multiplier_23 i))
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

option_valid_message_prop parity_composition_23 (Some 2)
by apply initial_message_is_valid, composition_23_2_initial.
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

valid (label_23 i) (s, Some 2)
by destruct i; cbn in Hsi |- *; lia.
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

parity_constraint_23 (label_23 i) (s, Some 2)
by apply parity_constraint_23_even; exists 1; lia.
i: index23
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s i = 2 * n → in_futures parity_composition_23 s (state_update_23 s i 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s i = 2 * Z.succ n
s':= state_update_23 s i (zproj s i - 2): j : index23, state (components_23 j)

transition (label_23 i) (s, Some 2) = (s', Some (2 * multiplier_23 i))
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s two = 2 * n → in_futures parity_composition_23 s (state_update_23 s two 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s two = 2 * Z.succ n
s':= state_update_23 s two (zproj s two - 2): j : index23, state (components_23 j)

s' = state_update components_23 s two (s two - 2)
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s three = 2 * n → in_futures parity_composition_23 s (state_update_23 s three 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s three = 2 * Z.succ n
s':= state_update_23 s three (zproj s three - 2): j : index23, state (components_23 j)
s' = state_update components_23 s three (s three - 2)
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s two = 2 * n → in_futures parity_composition_23 s (state_update_23 s two 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s two = 2 * Z.succ n
s':= state_update_23 s two (zproj s two - 2): j : index23, state (components_23 j)

s' = state_update components_23 s two (s two - 2)
by apply state_update_23_two.
n: Z
Hn: 0 ≤ n
IHn: s : composite_state components_23, valid_state_prop parity_composition_23 s → zproj s three = 2 * n → in_futures parity_composition_23 s (state_update_23 s three 0)
s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s three = 2 * Z.succ n
s':= state_update_23 s three (zproj s three - 2): j : index23, state (components_23 j)

s' = state_update components_23 s three (s three - 2)
by apply state_update_23_three. Qed.
From any composite state whose components are even non-negative integers there is a valid trace reaching state00.

s2 s3 : Z, 0 ≤ s2 → 0 ≤ s3 → in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) state00

s2 s3 : Z, 0 ≤ s2 → 0 ≤ s3 → in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) state00
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) state00
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3)) → in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) state00
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3)) → in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) state00
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

in_futures parity_composition_23 (state_23 0 (2 * s3)) state00
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

in_futures parity_composition_23 (state_23 0 (2 * s3)) (state_update_23 (state_23 0 (2 * s3)) three 0)
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))
state_update_23 (state_23 0 (2 * s3)) three 0 = state00
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

in_futures parity_composition_23 (state_23 0 (2 * s3)) (state_update_23 (state_23 0 (2 * s3)) three 0)
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

valid_state_prop parity_composition_23 (state_23 0 (2 * s3))
by eapply in_futures_valid_snd.
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

state_update_23 (state_23 0 (2 * s3)) three 0 = state00
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

state_update_23 (state_23 0 (2 * s3)) three 0 two = 0
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))
state_update_23 (state_23 0 (2 * s3)) three 0 three = 0
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

state_update_23 (state_23 0 (2 * s3)) three 0 two = 0
by rewrite state_update_23_neq.
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
H1: in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))

state_update_23 (state_23 0 (2 * s3)) three 0 three = 0
by rewrite state_update_23_three; state_update_simpl.
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_update_23 (state_23 (2 * s2) (2 * s3)) two 0)
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 = state_23 0 (2 * s3)
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_update_23 (state_23 (2 * s2) (2 * s3)) two 0)
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * s3))
H, H0: 00

valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * 0))
s3: Z
H: 00
H0: 0 ≤ s3
n: s3 ≠ 0
valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * s3))
s2: Z
H: 0 ≤ s2
H0: 00
n: s2 ≠ 0
valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * 0))
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
n: s2 ≠ 0
n0: s3 ≠ 0
valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * s3))
H, H0: 00

valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * 0))
by apply valid_state00.
s3: Z
H: 00
H0: 0 ≤ s3
n: s3 ≠ 0

valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * s3))
by apply valid_state0n; lia.
s2: Z
H: 0 ≤ s2
H0: 00
n: s2 ≠ 0

valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * 0))
by apply valid_staten0; lia.
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
n: s2 ≠ 0
n0: s3 ≠ 0

valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * s3))
by apply valid_state_23_geq1; lia.
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 = state_23 0 (2 * s3)
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 two = 0
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 three = 2 * s3
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 two = 0
by rewrite state_update_23_two; state_update_simpl.
s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3

state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 three = 2 * s3
by rewrite state_update_23_neq. Qed. End sec_23_composition.